5
$\begingroup$

Is there a recommended implementation of Standard ML to use for Isabelle?

Note: An answer should strive to include why that implementation (noted in build instructions is acceptable). While not needed for the accept, if the recommended implementation changed over time.


The Wikipedia page for Isabelle notes

Written in Standard ML and Scala

The Wikipedia page for Standard ML notes

Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.

The Wikipedia article also notes

Major implementations - SML/NJ, MLton

and several other Implementations

About a decade ago when I used ML I would choose SML/NJ, it didn't leave me out on a limb.

$\endgroup$
7
  • 2
    $\begingroup$ Definitely the one bundled with Isabelle, as per the second paragraph of my (now in way to oblivion) answer here. $\endgroup$ Feb 17, 2022 at 20:56
  • $\begingroup$ I don't think there's much choice, tbh. Isabelle comes as a very integrated package, I've never tried to build it on a different ML compiler and would guess that things would likely go wrong if one tried. $\endgroup$
    – Josh
    Feb 17, 2022 at 20:59
  • $\begingroup$ I'm also curious exactly which parts of it are written in Scala and how the Scala-SML interface works in Isabelle ... for one thing I'm curious why the SML implementation used in Isabelle doesn't need to target the JVM. $\endgroup$ Feb 17, 2022 at 20:59
  • $\begingroup$ I can't promise anything. I'm very excited about the site, which drives my writing some responses. But I prefer to see if other enthusiasts have a say and then supplement their answers, either by suggestions or, if that isn't enough, an alternative answer. Thanks anyway for the invitation! $\endgroup$ Feb 17, 2022 at 21:05
  • 2
    $\begingroup$ Re: view $\implies$ upvote: I foresee a steady grow, like Kevin Buzzard does for the use of Lean (and PAs) in maths. For Isabelle, the main knowledge base is distributed in two mailing lists, and there are lots of know-how there. Turning that into a SE format could be extremely useful for the community $\endgroup$ Feb 17, 2022 at 21:10

2 Answers 2

4
$\begingroup$

I wondered about the same question before. Based on this blog, it seems that the only supported SML implementation now is Poly/ML.

17-Feb-2016 marks the historic day when support for SML/NJ was removed from the Isabelle code base, ...

In the future, we will be able to proceed faster in just one direction, and pick up more advanced features of Poly/ML.

The author went on to discuss heap/memory/performance issues associated with SML/NJ and in this CS.SE question.

$\endgroup$
4
  • $\begingroup$ @GuyCoder Yes, I did:). I wondered about the same question, and had hoped that Isabelle would be portable among multiple implementations. $\endgroup$
    – tinlyx
    Feb 17, 2022 at 22:32
  • $\begingroup$ @GuyCoder Thanks. It's indeed a copy-paste error. $\endgroup$
    – tinlyx
    Feb 17, 2022 at 22:35
  • $\begingroup$ @GuyCoder Sure. np $\endgroup$
    – tinlyx
    Feb 17, 2022 at 22:38
  • $\begingroup$ @GuyCoder Thanks for sharing. It's interesting stuff. $\endgroup$
    – tinlyx
    Feb 17, 2022 at 22:48
7
$\begingroup$

Historically, we always tried to ensure that Isabelle would run on both Poly/ML and SML/NJ. It's a curious fact that Poly/ML always greatly outperformed SML/NJ even though the latter seemed much faster on small benchmarks. I never got to the root of the problem but always suspected it lay in garbage collection. And the greater and greater emphasis on multithreading, which was not supported in SML/NJ, made the difference more extreme. Eventually the disparity in performance meant that SML/NJ could no longer be seen as a viable option.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.