# Preview of Ltac2 Visual Debugger is now available

**URL:** <https://discourse.rocq-prover.org/t/preview-of-ltac2-visual-debugger-is-now-available/2480>\
**Category:** Announcements\
**Created:** [December 2, 2024, 9:30pm UTC](https://discourse.rocq-prover.org/t/preview-of-ltac2-visual-debugger-is-now-available/2480 "2024-12-02T21:30:16Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![jfehrle](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jfehrle/32/112_2.png) [@jfehrle](https://discourse.rocq-prover.org/u/jfehrle)\
**Post date:** [December 2, 2024, 9:30pm UTC](https://discourse.rocq-prover.org/t/preview-of-ltac2-visual-debugger-is-now-available/2480/1 "2024-12-02T21:30:17Z")

</div>

Coq Platform now includes a preview of the Ltac/Ltac2 debugger running on Coq 8.19. Diffs for the updated documentation are [here](https://github.com/coq/coq/pull/19397/files#diff-feb466e338cd549a97f541a20ebb2aef27f68752824f1772efc1b38bd8e45cfb). 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 select 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](https://github.com/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](https://coq.zulipchat.com/) (Jim Fehrle) or by email at jim dot fehrle at gmail dot com.