A Visual Ltac Debugger in CoqIDE
summary
A visual Ltac debugger in CoqIDE (Coq 8.15) shows a concrete prototype: set a breakpoint on idtac, run and stop before the idtac, view call stack and local variables and use continue / step / step in / step out from the messages panel. It ports the coqtop debugger to the GUI, requires the set ltac debug option today, supports detaching the debugger for multi-file scripts, and outlines planned work for Ltac2, cbv/term-reduction tracing, history/backtracking navigation, evar breakpoints, and IDE protocol reuse.
AI-written summary · about
chapters (8)
- 0:00Intro
- 8:00Other debuggers
- 9:55Term reductions
- 11:30History
- 13:35Info Display
- 15:50existential variables
- 16:10GUI refinements
- 17:25Questions
related talks
21mLive Verification in an Interactive Proof Assistant
23mThe GHC Debugger
01h 01mDebugger: A Hidden Gem
24mA Counterexample-Guided Debugger for Non-Recursive Datalog
19mCodeTalk: Improving Programming Environment Accessibility for Visually Impaired Developers
26mIntegrating graphical proofs in Coq
01h 36mOpen source tooling with Eclipse IDE & Theia
31mLiterate Tracing