5
$\begingroup$

My question is based on this question, which asks about swapping out different SML implementations when building Isabelle.

I've read on Wikipedia that Isaballe is written in Scala and SML.

Based on casually browsing the Isabelle GitHub mirror, we can see some files written in Scala and some files written in SML.

I know that SML has at least one implementation that targets the JVM, but Poly/ML, the implementation of SML chosen for Isabelle, doesn't seem to be able to do this.

Scala also has a native code compiler (in addition to the better known JVM bytecode compiler), so there are quite a few ways that the language boundary could work.

  • Does Isabelle use the JVM backend for Scala?
  • What does the boundary between the Scala parts of the code and the SML parts of the code look like in Isabelle? (Is there some kind of Foreign Function Interface, for example?)
  • Is there an easy way to describe the areas that code written in Scala is responsible for vs SML?
$\endgroup$
0

1 Answer 1

4
$\begingroup$

Scala appears to use the JVM, and this has been marketed as a feature, not a bug.

According to Isabelle/Scala:

  • Isabelle/ML is for ‹mathematics›, to develop tools within the context of symbolic logic, e.g. for constructing proofs or defining domain-specific formal languages. See the ‹Isabelle/Isar implementation manual› for more details.
  • Isabelle/Scala is for ‹physics›, to connect with the world of systems and services, including editors and IDE frameworks.

This probably coincides with the use of jEdit as the editor-of-choice for Isabelle.

$\endgroup$
4
  • $\begingroup$ I didn't mean to imply that Scala primarily targets native code; just that it has a native code compiler in addition to a JVM backend (and I think a JavaScript backend too). $\endgroup$ Feb 18, 2022 at 0:01
  • 1
    $\begingroup$ @GregoryNisbet I added a link to some slides where the goals were laid out; the hope was to leverage the JVM interoperating with the ML native generated code. I, uh, don't share Isabelle's enthusiasm for JVM, but they wanted to use it for front-end stuff. $\endgroup$ Feb 18, 2022 at 0:05
  • $\begingroup$ @AlexNelson Interesting. Thanks for the link; based on the last slide it almost sounds like they're deprecating Proof General as a frontend long term? $\endgroup$ Feb 18, 2022 at 0:09
  • $\begingroup$ @GregoryNisbet Yeah, though there's a (small-ish?) group of Isabelle users who still use Emacs; see, e.g., this question on Stackoverflow. $\endgroup$ Feb 18, 2022 at 0:11

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.