[isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
Rafal Kolanski
xs at xaph.net
Mon Jun 25 06:45:04 CEST 2018
Isabelle Developers,
While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT
environment variable functionality has been removed.
We have previously used this functionality for the following scenarios:
- networked home directory storing Isabelle settings, but heaps built on
a different, faster / not backed up drive
- checking out two revisions of the same repository and building them
with the same settings and version of Isabelle, or running them
side-by-side on the screen
- appending extra information from the environment to ISABELLE_OUTPUT,
allowing us to build the same repository at the same revision with
different environments (e.g. using L4V_ARCH to select the
target architecture for seL4 verification) and caching the images
The common thread between these scenarios is that the settings we use
are nearly identical, with ISABELLE_OUTPUT being the variance.
Using separate ISABELLE_HOME would be overkill.
A typical setting of ISABELLE_OUTPUT/ISABELLE_PATH we use here is:
USER_HEAPS=${OVERRIDE_USER_HEAPS:-"$ISABELLE_HOME_USER/heaps-${L4V_ARCH}${ISABELLE_HOME//\//-}"}
ISABELLE_OUTPUT=${OVERRIDE_ISABELLE_OUTPUT:-"$USER_HEAPS"}
ISABELLE_PATH=${OVERRIDE_ISABELLE_PATH:-"$USER_HEAPS"}
What is now the canonical way of supporting the workflows I described
above without having to duplicate most of etc/ jedit/ and contrib/ now
that both ISABELLE_PATH and ISABELLE_OUTPUT are gone?
Sincerely,
Rafal Kolanski
More information about the isabelle-dev
mailing list