[isabelle-dev] isabelle build

[Christian Sternagel]

Another thing,

In the example below Abstract-Rewriting did initially not build (since I 
forgot to update my local AFP clone). Instead of giving me an 
error-message (which did work when I just put the single theory 
Abstract_Rewriting under "theories"), however, the build process ran for 
more than 20 minutes (using several GB of RAM) before I killed it manually.

cheers

chris

On 07/31/2012 01:38 PM, Christian Sternagel wrote:
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev