Email Gateway (Aug 18 2022 at 10:37): Email Gateway (Aug 18 2022 at 10:37):From: Jonas Bergerson <jonas.bergerson@hotmail.de>
Hello everyone,
I'm approaching you with a rather technical question: Is there a way to start Isabelle (in Isar interaction mode) from within PolyML? I'm far from familiar with the technical side of Isabelle. I tried this:
./poly-driver -r -H 80 /usr/local/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL /usr/local/polyml/x86-linux/ML_dbase
This brings me the same welcome message, as when I run "isabelle -I", but the line "Welcome to Isabelle/HOL (Isabelle2005: October 2005)" is missing, so I still need to do something to get into "Isabelle mode".
Thank you,
Jonas.
The show must go on! Ihre Diashow auf Ihrem Space! Jetzt loslegen!
http://get.live.com/spaces/overview
Email Gateway (Aug 18 2022 at 10:38):From: Makarius <makarius@sketis.net>
Above you've started a naked Poly/ML process with the HOL heap preloaded.
By invoking Isar.main() you should get into the usual interactive toplevel
-- use 'exit' to get back to ML.
Note that this is still not the real "Isabelle mode", because the process
environment (for settings etc.) is missing. Since the "isabelle" (or
"isabelle-process") script already provides full access to both ML and
Isabelle, I don't see any need to invoke polyml manually.
Makarius
Last updated: May 03 2024 at 04:19 UTC