[isabelle-dev] NEWS: Isabelle support for Standard ML

[Makarius]

On Mon, 31 Mar 2014, Lars Noschinski wrote:

> On 31.03.2014 16:04, Makarius wrote:
>> What we have here is the Isabelle Prover IDE technology used for
>> something that is not Isabelle, namely official Standard ML.  It is
>> just a coincidence that it runs within the same Poly/ML runtime system
>> -- there is no direct connection to the Isabelle/ML world.
>>
>> This means regular SML projects can be edited with it, assuming that
>> the "build" process is not too exotic --- just the typical list of
>> "use" statements (without nesting) that need to be replaced by
>> 'SML_file' here.
> I tried to load Pure.ML with SML_File, but this probably qualifies as a
> "too exotic" build process ;)

You probaly mean Pure/ROOT.ML, but that is beyond anything that could be 
called a build process.  The bootstrapping of Isabelle/ML is very 
delicate, even after many rounds of clarification and simplification over 
the years.  (Most recently in Isabelle/bf1bdf335ea0, Isabelle/4cc3f4db3447 
from last week.)

The recent thread "Hints on Isabelle/ML IDE" has some explanations about 
this very special ML project:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-March/005106.html

The situation might still improve, when I get some more ideas how to use 
Isabelle/Pure as a "holodeck" to simulate itself, which might actually 
work out soon.


I am presently more concerned about the Isabelle/HOL bootstrap process. 
It is technically a plain Isabelle/ML application, but so huge that the 
IDE has problems digesting it.  Something might happen here within a few 
days -- right now I am again working there.


 	Makarius