Stream: Announcements

Topic: REPL

Qiyuan Xu (Nov 12 2024 at 12:03):

Hi, dear users of Isabelle,

It is exciting to announce an unofficial REPL server for Isabelle.

This tool addresses a need in the machine learning community, where people have faced challenges connecting Isabelle with ML systems. Some of my colleagues in machine learning have expressed that this integration difficulty has led them to choose other proof assistants like Lean. This REPL server aims to bridge this gap as a first step. Additionally, I am also planning an abstraction layer to simplify the complexity that exposures to AI agents (join the discussion from GitHub or Zulip thread).

Repository URL: https://github.com/xqyww123/Isa-REPL

Features

• Python client
• Tracing the proof state and the output panel for step-by-step evaluation.
  - Plugin: collecting data from Isabelle's internal representations by hot plugins written in Isabelle/ML.
• Socket based remote communication
• Socket based concurrency
• State rollback

About the implementation, I use the Toplevel.state interface in a dedicated thread separate from Isabelle workers (Task_Queue.task). This disables the concurrency between commands within a single file, allowing the REPL to sequentially evaluate every command and capture its complete output as expected. However, I dunno if it could cause any unforeseen problems. Let me know if it is bad!

The REPL server runs in the batch mode of isabelle build, in a tricky way preventing the build process from terminating and transforming it into a server. While functional, the ideal solution perhaps should be implementing the server as an Isabelle tool integrated into the isabelle command line tool. I welcome expertise and assistance from the community to help develop this integration.

Last updated: Dec 22 2024 at 08:21 UTC