Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interactive Isabelle session with remote prover

view this post on Zulip Email Gateway (Feb 18 2026 at 12:18):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>

Hi,

This relates to "Isabelle/jEdit: Remote continuous proof checking" https://lists.cam.ac.uk/sympa/msg/cl-isabelle-users/2023-08/jCqSPiupwo2LeIqr-MJZTQ from 03 Aug 2023.

We added to AutoCorrode a proxy script "I/P" (https://github.com/awslabs/AutoCorrode/tree/main/ip) which allows users to run an interactive Isabelle/jEdit+Scala session locally, while offloading the Isabelle/ML prover to a remote machine.

When working with very large code bases, this allows us and AI agents to work on multiple copies of the code-base at once without being limited by the resource constraints of the local machine.

We share in the hope it proves useful for the community. We'd love feedback on how to make the approach more robust -- it's still a prototype and pretty hacky in places.

Since I/P works at the PIDE level, it is compatible with other tooling operating at the Scala level, like our MCP interface I/Q or Isabelle Assistant that Dominic posted about earlier this week.

Regards,
Hanno

view this post on Zulip Email Gateway (Feb 18 2026 at 12:33):

From: Makarius <makarius@sketis.net>

On 18/02/2026 13:17, "Becker, Hanno" (via cl-isabelle-users Mailing List) >

We added to AutoCorrode a proxy script "I/P" (https://github.com/awslabs/
AutoCorrode/tree/main/ip <https://github.com/awslabs/AutoCorrode/tree/main/
ip>) which allows users to run an interactive Isabelle/jEdit+Scala session
locally, while offloading the Isabelle/ML prover to a remote machine.

I don't have time to look at it now. My main job in the past decades has been
to get contributions into proper form for long term usage.

Since I/P works at the PIDE level, it is compatible with other tooling
operating at the Scala level, like our MCP interface I/Q or Isabelle Assistant
that Dominic posted about earlier this week.

Important note on proper terminology: Isabelle does not have any "levels". The
canonical naming scheme is Isabelle/XYZ for almost anything. For example,
Isabelle/PIDE, Isabelle/Scala, Isabelle/ML etc.

Gettings words right is important to understand underlying concepts.

Makarius

Last updated: Feb 22 2026 at 05:16 UTC