Gergely Buday (Aug 27 2026 at 11:34): Gergely Buday (Aug 27 2026 at 11:34):I am to see an Isabelle extension in action.
In $ISABELLE_HOME/etc/options, I have set
public option ML_debugger : bool = true
I have rebuilt HOL:
isabelle build -f -b HOL
I opened my theory file containing the Isabelle/ML parts, and the theory file containing the use of the extension, in the same Isabelle/jEdit window. Still when I set a breakpoint, fiddle with the extension using theory, point the cursor where the new construct is, trying to run the Debugger with Continue to the breakpoint, nothing happens.
What else do I need to run the Debugger properly in this setting?
Last updated: Sep 15 2026 at 09:19 UTC