Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-1-RC4: isabelle process_theories ...

Email Gateway (Dec 10 2025 at 22:27):

From: Makarius <makarius@sketis.net>

Dear Isabelle users,

people often come to me with the request to make Isabelle appear more like a
plain-old command-line proof assistant from some decades ago. Short answer: We
have given up this model > 10 years ago, and won't go back. Isabelle is a
document-oriented proof assistant instead.

And in fact, asking the canonical questions: "What is your application? What
are you trying to do?" the answer is often something like this: "I want to
inspect intermediate states of processed theories (including proofs), but not
necessarily while the engine is still running".

Here are some answers to that, from the NEWS of Isabelle2021-1:

"""
* System *

• The command-line tool "isabelle process_theories" tool takes source
  files and theories within a proper session context (like regular
  "isabelle build"). Output of prover messages works roughly like
  "isabelle build_log", while the theories are being processed.

Examples:

isabelle process_theories -U -O HOL-Library.Multiset

isabelle process_theories -U -O -o show_states HOL-Library.Multiset

isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'

• System option "record_theories" tells "isabelle build" to record
  intermediate theory commands and results, at the cost of approx. 5 times
  larger ML heap images. This allows to retrieve fine-grained semantic
  information later on, using Thy_Info.get_theory_segments or
  Thy_Info.get_theory_elements in Isabelle/ML.
  """

That status-quo will be the starting point for any further discussions about
this topic (private or public).

I do want to see Isabelle system tools eventually that work properly ---
with the system and not against it. My claim is that it can be done with a
little bit Isabelle/Scala, and maybe some tiny Isabelle/ML addons that are
loaded beforehand in a proper session context.

Note that in the Isabelle System manual ("isabelle doc system") there is some
explanation on "isabelle scala_project", to use Java/Scala IDEs like IntelliJ
IDEA with Isabelle/Scala. There is also our src/Tools/Demo/ for the
Isabelle/Scala project setup via etc/build.props --- it is easier and more
robust than Maven / Gradle / sbt from the Java/Scala world.

Further note that in Isabelle2025-1, the terminology "Isabelle Process" means
"Isabelle/Scala process running on the JVM" by default, and the old notion of
"Isabelle/ML process running on Poly/ML" is explicitly called "ML_Process"
(which is a module in Isabelle/Scala and Isabelle/ML). That has a command-line
interface "isabelle ML_process", although it is rarely useful, because it lack
the mandatory Isabelle/Scala/PIDE session context.

Makarius

Last updated: Dec 21 2025 at 20:24 UTC