Stream: Mirror: Isabelle Development Mailing List

Topic: Thy_Info.use_thy_legacy removed

Email Gateway (Jan 14 2026 at 20:35):

From: Makarius <makarius@sketis.net>

* ML *

• Obsolete Thy_Info.use_thy_legacy has been removed. Rare
  INCOMPATIBILITY: need to use formal PIDE session to load theories, e.g.
  via "isabelle build" or "isabelle process_theories".

This refers to Isabelle/955f8ac18136.

The Isabelle2025-1 release already had this NEWS entry:

• 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.

So that's finally it: no "use_thy" anymore. It was the central Isabelle/ML
operation since 1992, and already present in changeset 0 (Sep-1993):
https://isabelle.in.tum.de/repos/isabelle/file/a5a9c433f639/src/Pure/Thy/read.ML

The implementation behind it has changed many times since then, but now we
have better ways to communicate between Isabelle/Scala and Isabelle/ML,
without the old toplevel loop.

Rather soon, I will revisit the protocol function "build_theories" and its
underlying ML function Thy_Info.use_theories, in order to make it more
scalable and less sequential: meaning that intermediate states are removed
earlier in the process, and heap space is released.

Makarius

Last updated: Feb 04 2026 at 02:22 UTC