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
	Florian

> 
> Thanks,
> Dominic
> 
> On 8 December 2016 at 13:58, Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de> 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:
>> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>

-- 

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.