[isabelle-dev] isabelle build

[Makarius]

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:

http://isabelle.in.tum.de/repos/isabelle/file/fb446a780d50/src/HOL/Mirabelle/ex/Ex.thy

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.


 	Makarius