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