Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code Generator and export of functions in Haskell

Email Gateway (Aug 19 2022 at 15:54):

From: Moa Johansson <moa.johansson@chalmers.se>
Hi,

Updating the code for our Hipster system which relies on the code generator. I notice that the function ‘export_code’ has changed, and obtained an extra boolean argument ‘all_public’. I also notice that the generated code now differs, in that it now exports the functions given from Isabelle, so we get the module header:

module Main (Tree, tmap, mirror) where…

instead of as previously (in Isabelle2013-2):

module Main where…

I would have assumed that setting ‘all_public’ to false would have produced the same version of Isabelle2013-2, which is what our tool expects the Haskell file to look like. However, this does not appear to be the case. So:

• What does ‘all_public’ change?
• Is there a possibility to get the code generator to produce the same header as in Isabelle2013-2, or do I have to work around the fact that it insist on exporting my functions?

I’m aware that we’re probably not using the code generator for the same purpose as most users, but still… :)

Cheers,
Moa

Email Gateway (Aug 19 2022 at 15:54):

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

Updating the code for our Hipster system which relies on the code
generator. I notice that the function ‘export_code’ has changed, and
obtained an extra boolean argument ‘all_public’. I also notice that the
generated code now differs, in that it now exports the functions given
from Isabelle, so we get the module header:

module Main (Tree, tmap, mirror) where…

instead of as previously (in Isabelle2013-2):

module Main where…

I would have assumed that setting ‘all_public’ to false would have produced the same version of Isabelle2013-2, which is what our tool expects the Haskell file to look like. However, this does not appear to be the case. So:

• What does ‘all_public’ change?
• Is there a possibility to get the code generator to produce the same header as in Isabelle2013-2, or do I have to work around the fact that it insist on exporting my functions?

see NEWS:

• Code generator: minimize exported identifiers by default. Minor
  INCOMPATIBILITY.

I.e. by default (not all_public) only the requested set of identifiers
is exported, else (all_public) all are exported explicitly.

There is no way to get the pre-Isabelle2014 headers back. I have no
idea what your application is, but you can strip the export lists using
e.g. a suitable perl script.

Hope this helps,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC