Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Discontinue isabelle process -T / use_thy

Email Gateway (Oct 21 2025 at 19:47):

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

• The command-line tool "isabelle process" no longer supports option -T
  to load individual theories via the "use_thy" function in Isabelle/ML.
  The latter is still available as "Thy_Info.use_thy_legacy", notably for
  "isabelle process -e ...", but it will be removed eventually. The proper
  way to process individual theories under program control is via
  "isabelle process_theories". INCOMPATIBILITY.

This refers to Isabelle/7505b5e592b1.

It needs to be understood in the context of the new "isabelle
process_theories", which is adjacent in the NEWS and provides a proper
Isabelle/Scala context for the Isabelle/ML process.

At some point after the Isabelle2025-1 release, I will revisit the remaining
Thy_Info.use_theories, which is the ML entry point for "isabelle build".
Without the assumption of being a sequential ML toplevel operation, it can be
done more efficiently, e.g. commit presentation hooks when a theory is
finished, and delete its intermediate states on the spot (instead of at the
end of the build 'theories' section).

Makarius

Last updated: Nov 05 2025 at 08:30 UTC