Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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:

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

Cheers,
Moa

view this post on Zulip 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:

see NEWS:

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: Mar 29 2024 at 08:18 UTC