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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
