[isabelle-dev] Fwd: Re: new isabelle interface

[Makarius]

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 
never stops.

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 
mode back.

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 
user.)


	Makarius