Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Announcement] An unofficial REPL server for I...

Email Gateway (Nov 12 2024 at 14:42):

From: Qiyuan XU ????? <cl-isabelle-users@lists.cam.ac.uk>
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 exposed to AI agents (join the discussion from GitHub<https://github.com/xqyww123/Isa-Proof-Shell> or Zulip thread<https://isabelle.zulipchat.com/#narrow/channel/202967-New-Members-.26-Projects/topic/A.20proof.20shell.20designed.20for.20machine.20learning>).

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.

CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.

Last updated: Jan 04 2025 at 20:18 UTC