[isabelle] Code Generator and export of functions in Haskell


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… :)


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