[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