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



Hi Florian,

Thanks for your reply.  The possible future extension of Isabelle with
hierarchical theory names explains the difference in behaviour between
the Haskell target of export_code (which does export to different
files) and the SML target (which doesn't), as Haskell itself has
hierarchical module names, then.

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?

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
>




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