On Wed, 10 Dec 2014, Peter Gammie wrote:
I’m not adverse to trying out JEdit, but it seems to dodge the issues
somewhat. Is anyone using it for hacking large-scale SML programs?
The largest ML program that I know of is Isabelle/HOL with all its add-on
tools: even big things like the Metis prover are incorporated there. The
Prover IDE is used routinely for editing Isabelle/HOL theories and ML
modules -- I also made special tricks in IDE memory management to support
this on current mainstream/low-end hardware with only 8 GB.
One measure of adequacy might be if JEdit/SML (err, Isabelle/SML?) can
load the foundational Isabelle stuff, e.g. Pure/ROOT.ML. (How do you
hack Isabelle/Pure presently?)
I don't "hack" on Isabelle/Pure, but edit it carefully and thoughtfully,
using plain jEdit with its static ML mode. It is still not possible to
load this ML bootstrap environment of Isabelle into Isabelle/PIDE, though.
There are some partial solutions to that: many ML modules of Isabelle/Pure
can be loaded individually into the Prover IDE via ML_file in Pure.thy.
In particular I’d want access to Poly/ML’s concurrency primitives. It
seems to nuke Poly/ML’s “use” function, which is a little unfriendly.
Can you explain what you mean? PolyML.use is not part of the SML
standard. The Isabelle/SML environment takes care to load sources via
'SML_file' commands -- it has to do that to manage changes and versions
properly.
BTW I have no problem cranking out .thy files as a kind of fake build
system if that’s what it takes.
This sounds like you still think in terms of "make" files to build things.
In PIDE you just assemble your project, presently by some .thy file as
shown in the SML example in the Documentation panel, and then edit without
further thinking about it.
An open problem is to generate a compiled application directly from this
IDE model, but right now Isabelle/SML is not a specific "product" for such
standalone application development yet (unless you want to ship it as
Isabelle session).
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 1,127,322 people so far
----------------------------------------------------------------------------_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
