|PyPI version|\ |Anaconda version|\ |CircleCI|\ |Documentation Status|\ |codecov|\ |DOI|
Python client for Isabelle server
=================================
``isabelle-client`` is a TCP client for
`Isabelle <https://isabelle.in.tum.de>`__ server. For more information
about the server see Chapter 4 of `the Isabelle system
manual <https://isabelle.in.tum.de/dist/Isabelle2025/doc/system.pdf#page=52>`__.
How to Install
==============
The best way to install this package is to use ``pip``:
.. code:: sh
pip install isabelle-client
Another option is to use Anaconda:
.. code:: sh
conda install -c conda-forge isabelle-client
One can also download and run the client together with Isabelle in a
Docker contanier:
.. code:: sh
docker build -t isabelle-client https://github.com/inpefess/isabelle-client.git
docker run -d --rm -p 8888:8888 --name isabelle-client isabelle-client
And navigate to `example page <http://localhost:8888/lab/tree/isabelle-client-examples/example.ipynb>`__
in your browser.
How to use
==========
.. code:: python
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)
# send a theory file from the current directory to the server
response = isabelle.use_theories(
theories=["Example"], master_dir=".", watchdog_timeout=0
)
# shut the server down
isabelle.shutdown()
For more details, follow the `usage example
<https://isabelle-client.readthedocs.io/en/latest/example.html>`__
from documentation or a `notebook
<https://github.com/inpefess/isabelle-client/blob/master/examples/example.ipynb>`__.
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:
.. code:: python
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:
.. code::
: Failed to finish proof\<^here>:
: goal (1 subgoal):
: 1. \<And>x y. x = y
More documentation
==================
More documentation can be found
`here <https://isabelle-client.readthedocs.io/en/latest>`__.
Similar Software
================
There are Python clients to other interactive theorem provers, for
example:
* `for Lean
<https://github.com/leanprover-community/lean-client-python>`__
* `for Coq <https://github.com/IBM/pycoq>`__
* `another one for Coq <https://github.com/ejgallego/pycoq>`__
Modules helping to inetract with Isabelle server from Python are
parts of the `Proving for Fun
<https://github.com/maxhaslbeck/proving-contest-backends>`__ project.
There are also clients to Isabelle server in other programming
languages, e.g. `this one in Rust
<https://lib.rs/crates/isabelle-client>`__.
Projects using the client
=========================
`isabelle-client` helped to build some cool LLM stuff (in reversed
chronological order):
* `StepProof: Step-by-step verification of natural language
mathematical proofs (Hu et al.)
<https://doi.org/10.48550/arXiv.2506.10558>`__ with `code
<https://github.com/r1nIGa/STEP-PROOF>`__
* `HybridProver: Augmenting Theorem Proving with LLM-Driven Proof
Synthesis and Refinement (Hu et al.)
<https://doi.org/10.48550/arXiv.2505.15740>`__
* `Verification and Refinement of Natural Language Explanations
through LLM-Symbolic Theorem Proving (Quan et al., EMNLP 2024)
<https://doi.org/10.18653/v1/2024.emnlp-main.172>`__ with `code
<https://github.com/neuro-symbolic-ai/explanation_refinement>`__
How to cite
===========
If you’re writing a research paper, you can cite the Isabelle client
using the `following DOI
<https://doi.org/10.1007/978-3-031-16681-5_24>`__. You can also cite
Isabelle 2021 (and an earlier version of the client) with `this DOI
<https://doi.org/10.1007/978-3-030-81097-9_20>`__. There also is a
somewhat more complete (but unpublished) `pre-print
<https://arxiv.org/abs/2212.11173>`__.
How to Contribute
=================
Please follow `the contribution guide <https://isabelle-client.readthedocs.io/en/latest/contributing.html>`__ while adhering to `the code of conduct <https://isabelle-client.readthedocs.io/en/latest/code-of-conduct.html>`__.
.. |PyPI version| image:: https://badge.fury.io/py/isabelle-client.svg
:target: https://badge.fury.io/py/isabelle-client
.. |Anaconda version| image:: https://anaconda.org/conda-forge/isabelle-client/badges/version.svg
:target: https://anaconda.org/conda-forge/isabelle-client
.. |CircleCI| image:: https://circleci.com/gh/inpefess/isabelle-client.svg?style=svg
:target: https://circleci.com/gh/inpefess/isabelle-client
.. |Documentation Status| image:: https://readthedocs.org/projects/isabelle-client/badge/?version=latest
:target: https://isabelle-client.readthedocs.io/en/latest/?badge=latest
.. |codecov| image:: https://codecov.io/gh/inpefess/isabelle-client/branch/master/graph/badge.svg
:target: https://codecov.io/gh/inpefess/isabelle-client
.. |DOI| image:: https://img.shields.io/badge/DOI-10.1007%2F978--3--031--16681--5__24-blue
:target: https://doi.org/10.1007/978-3-031-16681-5_24
Raw data
{
"_id": null,
"home_page": "https://github.com/inpefess/isabelle-client",
"name": "isabelle-client",
"maintainer": null,
"docs_url": null,
"requires_python": "<3.14,>=3.9.1",
"maintainer_email": null,
"keywords": "TCP client, Isabelle proof assistant, interactive theorem prover",
"author": "Boris Shminke",
"author_email": "<boris@shminke.com",
"download_url": "https://files.pythonhosted.org/packages/21/dd/c047dd223a90b8d623c290f5ef6f65abfdde3fe22474b52a1d0fda96fabe/isabelle_client-0.6.0.tar.gz",
"platform": null,
"description": "|PyPI version|\\ |Anaconda version|\\ |CircleCI|\\ |Documentation Status|\\ |codecov|\\ |DOI|\n\nPython client for Isabelle server\n=================================\n\n``isabelle-client`` is a TCP client for\n`Isabelle <https://isabelle.in.tum.de>`__ server. For more information\nabout the server see Chapter 4 of `the Isabelle system\nmanual <https://isabelle.in.tum.de/dist/Isabelle2025/doc/system.pdf#page=52>`__.\n\nHow to Install\n==============\n\nThe best way to install this package is to use ``pip``:\n\n.. code:: sh\n\n pip install isabelle-client\n\n\nAnother option is to use Anaconda:\n\n.. code:: sh\n\t \n conda install -c conda-forge isabelle-client \n\nOne can also download and run the client together with Isabelle in a\nDocker contanier:\n\n.. code:: sh\n\n docker build -t isabelle-client https://github.com/inpefess/isabelle-client.git\n docker run -d --rm -p 8888:8888 --name isabelle-client isabelle-client\n\nAnd navigate to `example page <http://localhost:8888/lab/tree/isabelle-client-examples/example.ipynb>`__\nin your browser.\n\nHow to use\n==========\n\n.. code:: python\n\n from isabelle_client import get_isabelle_client, start_isabelle_server\n \n # start Isabelle server\n server_info, _ = start_isabelle_server()\n # create a client object\n isabelle = get_isabelle_client(server_info)\n # send a theory file from the current directory to the server\n response = isabelle.use_theories(\n theories=[\"Example\"], master_dir=\".\", watchdog_timeout=0\n )\n # shut the server down\n isabelle.shutdown()\n\n\nFor more details, follow the `usage example\n<https://isabelle-client.readthedocs.io/en/latest/example.html>`__\nfrom documentation or a `notebook\n<https://github.com/inpefess/isabelle-client/blob/master/examples/example.ipynb>`__.\n\n\nHigh-level connector\n====================\n\nYou can also pass a theory file body (something you typically put\nbetween ``begin`` and ``end`` keywords) to a high-level connector\nthat will generate a temporary file for you, send it to the Isabelle\nserver and get the result for you. For example, this snippet:\n\n.. code:: python\n\n from isabelle_client.isabelle_connector import IsabelleConnector\n from isabelle_client.isabelle_connector import IsabelleTheoryError\n\n isabelle_connector = IsabelleConnector()\n try:\n isabelle_connector.build_theory(\n r'lemma \"\\<forall> x. \\<forall> y. x = y\"' \"\\nby auto\"\n )\n print(\"Theory is validated!\")\n except IsabelleTheoryError as error:\n print(error.args[0])\n\n\nwill produce something like:\n\n.. code::\n\n : Failed to finish proof\\<^here>:\n : goal (1 subgoal):\n : 1. \\<And>x y. x = y\n\nMore documentation\n==================\n\nMore documentation can be found\n`here <https://isabelle-client.readthedocs.io/en/latest>`__.\n\nSimilar Software\n================\n\nThere are Python clients to other interactive theorem provers, for\nexample:\n\n* `for Lean\n <https://github.com/leanprover-community/lean-client-python>`__\n* `for Coq <https://github.com/IBM/pycoq>`__\n* `another one for Coq <https://github.com/ejgallego/pycoq>`__\n\nModules helping to inetract with Isabelle server from Python are\nparts of the `Proving for Fun\n<https://github.com/maxhaslbeck/proving-contest-backends>`__ project.\n\nThere are also clients to Isabelle server in other programming\nlanguages, e.g. `this one in Rust\n<https://lib.rs/crates/isabelle-client>`__.\n\nProjects using the client\n=========================\n\n`isabelle-client` helped to build some cool LLM stuff (in reversed\nchronological order):\n\n* `StepProof: Step-by-step verification of natural language\n mathematical proofs (Hu et al.)\n <https://doi.org/10.48550/arXiv.2506.10558>`__ with `code\n <https://github.com/r1nIGa/STEP-PROOF>`__\n* `HybridProver: Augmenting Theorem Proving with LLM-Driven Proof\n Synthesis and Refinement (Hu et al.)\n <https://doi.org/10.48550/arXiv.2505.15740>`__\n* `Verification and Refinement of Natural Language Explanations\n through LLM-Symbolic Theorem Proving (Quan et al., EMNLP 2024)\n <https://doi.org/10.18653/v1/2024.emnlp-main.172>`__ with `code\n <https://github.com/neuro-symbolic-ai/explanation_refinement>`__\n\nHow to cite\n===========\n\nIf you\u2019re writing a research paper, you can cite the Isabelle client\nusing the `following DOI\n<https://doi.org/10.1007/978-3-031-16681-5_24>`__. You can also cite\nIsabelle 2021 (and an earlier version of the client) with `this DOI\n<https://doi.org/10.1007/978-3-030-81097-9_20>`__. There also is a\nsomewhat more complete (but unpublished) `pre-print\n<https://arxiv.org/abs/2212.11173>`__.\n\nHow to Contribute\n=================\n\nPlease follow `the contribution guide <https://isabelle-client.readthedocs.io/en/latest/contributing.html>`__ while adhering to `the code of conduct <https://isabelle-client.readthedocs.io/en/latest/code-of-conduct.html>`__.\n\n\n.. |PyPI version| image:: https://badge.fury.io/py/isabelle-client.svg\n :target: https://badge.fury.io/py/isabelle-client\n.. |Anaconda version| image:: https://anaconda.org/conda-forge/isabelle-client/badges/version.svg\n :target: https://anaconda.org/conda-forge/isabelle-client\n.. |CircleCI| image:: https://circleci.com/gh/inpefess/isabelle-client.svg?style=svg\n :target: https://circleci.com/gh/inpefess/isabelle-client\n.. |Documentation Status| image:: https://readthedocs.org/projects/isabelle-client/badge/?version=latest\n :target: https://isabelle-client.readthedocs.io/en/latest/?badge=latest\n.. |codecov| image:: https://codecov.io/gh/inpefess/isabelle-client/branch/master/graph/badge.svg\n :target: https://codecov.io/gh/inpefess/isabelle-client\n.. |DOI| image:: https://img.shields.io/badge/DOI-10.1007%2F978--3--031--16681--5__24-blue\n :target: https://doi.org/10.1007/978-3-031-16681-5_24\n",
"bugtrack_url": null,
"license": null,
"summary": "A client to Isabelle proof assistant server",
"version": "0.6.0",
"project_urls": {
"Homepage": "https://github.com/inpefess/isabelle-client",
"Issues": "https://github.com/inpefess/isabelle-client/issues",
"Repository": "https://github.com/inpefess/isabelle-client.git"
},
"split_keywords": [
"tcp client",
" isabelle proof assistant",
" interactive theorem prover"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "713c47650303858ffbfd0f030a1c22ac962fac98171feaf38c3a298f00bdbdca",
"md5": "8d459d0a3aeb33fcf385851a01bebe62",
"sha256": "52efbf42b15f5fbbb25b8cf4276ed75df5aaffc34cf372faddc1d4be5a28cb95"
},
"downloads": -1,
"filename": "isabelle_client-0.6.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "8d459d0a3aeb33fcf385851a01bebe62",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<3.14,>=3.9.1",
"size": 25565,
"upload_time": "2025-10-07T15:40:14",
"upload_time_iso_8601": "2025-10-07T15:40:14.381440Z",
"url": "https://files.pythonhosted.org/packages/71/3c/47650303858ffbfd0f030a1c22ac962fac98171feaf38c3a298f00bdbdca/isabelle_client-0.6.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "21ddc047dd223a90b8d623c290f5ef6f65abfdde3fe22474b52a1d0fda96fabe",
"md5": "250ccc541618090053f9124b633a298d",
"sha256": "49d2ad0335dd86e6440e1b3f9261ae1dfdb42afaf4dfceb67325fe3d56f23ff3"
},
"downloads": -1,
"filename": "isabelle_client-0.6.0.tar.gz",
"has_sig": false,
"md5_digest": "250ccc541618090053f9124b633a298d",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<3.14,>=3.9.1",
"size": 19310,
"upload_time": "2025-10-07T15:40:15",
"upload_time_iso_8601": "2025-10-07T15:40:15.810979Z",
"url": "https://files.pythonhosted.org/packages/21/dd/c047dd223a90b8d623c290f5ef6f65abfdde3fe22474b52a1d0fda96fabe/isabelle_client-0.6.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-10-07 15:40:15",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "inpefess",
"github_project": "isabelle-client",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"circle": true,
"lcname": "isabelle-client"
}
JSON
