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

> One more export_code question: what is the best way to force the
> export of every constant and function that I have defined in a given
> development?  I have a theory with >300 constants, numerous functions
> defined within it, as well as multiple other large theories with large
> numbers of constants, definitions, and functions.  Obviously I could
> name all of these constants in an export_code command, but I wonder if
> there is a better way?

Try sth like

	export_code "Foo._"

Hope this helps

> Thanks,
> Dominic
> On 8 December 2016 at 13:58, Florian Haftmann
> <florian.haftmann at> wrote:
>> 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:


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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