Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Isabelle_System.ML_process vs. "isabelle ML_process"

Email Gateway (Nov 19 2025 at 21:00):

From: Makarius <makarius@sketis.net>
* ML *

• Isabelle_System.ML_process and ML_Process.args allow to run an
  external ML process directly via the current Isabelle/Scala context,
  without running another bulky Java process of "isabelle ML_process" on
  the command-line.

* System *

• The former command-line tool "isabelle process" has been renamed to
  "isabelle ML_process", with new options -C DIR and -r (redirect). The
  old option option -T to load individual theories via the Isabelle/ML
  "use_thy" function has been removed. It is still possible to use
  "Thy_Info.use_thy_legacy" together with "isabelle ML_process -e ...",
  but that low-level entry to the theory loader will be removed at a later
  stage. The proper way to process individual theories under program
  control is via "isabelle process_theories". INCOMPATIBILITY.

This refers to Isabelle/baf75b1bf14a.

It is a clarification of ancient terminology and concepts. Many decades ago,
an "Isabelle process" was indeed the Poly/ML runtime system with our modest
Pure/ROOT.ML or HOL/ROOT.ML pre-loaded. In the past 10 years, the "Isabelle
system process" has become a Java Virtual Machine running the bulky
isabelle.jar (11 MiB of JVM byte code). That Isabelle system process can start
any number of Isabelle/ML processes, using operations from the Scala modules
isabelle.ML_Process and isabelle.Bash. Isabelle/ML programs can now directly
invoke that as well, e.g. to run a generated SML program via Isabelle/HOL codegen.

So ML-to-ML_process now goes via the already running Scala process, and not
ML-to-Bash.Server-to-java_process-to-ML_process.

To see the wiring, it might help to use the Prover IDE:

isabelle jedit -l Pure ~/Scratch.thy src/Pure/ROOT.ML

and then explore this source snippet via C-hover-click:

theory Scratch
imports Pure
begin

ML ‹
Isabelle_System.ML_process;
\<^scala_function>‹ML_process›;
›

end

We don't have a proper Isabelle/Scala IDE yet: One happy day it will be part
of the regular Isabelle/PIDE setup -- not the somewhat lacking IntelliJ IDEA
Scala plugin.

Makarius

Last updated: Dec 10 2025 at 12:50 UTC