Email Gateway (Aug 22 2022 at 14:42): Email Gateway (Aug 22 2022 at 14:42):From: albert rizaldi <rizaldi@in.tum.de>
Hi everyone,
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?
Thanks,
Albert
Email Gateway (Aug 22 2022 at 14:43):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 16:19 UTC