Re: [isabelle] ISABELLE_OUTPUT



On Tue, 19 Aug 2014, Lars Noschinski wrote:

On 19.08.2014 16:09, Lars Hupel wrote:
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'?
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?

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.