Re: [isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal

2018-06-28 Thread Rafal Kolanski
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

2018-06-27 Thread Makarius
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