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