[isabelle-dev] NEWS

Makarius makarius at sketis.net
Tue Dec 2 18:59:40 CET 2008


On Tue, 2 Dec 2008, Tjark Weber wrote:

> On Sun, 2008-11-30 at 13:03 +0100, Makarius wrote:
> > * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
> > old ~/isabelle, which was slightly non-standard and apt cause
> > surprises on case-insensitive file-systems, or when working with local 
> > copies of the Isabelle repository.
> 
> I am using the repository version of Isabelle.

BTW, thanks to Mercurial you can now refer to the actual version you are 
using, by means of the unique changeset id.  (This might be important in a 
less trivial situation, because "the" repository is in continues flow.)


> Despite "isabelle getenv -a" reporting
> 
> ISABELLE_HOME_USER=/home/weber/.isabelle
> ISABELLE_OUTPUT=/home/weber/.isabelle/heaps//polyml-5.2_x86-linux
> 
> the command "./build Pure" creates a heap file in
> 
> /home/weber/isabelle/heaps/polyml-5.2_x86-linux
> 
> (Note the missing ".".)  Am I doing something wrong?

This is right.  The build script produces heaps for the "distribution" 
which is your repository clone here, which appears to be ~/isabelle

In fact, one reason for the change of ISABELLE_HOME_USER=$HOME/.isabelle 
with the dot was to avoid a clash in excactly this situation.  Now your 
user config directory and distribution directory are clearly separated.

Of course, heaps produced inside the repository file space like that must 
not be committed.


	Makarius


More information about the isabelle-dev mailing list