There is an interesting thing here which I'd like make sure is said explicitly: if you're interested in writing ML (not SML'97 as Makarius points out), then writing your program on top of Isabelle is something you should seriously consider. You get a better build system, an IDE, and tons of very helpful libraries. One downside of using this approach is you end up with a bigger binary.
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. Short of that, I'd go for using a custom PolyML use function with some modifications. This is more or less what was done for Quantomatic ( https://github.com/Quantomatic/quantomatic/blob/stable/core/ROOT.ML) - along with pulling out a bunch of the lovely Isabelle library functions. But it is worth noting that what you get here is not necessarily exactly SML'97, it's very likely to end up with some PolyML specific magic in it (at least that's how quantomatic ended up). If I was to do Quantomatic again, I'd probably have just built it directly on Isabelle, and not worried about all the background theory stuff (main reason not to at the time was that I didn't get the benefits of the IDE as it was still early days). best, lucas On 12 December 2014 at 02:55, Makarius <[email protected]> wrote: > On Thu, 11 Dec 2014, Peter Gammie wrote: > > On 11 Dec 2014, at 4:14, Makarius <[email protected]> wrote: >> >>> >>> I don’t "hack" on Isabelle/Pure, but edit it carefully and thoughtfully, >>> using plain jEdit with its static ML mode. >>> >> >> Sounds like I might as well use emacs rather than “plain jEdit with its >> static ML mode” for this purpose. >> > > I did this myself until 2006 and then switched to jEdit. After 2 weeks of > unlearning ESCAPE-META-ALT-CONTROL-SHIFT I became much more productive with > the new editor. Then I set out to make a full-scale IDE based on it: 8 > years later it is there. > > > 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? >> > > As I said, the Prover IDE can load many modules of Isabelle/Pure later on, > as a second copy within the context of Pure.thy. I still wonder how > relevant this is for users of PIDE for general ML development, even for > users of Isabelle. As a user of Linux I also don't edit the kernel > sources, neither do I "hack" on it. > > Below Pure.thy several delicate bootstrap stages turn the raw ML system > into something that can then support user-space Isabelle/ML, and now also > regular Standard ML. > > > 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”). >> > > Isabelle/Pure is definitely not an SML program. I usually say "ML" in a > general sense, and "SML" in the specific sense of SML'97. > > The "largest ML program that I know of" was referring to Isabelle/HOL: it > is an application of Isabelle/ML with Pure.thy as starting point. > > > Makarius > > ------------------------------------------------------------ > ---------------- > http://stop-ttip.org 1,138,652 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
