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

[Alexander Krauss]

On 06/29/2012 12:27 AM, Jasmin Christian Blanchette wrote:

>> Since our component store grows monotonically,
>
> The way I see it, obsolete components should be removed, so as to
> minimize confusion.

No reason for confusion here, since Admin/components tells you what you 
need (and I am assuming there is a little script that will download it 
for you if you are not sitting on NFS).

Removing "obsolete" (wrt. to what? The repository tip? The latest 
release?) versions raises the question of how to easily retrieve the 
matching revisions for older Isabelle versions. There must be a formal 
link to the matching revision in the component repository.

So here is another implementation alternative for all this:
- This assumes universal components.
- Instead of Admin/components as a file with references, there is a hg 
repository (using the largefiles extension), which evolves along with 
Isabelle and always contains exactly the components that would now be 
mentioned in Admin/components.
- The Isabelle repository contains a file with the hash of the matching 
revision in the component repository, which serves as a formal link.
- Thus, to get a fully working installation for a given Isabelle 
revision, it is enough to update the component repository to the 
matching revision, which will automatically download the relevant files.

This looks pretty much equivalent to the other proposed solutions, at 
least at this late hour. But it needs some testing with real data to get 
some experience with the largefile extension. Moreover, I am not sure if 
Mercurial 2.0+ can really be assumed to be available everywhere. My 
Debian stable installation still has 1.6.4. Currently, Isabelle 
development works just fine even with very old Mercurial.

>> 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"?

This was assuming that we do not remove old components.

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

They are easy to use, since there are not many ways how we would use 
them: Component upload can be done via a web interface, and download is 
via http, following some path conventions. Not sure about installation 
and maintenance. They do impose some conventions and strange terminology 
on you though, which come from the Maven way of organizing stuff.

> What are the arguments in favor of a monotonic store as
> opposed to removing obsoleted components?

Well, in the end these are different implementations of the same thing, 
so the question is which one is simpler to use and maintain in the 
end... I don't know.

Alex