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



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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