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

[Jasmin Christian Blanchette]

Hi Alex,

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

There is a conceptual mismatch, but even forgetting about third-party components most Mercurial repositories have some files that don't really change or change monotonically. As an example, there's plenty of open-source software that has separate "NEWS.xxx" files for different versions "xxx" and one would normally just monotonically add new files. Hence, SCM users are familiar with the situation and still prefer it to having to deal with an entirely different system (at least on a small scale).

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

The way I see it, obsolete components should be removed, so as to minimize confusion. When E-1.5 appears, we should remove E-1.4, since it's obsoleted. Just like "Metis in Isabelle2012" obsoletes "Metis in Isabelle2011" and there's no way to use the old Metis with the new Isabelle. And E-1.0 to E-1.3 should have been removed a long time ago. For good reasons; as an example recent repository versions of Isabelle require SPASS 3.8ds or better, even though it was released only a few months ago.

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

I'm not sure I'm following this part about "pull" vs. "update". Sure, the components are really big and should arguably live in a different Mercurial repository than Isabelle, but how is "pull" vs. "update" more expensive than copying files around using "scp"?

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

Yes, I agree with you here.

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

How easy are these to use? Are they worth learning in addition to Mercurial? What are the arguments in favor of a monotonic store as opposed to removing obsoleted components?

Jasmin