Interactive Simplifier Tracing and Debugging in Isabelle
Lars Hupel
TL;DR
This paper introduces an interactive tracing and debugging tool for Isabelle's simplifier, enhancing user insight and control over the proof simplification process within the Isabelle/jEdit IDE.
Contribution
It presents a novel interactive tracing facility with filtering, memoization, and search features integrated into Isabelle's IDE, improving proof simplification transparency.
Findings
Enhanced understanding of simplification steps
Improved debugging capabilities for proof development
Seamless integration into Isabelle/jEdit IDE
Abstract
The Isabelle proof assistant comes equipped with a very powerful tactic for term simplification. While tremendously useful, the results of simplifying a term do not always match the user's expectation: sometimes, the resulting term is not in the form the user expected, or the simplifier fails to apply a rule. We describe a new, interactive tracing facility which offers insight into the hierarchical structure of the simplification with user-defined filtering, memoization and search. The new simplifier trace is integrated into the Isabelle/jEdit Prover IDE.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.