[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

Makarius makarius at sketis.net
Fri Jun 29 16:37:55 CEST 2012

On Fri, 29 Jun 2012, Alexander Krauss wrote:

>> On Thu, 28 Jun 2012, Tjark Weber wrote:
>>> Directories would be more amenable to version control than tarballs, if
>>> that makes a difference.
> These are build artifacts, not sources, so SCM a la Mercurial is a 
> conceptual mismatch: There is no real notion of "change" (just monotonic 
> addition of new components), no diffs, no merges etc.

I did not know this "build artifacts" business yet, but after some web 
browsing I now understand for what SVN used to be abused in the past.

Here is a comparison matrix for the 3 main players in the field (from the 
Maven perspective):

Artifactory appears to win in most respects; this is consistent with what 
I've seen on Stackoverflow discussions etc. about the same question "foo 
vs. bar vs. baz" in artifact management.

> I looked briefly at Mercurial's largefiles extension, but I don't think 
> it is suitable: The extension helps in situations when the repository 
> history consumes significantly more space than the working directory due 
> to large binaries that are part of previous revisions but not the 
> current ones, since they were changed or removed.

BTW Mercurial classifies largefiles (and subrepositories) as "Features of 
Last Resort" http://mercurial.selenic.com/wiki/FeaturesOfLastResort

They say:

   Needing (or thinking you need) these features is often an indicator of a
   bad practice somewhere else in your workflow.

> Since our component store grows monotonically, there is no benefit from 
> largefiles, since the size of the tip revision basically equals the size 
> of the whole repository. In practice, this means that a pull would be 
> cheap, but an update would be prohibitively expensive.
> The above assumes that we simply try to manage the flat directory as a 
> hg repository. Trying to capture the evolution of components (i.e., 
> different versions) does not really make sense, since each component 
> evolves completely independently, and it would not be clear what a given 
> revision of the component repository would mean.
> All this is just the conceptual difference between a source code 
> repository such as Mercurial and build artifact repositories such as 
> Sonatype Nexus or Artifactory. These basically implement a monotonic 
> file store (plus integration with certain build frameworks which is 
> quite irrelevant for us).

These observations are very important.  What we have is a monotonic store 
of "artifacts", where certain Isabelle versions take a projection 
according to Admin/components or similar.  This allows to use the Isabelle 
history in the expected way, e.g. bisect over a certain range with the
right components being used automatically.  No restriction to "latest 
this, latest that", with implicit meaning of "latest".

Artifactory seems to be the "solves all your problems solution", but it is 
also quite large.  See also http://www.jfrog.com/products.php

Here is a live demo 

This means all this infrastructure offers a plain hierarchic web download 
in the end -- no need to use Maven.  A modest wget script can still 
download components as plain URLs.  On the server side it is a bit more 
than just a modest python script, though ...


More information about the isabelle-dev mailing list