Re: [isabelle] Separate code extraction for multiple Isabelle theories



Hi Dominic,

> 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.

I'll take Âreflect the breakdown â into Isabelle theories as a starting
point.

Indeed, after issuing

export_code distinct in SML file "/tmp/all.ML"

you see that the generated code is structured into ML modules reflecting
the underlying theory name space.  It is not generated into separated
files since it is not clear how this shall look for hierarchical theory
names, which however have not emerged in Isabelle yet.

Note however that especially the basic HOL theories Âas they are have a
lot of mutual depdencies wrt. code equations, so using separate modules
may need considerable tweaking of the name space using Âcode_identifierÂ
declarations.  See also Â7.2 of the tutorial on code generation.

Hope this helps,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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