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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
