Re: [polyml] Isabelle/ML IDE (update)
On Thu, 2014-10-02 at 23:19 +0200, Makarius wrote: We also need to find out how many people are still there to use SML. So far there are already 9 supporters on http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux-or-mac and the green tick has changed as well :-) FWIW, I am teaching a Functional Programming course with approx. 50 students annually at Master's level. Unfortunate (like fix) is a word of this odd street language that has emerged in recent years and is better ignored. The enclosing theory file is like a project file, but with slightly odd syntax for that purpose, although not too bad compared to the traditional use script. I agree that the syntax could be less odd. Still, no syntax at all would be even better IMHO, and seems within reach for trivial (single-file) projects. Further note that print is also not Standard ML, although TextIO.print is covered by the Basis Library. In what sense is print not Standard ML? David Matthews might be able to tell what happens with * (or +). I know myself from Isabelle/Pure bootstrapping, that formal references to very basic things are sometimes surprising, by construction of the initial environment. It may be that Poly/ML already returns the most sensible reference, but that the IDE could treat this case specially to indicate more clearly that the declaration is not actually available. Anyway, this is just a very minor UI issue. Best, Tjark ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Isabelle/ML IDE (update)
On Fri, Oct 3, 2014 at 3:15 PM, Tjark Weber tjark.we...@it.uu.se wrote: Further note that print is also not Standard ML, although TextIO.print is covered by the Basis Library. In what sense is print not Standard ML? In the same way use is not Standard ML (although as Makarius points out, at least print is in the Basis). They're not in the definition. http://sml-family.org is worth a look. ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Isabelle/ML IDE (update)
On Fri, 2014-10-03 at 15:32 +0100, Ramana Kumar wrote: On Fri, Oct 3, 2014 at 3:15 PM, Tjark Weber tjark.we...@it.uu.se wrote: Further note that print is also not Standard ML, although TextIO.print is covered by the Basis Library. In what sense is print not Standard ML? In the same way use is not Standard ML (although as Makarius points out, at least print is in the Basis). They're not in the definition. In this sense, very little is in the Definition. In SML'97, the initial basis intentionally has been cut down to a bare minimum [SML'97, section G.19]. At the same time, the SML Basis Library demands that [r]equired components must be provided by all SML implementations. Note that use and print have different status in the Basis Library, which explicitly states that [i]mplementations are not required to supply a use function. http://sml-family.org is worth a look. Definitely. Best, Tjark ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Isabelle/ML IDE (update)
On Thu, 2 Oct 2014, Tjark Weber wrote: 1. I suspect that the ITP aspect of Isabelle may put off people who just want to write SML code. (For instance, there are many documents and panels visible in the UI that are entirely irrelevant to SML programming.) If you had unlimited time, I would suggest that the SML IDE be released separately from Isabelle. This is only the first release of the SML PIDE, but I have started thinking about these questions before. It is probably mainly a matter to re-package the system such that it looks more like an SML IDE outright. Many things are possible, but it also requires some work. Does anybody has smart ideas to find some funding for such projects? It might be also interesting for David Matthews himself, to provide even more IDE support at the bottom, e.g. inclusion of the debugger. We also need to find out how many people are still there to use SML. So far there are already 9 supporters on http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux-or-mac and the green tick has changed as well :-) 2. The need to have a theory file (no matter how simple) is slightly unfortunate. Would an Isabelle/jEdit option -sml (or similar) be feasible to make the enclosing theory redundant, at least for single-file SML projects? Unfortunate (like fix) is a word of this odd street language that has emerged in recent years and is better ignored. The enclosing theory file is like a project file, but with slightly odd syntax for that purpose, although not too bad compared to the traditional use script. There might be other ways emerging to assemble ML files; or maybe just some IDE support to generate such templates. There was also a private discussion with Larry Paulson, to re-use the model of the SML/NJ compilation management, whatever that might be exactly -- we still need to find out. 3. I noticed that use is not available, and that print doesn't affect the output panel. A document that summarizes such differences (and explains, e.g., how to perform I/O instead) might be useful. Note that use is not part of Standard ML. This touches again the question how SML projects are actually managed. For the IDE to work, the control over the ML files needs to be given to the IDE, not the ML program. Further note that print is also not Standard ML, although TextIO.print is covered by the Basis Library. That raw stateful output is in conflict with the stateless model of PIDE, but it works as specified: via stdout, which is shown in PIDE in the Raw Output panel. In contrast, the Documentation panel includes src/Tools/SML/Examples.thy with some examples to re-use stateless Isabelle output in SML. 4. Ctrl+click on certain built-in operators, such as *, takes me to an empty buffer called Standard Basis. Surely some explanatory message could be displayed in the buffer. This information is produced by Poly/ML at the very bottom. E.g. the length function refers to $ML_SOURCE/basis/List.sml as expected. David Matthews might be able to tell what happens with * (or +). I know myself from Isabelle/Pure bootstrapping, that formal references to very basic things are sometimes surprising, by construction of the initial environment. Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
[polyml] Isabelle/ML IDE (update)
Dear friends of Standard ML. This is an update on the Standard ML facilities of the recent release of Isabelle2014 (August 2014). Compared to Isabelle2013-2 (December 2013), the Prover IDE based on Isabelle/jEdit has been greatly improved. IDE support for both Isabelle/ML and official Standard ML (SML'97) allows direct editing of programs that are assembled from separate ML files. The enclosing theory merely serves as some kind of project file. See the Documentation/Examples panel in Isabelle/jEdit (bottom of the list). Isabelle2014 is available from the usual mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ If we've had such IDE support on all major platforms 10 or 20 years ago, SML might be a bit more popular today. For example, a web search of SML IDE yields the following slightly odd page: http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux It mostly refers to some editors with plain and basic syntax highlighting, not really IDEs. Maybe some enthusiasts of Poly/ML and Isabelle/PIDE can help to vote up my (updated) answer on the SML IDE in Isabelle2014. Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
