[isabelle-dev] isabelle build

[Christian Sternagel]

Dear Makarius,

I am just about to test how  our IsaFoR project can be built with 
'isabelle build' (very nice, by the way!), which would allow us to get 
rid of a really ugly Makefile and several *.ML "driver" files. One thing 
I noticed:

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

(where 'isadev' is just a shell script that points to the development 
version of Isabelle; such that 'isabelle' always points to the latest 
stable release). Now in a ROOT file I expected

session AFP in "$ISAFOR_AFP" = HOL +
   options [document = false]
   theories
     "Abstract-Rewriting/Abstract_Rewriting"
     (*and many more*)

to work. But when invoking

   $ isadev build -d . -b HOL-AFP

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

When I use a hard-wired absolute path instead of $ISAFOR_AFP it works.

cheers

chris