Makarius,
On 11 Dec 2014, at 4:14, Makarius <makarius at sketis.net> wrote:
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.
Sorry, my mistake.
Sounds like I might as well use emacs rather than ?plain jEdit with its static ML mode? for this purpose.
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.
So, err, if my little project is more like the ?ML bootstrap environment of Isabelle? and less like ?many modules of Isabelle/Pure? then ?the Prover IDE? is not going to help me, is it?
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.
So I think we run the risk of the no true Scotsman fallacy here. One could argue that Isabelle is not an SML program (ah, I note you said it was the ?largest ML program that I know of?).
I don?t want to (merely) sit around splitting hairs - I want to hack a program that uses Poly/ML?s wonderful concurent/parallel runtime.
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.
No, I think in terms of wonderful dependency-discovering tools like ?ghc ?make Main.hs? that go off and build my universe for me. Yes, they don?t work so well with preprocessors etc. I?m looking for the (S)ML equivalent of ghci.
I need to think about the guts of the thy file as I have to list my (S)ML files in dependency order, and every time I add another file to my project, which is common for new things.
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).
That takes us far away from my simple concerns about REPLs and error messages.
Thanks for all your work on this. I wish I could use it.
cheers peter