Thanks for the update!
I'm going to try and update TheoryMine to the latest Isabelle, that way I'll get to play with all that cool new work you've been doing :)
On 13 December 2014 at 02:15, Makarius <makarius at sketis.net> wrote:
On Fri, 12 Dec 2014, Lucas Dixon wrote:
If you really want plain SML'97, then your best approach might be to
cannibalize Isabelle, pull out it's build system, and hack it's IDE a little, and build your own SML'97 IDE. But this is probably quite a big task.
Lucas, we've had many private discussions about that in the past, so lets continue that publicly now.
What I've done in Isabelle2014 is the following:
The Isabelle/Pure/PIDE environment is able to include strict SML'97 modules with their own toplevel ML name space: command 'SML_file'.
It is possible to move toplevel bindings back and forth between the Isabelle/ML and SML environment: command 'SML_import' and 'SML_export'.
In $ISABELLE_HOME/src/Tools/SML/Examples.thy there are some tiny examples to illustrate that, e.g. the Isabelle/ML function Output.writeln is re-used for SML to make output actually visible in the IDE and not get lost on bare stdout via TextIO.print etc.
Another example is to re-use the Isabelle/ML Par_List.map combinator for SML: it provides already some realistic parallel programming facility at very little cost for an existing program.
Many things can be imagined beyond this:
Some way to single-out SML programs for standalone builds, without the Isabelle or PIDE framework around it.
Some way to allow multiple simultaneous arguments for SML_file: the compiler could be instructed to find signature/structure/functor definitions according to certain naming conventions of source files, without requiring the usual sequential load order of the logical framework.
Emulation of the SML/NJ make system, to allow easy inclusion of other SML projects.
As a start, I am considering to make a stand-alone Isabelle/SML/PIDE distribution next time. I have already reduced the disk footprint drastically, by using only JRE and not full JDK, and without the Isabelle/HOL image it will come out rather small.
Makarius
http://stop-ttip.org 1,143,454 people so far