[isabelle-dev] NEWS: Isabelle support for Standard ML
makarius at sketis.net
Mon Mar 31 17:07:31 CEST 2014
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:
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.
More information about the isabelle-dev