[isabelle-dev] Fwd: Re: new isabelle interface
makarius at sketis.net
Mon Aug 25 13:52:26 CEST 2008
On Mon, 25 Aug 2008, Michael Nedzelsky wrote:
> > I plan to use SML.NET to compile Isabelle. Does anyone forsee any
> > problems with this? Is Isabelle's code fairly portable across Standard
> > ML compilers?
> The SML.NET user manual says (p. 4).
> "No interactive evaluation. The interactive environment is for compilation
> of stand-alone applications or libraries only. SML expressions can not be
> evaluated interactively and the use command is not available."
> Isabelle sources contains many "use commands", so it will not
> run on SML.NET.
This should settle that question. Runtime "use" of ML source is an
inherent requirement of the LCF-style architecture of Isabelle. Building
theories and corresponding proof tools etc. is an alternating process that
Concerning the general architecture of UI vs. prover there is the
fundamental choice of having everything in a single process vs. the Proof
General way of speaking to a separate prover process via pipes. In
Coq-IDE you have the first variant, where everything is in OCaml. This
simplifies the implementation, because values can be passed between the
prover and GUI without a separate protocol. On the other hand, I've heard
from Coq users that Coq-IDE stability suffers signigicantly from joining
the two parts in one process, and they want to traditional Proof General
Since we do not really have the choice in Isabelle anyway (there is no
real GUI support in Poly/ML), we can be glad to be on the right track
already: keep with the separate process model. Apart from stability it
also allows to run the prover and GUI an separate machines. (``Modern''
GUIs do need 1 or 2 cores for themselves, just to display things to the
More information about the isabelle-dev