András Salamon (Jun 06 2026 at 21:31): András Salamon (Jun 06 2026 at 21:31):Now available: https://github.com/ott2/isabelle-query
isabelle-query installs a Python script to query the theories of Isabelle/Isar projects: which results are orphaned; which results call another; which theories depend on a theory of interest; the current sorry statements that appear in proofs; and (somewhat) syntax-aware text retrieval.
Claude likes to use query, especially for refactoring large projects (and also wrote it, with my guidance). query is fast enough to be usable over the complete AFP repo, but parsing is approximate: the goal was a usable exploration tool that improves over grep/awk/sed, not to replicate the full parser.
Although isabelle-query has many features also found in the Isabelle/Q MCP-based Isabelle/jEdit plugin, it aims to assist workflows that do not use jEdit. The dependence graph features are new.
Last updated: Jun 12 2026 at 11:44 UTC