Re: [isabelle] Starting Isabelle from within PolyML

On Sat, 7 Jul 2007, Jonas Bergerson wrote:

> 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".

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.


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