Re: [isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
On 28/06/18 05:27, Makarius wrote: > On 25/06/18 06:45, Rafal Kolanski wrote: >> >> While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT >> environment variable functionality has been removed. > > This refers to > > changeset: 68219:c0341c0080e2 > user:wenzelm > date:Sat May 19 15:45:45 2018 +0200 > description: > clarified store directories; > discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT; > > >> 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"} > > This example already motivates the change: ISABELLE_OUTPUT and > ISABELLE_PATH were somehow duplicates, with subtle differences. Together > with the "system build mode" (option -s of "isabelle build", "isabelle > jedit" etc.) it has lead to an ill-defined situation. Agreed, ISABELLE_PATH and ISABELLE_OUTPUT were confusing. > I have now refined the change further in > > changeset: 68523:ccacc84e0251 > user:wenzelm > date:Wed Jun 27 20:31:22 2018 +0200 > description: > clarified settings -- avoid hard-wired directories; > tuned documentation; > > > I.e. you can use ISABELLE_HEAPS above. My sincere thanks for adding this, it really makes a big difference to our workflow. Rafal Kolanski ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
On 25/06/18 06:45, Rafal Kolanski wrote: > > While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT > environment variable functionality has been removed. This refers to changeset: 68219:c0341c0080e2 user:wenzelm date:Sat May 19 15:45:45 2018 +0200 description: clarified store directories; discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT; > 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"} This example already motivates the change: ISABELLE_OUTPUT and ISABELLE_PATH were somehow duplicates, with subtle differences. Together with the "system build mode" (option -s of "isabelle build", "isabelle jedit" etc.) it has lead to an ill-defined situation. I have now refined the change further in changeset: 68523:ccacc84e0251 user:wenzelm date:Wed Jun 27 20:31:22 2018 +0200 description: clarified settings -- avoid hard-wired directories; tuned documentation; I.e. you can use ISABELLE_HEAPS above. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev