Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Separate code extraction for multiple Isabelle...

view this post on Zulip Email Gateway (Aug 22 2022 at 14:48):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,

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.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 22 2022 at 14:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominic,

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:49):

From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:50):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

signature.asc

Last updated: Apr 23 2024 at 12:29 UTC