announcement: isabelle-query · New Members & Projects

Stream: New Members & Projects

Topic: announcement: isabelle-query

András Salamon (Aug 21 2026 at 23:20):

To install: pip install isabelle-query

David Wang (Aug 29 2026 at 13:14):

Claude really likes this tool and I thought it would be useful as a base for some IDE-like features for jEdit, so I told Claude to rewrite it in Scala as an isabelle component. A benefit is that it's faster now. https://github.com/david-wang-0/isabelle-query

Pros:

jEdit dockable and right click for some IDE features like find usages
Find code equations and instantiations (of locales/classes)
Uses canonical parser from isabelle distribution

Cons:

Did not review the code yet
Performance needs a running JVM, which is why there is still a Python client that queries a server that's started on the first invocation. isabelle query (no server) -> python3 client -> isabelle query (server)

Table by Claude:

	Python `query`	JVM tool, cold	thin client (a plain `isabelle query`)
`show` on a 2-theory AFP entry	73 ms	1091 ms	33 ms
`callers` on a 28-theory entry	290 ms	1441 ms	112 ms
`summary` on `src/HOL` (1451 theories)	4865 ms	4197 ms	64 ms
`summary --by-session` over the whole AFP	37.5 s	19.5 s	0.27 s

András Salamon (Aug 29 2026 at 15:51):

This is good news! I've added a link to David's Scala port in the README of the current version of the Python isabelle-query.

David Wang (Aug 30 2026 at 11:11):

The JVM startup is not the only reason the server is faster. It holds the entire parsed project in memory. That costs about 1.2GB for the whole AFP. A cold run with Python is still faster. Performance is not strictly better, but rather a trade off between memory and speed.

Last updated: Sep 15 2026 at 09:19 UTC