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.
András Salamon (Aug 21 2026 at 23:20):To install: pip install isabelle-query
Last updated: Aug 26 2026 at 08:45 UTC