I've actually been updating quantomatic to take advantage of the new IDE support. It's generally pretty straightforward, since we've been emulating Isabelle's toplevel (rather than SML) for a long time now.
In terms of organisation, this is what I had in mind. Basically, we need to be able to load ~100 ML files in one of two ways. The first is within Isabelle/jEdit (IDE-style) for development. The second is to batch-process them to make a heap, for deployment as part of the Quantomatic GUI.
My thinking was to use .thy files to play the role of old-style ROOT.ML files, and have one thy file for each "logical chunk" (i.e. subdirectory) of the code, which would just contain many "ML_file" declarations. Then, for batch processing, use a shell script to turn these thy files into plain ML, essentially by deleting the front-matter and replacing "ML_file" by "use". Then, process these files these with poly, after loading our isabelle-emulation code.
Given that I want to keep isabelle strictly optional to the build process, this seems the most efficient. Any comments/pointers?
On 13 December 2014 at 13:53, Lucas Dixon <lucas.dixon at gmail.com> wrote:
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
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml