Omar, I recently installed ProofPower <http://www.lemma-one.com/ProofPower/index/index.html>and discovered that it has capabilities as an efficient and effective PolyML IDE too! It also uses a simplified variation of Knuth's "literate programming" idea where you can intersperse mathematics with the correct symbols (rather than ASCII code approximations). In an earlier post, I had mistakenly claimed that ProofPower required an earilier version of PolyML (v 4), but Rob Arthan helped me through the very minor update to a makefile to get it to build easily using the latest PolyML version, so that is not a problem. I have attached a small sample to show how the integration works with math using a few macros in the source code. The source (in the doc file) was entered using the xpp "IDE" which allows you to run the SML code right in the editor. -Dave Topham
> 2. Re: [isabelle] Isabelle as an SML environment and IDE > (Omar Montano Rivas) > > ------------------------------ > Date: Mon, 22 Dec 2014 11:50:28 -0600 > From: Omar Montano Rivas <[email protected]> > To: Aleks Kissinger <[email protected]> > Cc: [email protected], Poly/ML Mailing List > <[email protected]> > Subject: Re: [isabelle] Isabelle as an SML environment and IDE > > Really useful. Thanks for sharing. > > Best, > Omar. > > 2014-12-19 10:49 GMT-06:00 Aleks Kissinger <[email protected]>: > > > It recently came up on the Poly/ML mailing list that Isabelle/jEdit > > makes a pretty efficient SML IDE these days. I manage a fairly large > > SML project called Quantomatic, so I thought I'd have a go at getting > > a setup to work. I've got a setup now that I am pretty happy with, so > > I thought I'd share my results. Hopefully other people will find this > > helpful. > > > > Quantomatic is fairly unique in that it is designed to run inside of > > Isabelle or as a standalone project. As a result, the whole codebase > > is implemented on top of an Isabelle/ML-like environment, obtained by > > importing chunks of the ML code in Pure. This can be done by copying > > src/Pure from Isabelle 2014 into an SML project and using this file: > > > > > > > https://github.com/Quantomatic/quantomatic/blob/integration/core/isabelle_env.ML > > > > In the past, we used a slightly hacked-up version of Pure, but for the > > sake of maintainability, we now use an exact copy. > > > > The project itself is loaded with special "thy" files that only > > contain comments and "ML_file" commands. These can be run from inside > > Isabelle/jEdit (in the "real" Isabelle/ML environment), or they can be > > imported in poly/ML with the function "use_thy": > > > > > https://github.com/Quantomatic/quantomatic/blob/integration/core/use_thy.ML > > > > This implements a baby version of the outer syntax parser, which > > ignores imports and translates the ML_file commands into use > > statements. This makes the external ROOT.ML tiny and easy to maintain: > > > > https://github.com/Quantomatic/quantomatic/blob/integration/core/ROOT.ML > > > > This can be executed with, e.g. "poly --use ROOT.ML" > > > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lists.inf.ed.ac.uk/pipermail/polyml/attachments/20141222/a0665ed1/attachment-0001.html > > > > >
higherOrder.pdf
Description: Adobe PDF document
higherOrder.doc
Description: MS-Word document
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
