[isabelle-dev] repository and components etc.

[Makarius]

On Wed, 29 Aug 2012, Christian Urban wrote:

>
> On Wednesday, August 29, 2012 at 21:45:35 (+0200), Makarius wrote:
> >
> > It is still used for isatest runs, but it does not have to be made public
> > as a crippled distribution that lacks most add-on components.
>
> If it is only a small effort, I am happy to keep
> it. The add-on components can normally be supplied easily.
> Instead of having to fiddle with mercurial and clone

This seems to describe the old state of affairs.  In the past 12 months or 
so there have been several initiatives by Florian Haftmann and others, to 
end the "fiddling" with the repository.  This is now converging to a 
pretty good state, so it is worth investing some time to learn how it 
works.


> it is also an easy way to have several "snapshots" work concurrently on 
> a machine (my brain handles dates much better than for example 
> f781bbe0d91b, though I appreciate that this extra mental effort is 
> sometimes needed).

Since Alex Krauss requested that for Mira, there is now the possibilty to 
provide ISABELLE_IDENTIFIER for unidentified repository versions from 
outside, e.g. like this:

   $ env ISABELLE_IDENTIFIER=latest isabelle getenv ISABELLE_HOME_USER
   ISABELLE_HOME_USER=/home/makarius/.isabelle/latest

It is then up to you to map the friendly Mercurial ids into symbolic names 
like above.


> Finally, I regarded the isatest blessing as a sign that nothing is 
> broken, which is reassuring when you live on the development edge.

Mira provides more fine-grained information already.


 	Makarius