David, On 15 Dec 2014, at 19:44, David Topham <[email protected]> wrote: > ... > I also found a reasonably current project using PolyML and Motif here: > http://www.lemma-one.com/ProofPower/index/ > > ...however it was built on PolyML 4 and has not yet been ported to the newer > version (e.g. depends on PolyML.commit which no longer seems to be supported).
Thanks for the plug. ProofPower does run on the latest versions of Poly/ML - it uses the SaveState structure (http://www.polyml.org/docs/SaveState.html) as a replacement for PolyML.commit. This is a way of working which I strongly recommend to anyone who wants a persistent object store for Standard ML that lets you store (at least modest amounts of) data and code in a type-safe way. Could you let me know off-line what gave you the impression that ProofPower did not run on recent versions of Poly/ML. As regards Motif, ProofPower comes with its own Motif-based GUI called xpp for editing scripts and executing Standard ML code interactively via its own variant of the Standard ML Read-Eval-Print-Loop. xpp is written in C and not ML. It was something I knocked up in the early 1990s and has lived a life of its own ever since (including heavy use by the Vietnamese contributors to the Flyspeck project, who apparently used it as a front-end to HOL Light). I have long wanted to replace it by something closer to the mainstream of the IDE world or at least editing world, but that still hasn’t happened. PPDaz, one of the ProofPower packages does include a tool written in ML using the Poly/ML Motif bindings, but this was experimental and has not been actively supported for some years. > > Happy Holidays to everyone in the PolyML community! > And Season’s Greetings to you! Rob.
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
