Coq Platform now includes a preview of the Ltac/Ltac2 debugger running on Coq 8.19. Diffs for the updated documentation are here. Let me know your suggestions for it and whether you find it useful.
The main improvements are:
- Ltac2 support, with a combined call stack for proofs that use both Ltac2 and Ltac
- A history mechanism that allows stepping backward to view previous states
- Proof diffs display while in the debugger
- You can change CoqIDE display settings while in the debugger
- You can which subgoal is fully displayed while in the debugger
- The debugger catches exceptions, permitting examination of the history
To install the preview, clone Coq Platform on your system, run coq_platform_make.sh and select option 9 (Coq 8.19.2+ltac2-debugger).
It shouldn’t have taken 3 years to get this new version out. About 2/3 of that time is due to delays beyond my control. Once this version is merged I will look at supporting the debugger in vsCoq2.
You can reach me on Zulip (Jim Fehrle) or by email at jim dot fehrle at gmail dot com.