[isabelle] Separate code extraction for multiple Isabelle theories


Is there a way of inducing Isabelle's export_code feature to
compositionally export code from Isabelle theories without
regenerating previously exported code over and over again?

That is: say I have two theories Foo.thy and Goo.thy, with Goo.thy
depending on Foo.thy.  I want to export code from both theories, so I
first export the contents of Foo.thy into foo.ML.  Now, exporting code
from Goo.thy into goo.ML regenerates bits of Foo.thy that Goo.thy
relies on and places those bits in goo.ML.  Is there a way of
indicating to Isabelle that this code already exists, and should not
be re-exported?

My use case is: I have a large model of a file format in Isabelle.  I
want to extract code from this and wrap it in untrusted hand written
code for validation purposes.  I do not want all of my Isabelle
development to be extracted into a single monolithic ML file, as that
would be unwieldy to work with, but rather have the generated ML files
reflect the breakdown of my development into Isabelle theories.  How
best to do this, if it is at all possible?  The codegen.pdf file
included with Isabelle is silent on this point.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.