[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