[isabelle-dev] isabelle build
makarius at sketis.net
Tue Jul 31 16:51:35 CEST 2012
On Tue, 31 Jul 2012, Christian Sternagel wrote:
> 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).
I've seen such postprocess scripts before, and found the following way to
do it without inventing new build features:
Thus the script depends formally on the other session, running in its own
derived session context, although that is quite heavy.
For codegen their might be special considerations to get more directly to
the result, without relaunching the command-line version of it. Florian
should be able to say more.
More information about the isabelle-dev