Re: [isabelle] CInterface in Isabelle 2016-1



On 21/12/16 19:43, albert rizaldi wrote:
> 
> In the news for Isabelle 2016-1, it is written that "low-level ML system
> structures are no longer exposed to Isabelle/ML user-space". I guess
> this is probably the reason why I cannot "open CInterface" in Isabelle
> 2016-1 any longer. Is there another way I could use the CInterface
> structure or is it not possible any more in Isabelle 2016-1?

Yes, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/ML/ml_name_space.ML#l73

Since Isabelle2016-1 has become final on 13-Dec-2016 (after 6 weeks with
stable release candidates), you need to change the source privately
yourself, and hand over such a change to anybody who uses your Isabelle
application.

Also note that CInterface in Poly/ML has been superseded by Foreign: it
basically does the same thing, but in a better way.


	Makarius






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