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