Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation in Isabelle


view this post on Zulip Email Gateway (Aug 18 2022 at 17:54):

From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello all,

at the moment, we have two code generators in Isabelle:

  1. An ancient code generator in Isabelle by Stefan Berghofer - limited
    to SML without supporting type classes.
    Commands to invoke it were code_module and code_library.

  2. A generic code generator in Isabelle by Florian Haftmann - extenible
    to multiple target languages, supporting type classes, basic integration
    of reflection and abstraction mechanisms
    Commands to invoke it are export_code, value, code_reflect, and some others.

The second subsumes the first, so we intend to remove the first code
generator from the next Isabelle distribution if there are not any
strong defenders of the ancient code generator.

Any thoughts?

Lukas

view this post on Zulip Email Gateway (Aug 18 2022 at 17:54):

From: Steven Obua <steven.obua@googlemail.com>
Actually, there is a third code generator hidden somewhere in Isabelle.

view this post on Zulip Email Gateway (Aug 18 2022 at 17:55):

From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
We moved recently to the new code-generator.

Burkhart


Last updated: Apr 26 2024 at 20:16 UTC