NEWS: Discontinue isabelle process -T / use_thy

Makarius makarius at sketis.net
Tue Oct 21 21:46:52 CEST 2025


*** 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



More information about the isabelle-dev mailing list