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

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

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


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