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

Alexander Krauss krauss at in.tum.de
Fri Jun 29 00:13:49 CEST 2012

> 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.

On 06/28/2012 09:54 PM, Makarius wrote:
> Proper versioning (with Mercurial) would solve several problems:
> * canonical identification of *the* true content of component repository
> * Unix permissions done right in shared space
> * built-in ssh/http pull

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.

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).


More information about the isabelle-dev mailing list