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 <[email protected]> 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 <[email protected]> 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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
