[isabelle-dev] isabelle build

[Makarius]

On Tue, 31 Jul 2012, Christian Sternagel wrote:

> We use an environment variable ISAFOR_AFP (set in each users etc/settings 
> file) to locate the local AFP repo. In my case this is, e.g.,
>
>  $ isadev getenv -b ISAFOR_AFP
>  ~/Repos/afp/thys

> Now in a ROOT file I expected
>
> session AFP in "$ISAFOR_AFP" = HOL +
>  options [document = false]
>  theories
>    "Abstract-Rewriting/Abstract_Rewriting"
>    (*and many more*)
>
> I obtain the error
>
>  I/O error: Cannot run program 
> "/home/griff/Repos/isabelle/lib/scripts/process" (in directory 
> "$USER_HOME/Repos/afp/thys"): java.io.IOException: error=2, No such file or 
> directory

The tilde in the value of $ISAFOR_AFP is not a valid directory, but a meta 
character (coincidentally of both bash and Isabelle Path specifications).

So it depends how often the path specification happens to be expanded.

Path variables are meant to refer to closed paths, without further 
variables.  So if you write:

   ISAFOR_AFP="$HOME/Repos/afp/thys"

in the bash script where you presumable introduce that definition, it 
should work.


Another unrelated snag: bash ~ expands to $HOME in certain situations, and 
Isabelle ~ to USER_HOME, and both happen to be the same only on Posix 
systems.  On Cygwin $HOME is the "system home" of the Cygwin installation, 
but only if it is run in default configuration.  Sometimes $HOME can be 
$USER_HOME as well.


 	Makarius