On Thu, 2 Oct 2014, Tjark Weber wrote:
- 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-o... and the green tick has changed as well :-)
- 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.
- 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.
- 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
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-o... 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
On Fri, Oct 3, 2014 at 3:15 PM, Tjark Weber <tjark.weber at 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.
On Fri, 2014-10-03 at 15:32 +0100, Ramana Kumar wrote:
On Fri, Oct 3, 2014 at 3:15 PM, Tjark Weber <tjark.weber at 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
On Fri, 3 Oct 2014, Tjark Weber wrote:
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."
In the wild times before the rather strict SML standards, both "use" and "print" where commonly available -- something every LISP programmer would expect anyway. Note that it was actually
print: 'a -> unit
and not the boring
TextIO.print: 'a -> unit
that we have today.
David Matthews has cultivated quite nice non-standard facilities both for "use" (or "eval") and "print" / "makestring" / "pretty" for arbitrary values. All this is available in Isabelle/ML, but the SML IDE uses strict SML'97 and spoils this game.
Printing values in the notation of the compiler is a bit impolite for proper programs anyway. It is mainly for experimentation and debugging. Proper integration of the Poly/ML debugger into the IDE might circumvent this potential limitation, but it is more work that is still to do.
Right now it is possible to use SML_import to pick useful add-ons from the Isabelle/ML environment and use them in SML, as well. See also $ISABELLE_HOME/src/Tools/SML/Examples.thy
Makarius
-
makarius＠sketis.net -
Ramana.Kumar＠cl.cam.ac.uk -
tjark.weber＠it.uu.se