Email Gateway (Aug 28 2026 at 10:46): Email Gateway (Aug 28 2026 at 10:46):From: balazs.toth@lmu.de
Subject: [isabelle] Hooks that nudge LLM coding agents toward sledgehammer
Hi all,
Coding agents (Claude Code, Codex, OpenCode) often don't want to run
sledgehammer: they'd rather guess |by (metis foo bar)|, fail, and guess
again. They also like falling back to long |apply| scripts.
I wrote a hook that forces them, to a certain degree, to do it properly:
https://github.com/balazstothofficial/isabelle-agent-hooks
It sits in front of every |.thy| write. A closer that sledgehammer or
try0 could have found only goes through if a real search result shows up
in the agent's transcript, and |apply| steps get bounced with a pointer
to Isar. With that in place, agents fall into a decent workflow on their
own: Isar skeleton with |sorry|s, then one search per closer.
It is compatible with the I/Q (AutoCorrode) and isabelle-pide-mcp servers.
I've used it with Isabelle2025-2 and the development version together
with I/Q since July and for me it works very well.
Feedback is very welcome, especially if it blocks something it shouldn't.
Best,
Balazs
Email Gateway (Aug 28 2026 at 11:39):From: Makarius <makarius@sketis.net>
Subject: [isabelle] Hooks that nudge LLM coding agents toward sledgehammer
On 28/08/2026 12:45, balazs.toth@lmu.de wrote:
I am not going to look at it before the final release of Isabelle2026.
It sits in front of every |.thy| write.
This is not a proper concept of Isabelle/PIDE. In fact, it works via its own
internal file-system (better called document model).
AI agents are wrong in changing files "on disk". (Or the makers of these agents).
Makarius
Email Gateway (Aug 28 2026 at 13:39):From: balazs.toth@lmu.de
Subject: [isabelle] Hooks that nudge LLM coding agents toward sledgehammer
On 28.08.26 13:37, Makarius wrote:
On 28/08/2026 12:45, balazs.toth@lmu.de wrote:
I am not going to look at it before the final release of Isabelle2026.
It is not meant as an addition to the Isabelle distribution or anything.
It is just a small tool that can be configured for coding agents.
It just prevents coding agents to do certain tools calls, e.g. through
MCP servers.
It sits in front of every |.thy| write.
The only thing I meant with that, is that the hook is active if a tool
call from a coding agent targets a .thy file.This is not a proper concept of Isabelle/PIDE. In fact, it works via
its own internal file-system (better called document model).AI agents are wrong in changing files "on disk". (Or the makers of
these agents).Makarius
Last updated: Sep 02 2026 at 16:10 UTC