[isabelle-dev] isabelle build

[Christian Sternagel]

How about dedicated sessions for code-generation? Would that make sense? 
E.g., in IsaFoR we currently have a Makefile target as follows

code: $(ISABELLE_OUTPUT)/Isafor
	@cd IsaFoR; \
   $(ISABELLE_TOOL) codegen Isafor Ceta \
   'certify_proof in Haskell module_name Ceta file "../generated/Haskell/"'

which just takes care of generating code. It would be nice not to have 
to fallback to Makefiles (to get the dependencies right).

cheers

chris

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