Email Gateway (Aug 19 2022 at 15:28): Email Gateway (Aug 19 2022 at 15:28):From: Lars Hupel <hupel@in.tum.de>
Hello,
I'm trying to change the heap directory when building in non-system mode
(i.e. default mode). So far, I've tried setting 'ISABELLE_HOME_USER' and
'ISABELLE_OUTPUT' as an environment variable:
$ ISABELLE_HOME_USER=/tmp/isa isabelle build -D . -vb
It still keeps using '$HOME/.isabelle' as 'ISABELLE_HOME_USER'. Upon
closer inspection of 'etc/settings', that doesn't seem surprising, since
this setting is just overridden:
if [ -z "$ISABELLE_IDENTIFIER" ]; then
ISABELLE_HOME_USER="$USER_HOME/.isabelle"
else
ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
fi
Is it actually possible to change this directory without touching
'etc/settings'?
Cheers
Lars
Email Gateway (Aug 19 2022 at 15:28):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Lars,
Can't you just "$USER_HOME"? This is the usual trick, cf. the thread titled "Testboard problem" on "isabelle-dev" (4 to 7 July 2014).
Jasmin
Email Gateway (Aug 19 2022 at 15:28):From: Lars Noschinski <noschinl@in.tum.de>
USER_HOME is taken from the environment and could point to another
etc/settings file. You probably could also use a little bit of Scala
instead of isabelle build?
Email Gateway (Aug 19 2022 at 15:30):From: Makarius <makarius@sketis.net>
USER_HOME is a portable version of plain HOME, so by default it should not
be changed, unless there is a very special situation.
As a general principle, Isabelle settings variables are better changed
within a settings file, e.g. $ISABELLE_HOME_USER/etc/settings, or any
other settings within some component directory. Since this is just a bash
script, some program logic can be embedded into it to pick up external
environment variables to manipulate its operation.
A special case is ISABELLE_IDENTIFIER, which may be set by external means
to pretend that the Isabelle release name is something else. Thus it
determines the location of ISABELLE_HOME_USER and ISABELLE_OUTPUT
indirectly.
Here is an example:
$ ISABELLE_IDENTIFIER=XYZ Isabelle2014-RC4/bin/isabelle getenv ISABELLE_OUTPUT
ISABELLE_OUTPUT=/Users/makarius/.isabelle/XYZ/heaps/polyml-5.5.2_x86-darwin
Makarius
Last updated: Apr 25 2024 at 16:19 UTC