Python client for Isabelle server
isabelle-client is a TCP client for Isabelle server. For more information about the server see Chapter 4 of the Isabelle system manual.
How to Install
The best way to install this package is to use pip:
pip install isabelle-clientAnother option is to use Anaconda:
conda install -c conda-forge isabelle-clientOne can also download and run the client together with Isabelle in a Docker container:
docker build -t isabelle-client https://github.com/inpefess/isabelle-client.git
docker run -d --rm -p 8888:8888 --name isabelle-client isabelle-clientAnd navigate to example page in your browser.
How to use
from isabelle_client import get_isabelle_client, start_isabelle_server
# start Isabelle server
server_info, _ = start_isabelle_server()
# create a client object
isabelle = get_isabelle_client(server_info)
# start a new session
responses = isabelle.session_start()
session_id = responses[-1].response_body.session_id
# send a theory file from the current directory to the server
responses = isabelle.use_theories(
theories=["Example"], master_dir=".", session_id=session_id
)
# shut the server down
isabelle.shutdown()For more details, follow the usage example from documentation or a notebook.
High-level connector
You can also pass a theory file body (something you typically put between begin and end keywords) to a high-level connector that will generate a temporary file for you, send it to the Isabelle server and get the result for you. For example, this snippet:
from isabelle_client.isabelle_connector import IsabelleConnector
from isabelle_client.isabelle_connector import IsabelleTheoryError
isabelle_connector = IsabelleConnector()
try:
isabelle_connector.build_theory(
r'lemma "\<forall> x. \<forall> y. x = y"' "\nby auto"
)
print("Theory is validated!")
except IsabelleTheoryError as error:
print(error.args[0])will produce something like:
: Failed to finish proof\<^here>:
: goal (1 subgoal):
: 1. \<And>x y. x = yMore documentation
More documentation can be found here.
Similar Software
There are Python clients to other interactive theorem provers, for example:
Modules helping to interact with Isabelle server from Python are parts of the Proving for Fun project.
There are also clients to Isabelle server in other programming languages, e.g. this one in Rust.
Projects using the client
isabelle-client helped to build some cool LLM stuff (in reversed chronological order):
Decompose-and-Formalise: Recursively Verifiable Natural Language Inference (Quan et al.)
Inferring Latent Intentions: Attributional Natural Language Inference in LLM Agents (Quan et al.)
StepProof: Step-by-step verification of natural language mathematical proofs (Hu et al.) with code
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement (Hu et al.)
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving (Quan et al., EMNLP 2024) with code
How to cite
If you’re writing a research paper, you can cite the Isabelle client using the following DOI. You can also cite Isabelle 2021 (and an earlier version of the client) with this DOI. There also is a somewhat more complete (but unpublished) pre-print.
How to Contribute
Please follow the contribution guide while adhering to the code of conduct.
1 maintainer
Release files for isabelle-client 1.1.2
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| isabelle_client-1.1.2.tar.gz | 20.7 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| isabelle_client-1.1.2-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 51.3 kB
Release files / isabelle_client-1.1.2.tar.gz
| Download URL | isabelle_client-1.1.2.tar.gz |
|---|---|
| Size | 20.7 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
1d8e2694f189eb8df315fb0acae7c41bdf9e9fae8fa02ed14e388babb01896c8
|
|
BLAKE2b-256 checksum How to use checksums |
081f13c1396a6ef77110daabe7fcae31948c6bba3bb5e5e4acedbcbbf80bdb97
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.11.15 {"installer":{"name":"uv","version":"0.11.15","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"Ubuntu","version":"26.04","id":"resolute","libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}
|
Release files / isabelle_client-1.1.2-py3-none-any.whl
| Download URL | isabelle_client-1.1.2-py3-none-any.whl |
|---|---|
| Size | 30.6 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
4e99604205010a7029b6e0dde4101fd2ca5e972a1492c705669e0efe8f76ecc5
|
|
BLAKE2b-256 checksum How to use checksums |
bafd9f5403628f58d39c27e2080af8c66f9ea3561ab72814b8a3f9131b16973d
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
uv/0.11.15 {"installer":{"name":"uv","version":"0.11.15","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"Ubuntu","version":"26.04","id":"resolute","libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}
|
