[polyml] Is Isabelle/PolyML reentrant? (fwd)

-- John Matthews Assistant Professor johnm@cse.ogi.edu OGI School of Science & Engineering (503) 748-1220 Oregon Health & Science University http://cse.ogi.edu/~johnm Beaverton, OR USA ---------- Forwarded message ---------- Date: Thu, 18 Mar 2004 15:58:41 -0800 (PST) From: John Matthews johnm@cse.ogi.edu To: isabelle-users@cl.cam.ac.uk Subject: Is Isabelle/PolyML reentrant? Tom Harke and I are interested in modifying an external oracle (verification tool) for Isabelle that is written in C. We would like the oracle to call back to selected Isabelle tactics while it is running, in order to deal with verification conditions that the external oracle can't handle itself. For this to work, the foreign function interface of the underlying SML compiler needs to allow foreign functions to call SML functions. I've found documentation for SML/NJ that indicates that this is possible, but nothing in the Poly ML documentation says that this can be done. Does this mean that I will be limited to running Isabelle on SML/NJ? If so, is support for running Isabelle on SML/NJ going to continue, or will future versions of Isabelle be limited to running only on Poly ML? Thanks, -john