|Binder|\ |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 part 4 of `the Isabelle system
manual <https://isabelle.in.tum.de/dist/Isabelle2024/doc/system.pdf>`__.
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 -it --rm -p 8888:8888 isabelle-client jupyter-lab --ip=0.0.0.0 --port=8888
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/usage-example.html#usage-example>`__
from documentation, run the
`script <https://github.com/inpefess/isabelle-client/blob/master/examples/example.py>`__,
or use ``isabelle-client`` from a
`notebook <https://github.com/inpefess/isabelle-client/blob/master/examples/example.ipynb>`__,
e.g. with
`Binder <https://mybinder.org/v2/gh/inpefess/isabelle-client/HEAD?labpath=isabelle-client-examples/example.ipynb>`__ (Binder might fail with 'Failed to create temporary user for ...' error which is `well known <https://mybinder-sre.readthedocs.io/en/latest/incident-reports/2018-02-20-jupyterlab-announcement.html>`__ and related neither to ``isabelle-client`` nor to the provided ``Dockerfile``. If that happens, try to run Docker as described in the section above).
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>`__.
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 the 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
.. |Binder| image:: https://mybinder.org/badge_logo.svg
:target: https://mybinder.org/v2/gh/inpefess/isabelle-client/HEAD?labpath=isabelle-client-examples/example.ipynb
.. |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.13,>=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/20/f9/da253525b7791f2cd1c69308b6438400e226e2241e4aadfe9469e2248a69/isabelle_client-0.5.3.tar.gz",
"platform": null,
"description": "|Binder|\\ |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 part 4 of `the Isabelle system\nmanual <https://isabelle.in.tum.de/dist/Isabelle2024/doc/system.pdf>`__.\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 -it --rm -p 8888:8888 isabelle-client jupyter-lab --ip=0.0.0.0 --port=8888\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\nexample <https://isabelle-client.readthedocs.io/en/latest/usage-example.html#usage-example>`__\nfrom documentation, run the\n`script <https://github.com/inpefess/isabelle-client/blob/master/examples/example.py>`__,\nor use ``isabelle-client`` from a\n`notebook <https://github.com/inpefess/isabelle-client/blob/master/examples/example.ipynb>`__,\ne.g.\u00a0with\n`Binder <https://mybinder.org/v2/gh/inpefess/isabelle-client/HEAD?labpath=isabelle-client-examples/example.ipynb>`__ (Binder might fail with 'Failed to create temporary user for ...' error which is `well known <https://mybinder-sre.readthedocs.io/en/latest/incident-reports/2018-02-20-jupyterlab-announcement.html>`__ and related neither to ``isabelle-client`` nor to the provided ``Dockerfile``. If that happens, try to run Docker as described in the section above).\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\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 the 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.. |Binder| image:: https://mybinder.org/badge_logo.svg\n :target: https://mybinder.org/v2/gh/inpefess/isabelle-client/HEAD?labpath=isabelle-client-examples/example.ipynb\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": "Apache-2.0",
"summary": "A client to Isabelle proof assistant server",
"version": "0.5.3",
"project_urls": {
"Homepage": "https://github.com/inpefess/isabelle-client",
"Repository": "https://github.com/inpefess/isabelle-client"
},
"split_keywords": [
"tcp client",
" isabelle proof assistant",
" interactive theorem prover"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "2910859d0b81ee55ad5ee3440860502c810e8b098af4996805474e8f4c3beba7",
"md5": "4f9d94ec218a073f462823c826dfebea",
"sha256": "e8a3503c2ea28b8396e9a4074a8eb6eda810e3daacb2da043dad90915716d9b5"
},
"downloads": -1,
"filename": "isabelle_client-0.5.3-py3-none-any.whl",
"has_sig": false,
"md5_digest": "4f9d94ec218a073f462823c826dfebea",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<3.13,>=3.9.1",
"size": 26049,
"upload_time": "2025-01-25T11:43:53",
"upload_time_iso_8601": "2025-01-25T11:43:53.274037Z",
"url": "https://files.pythonhosted.org/packages/29/10/859d0b81ee55ad5ee3440860502c810e8b098af4996805474e8f4c3beba7/isabelle_client-0.5.3-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "20f9da253525b7791f2cd1c69308b6438400e226e2241e4aadfe9469e2248a69",
"md5": "18330cd0bcd458413cb04585ba7e1dba",
"sha256": "3bb8492c8aea9da59da74e54514ee17d1ae6a7cfa060ab4afa8442a73e240e98"
},
"downloads": -1,
"filename": "isabelle_client-0.5.3.tar.gz",
"has_sig": false,
"md5_digest": "18330cd0bcd458413cb04585ba7e1dba",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<3.13,>=3.9.1",
"size": 20058,
"upload_time": "2025-01-25T11:43:55",
"upload_time_iso_8601": "2025-01-25T11:43:55.546177Z",
"url": "https://files.pythonhosted.org/packages/20/f9/da253525b7791f2cd1c69308b6438400e226e2241e4aadfe9469e2248a69/isabelle_client-0.5.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-01-25 11:43:55",
"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
