Merge pull request #56 from inpefess/better-readme

better README

.circleci/config.yml

@@ -14,7 +14,7 @@ jobs:
           name: use tox
           command: |
             pip install tox
-            pyenv local 3.7.13 3.8.13 3.9.13 3.10.4
+            pyenv local 3.7.15 3.8.15 3.9.15 3.10.7 3.11.0
             tox
       - run:
           name: upload data to codecov

Dockerfile

@@ -1,4 +1,4 @@
-FROM makarius/isabelle:Isabelle2021-1
+FROM makarius/isabelle:Isabelle2022
 ARG NB_USER=jovyan
 ARG NB_UID=1000
 ENV USER ${NB_USER}
@@ -11,7 +11,7 @@ RUN adduser --disabled-password \
     --uid ${NB_UID} \
     ${NB_USER}
 RUN apt-get update
-RUN apt-get install -y python3-pip netcat
+RUN apt-get install -y python3-pip
 ENV HOME /home/${NB_USER}
 ENV ISABELLE_BIN /home/isabelle/Isabelle/bin/
 ENV PATH=${HOME}/.local/bin/:${ISABELLE_BIN}:${PATH}

README.rst

@@ -35,7 +35,23 @@ Docker contanier:
 How to use
 ==========
 
-Follow the `usage
+.. 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>`__,
@@ -44,6 +60,36 @@ or use ``isabelle-client`` from a
 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 Packages
+================
+
+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.
+
+How to cite
+===========
+
+If you’re writing a research paper, you can cite 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>`__.
+
 How to Contribute
 =================
 
@@ -73,26 +119,6 @@ Reporting issues or problems with the software
 Questions and bug reports are welcome on `the
 tracker <https://github.com/inpefess/isabelle-client/issues>`__.
 
-More documentation
-==================
-
-More documentation can be found
-`here <https://isabelle-client.readthedocs.io/en/latest>`__.
-
-Video example
-=============
-
-.. image:: https://isabelle-client.readthedocs.io/en/latest/_images/tty.gif
-
-How to cite
-===========
-
-If you’re writing a research paper, you can cite 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>`__.
-
 .. |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
@@ -105,4 +131,3 @@ DOI <https://doi.org/10.1007/978-3-030-81097-9_20>`__.
    :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
-

doc/source/conf.py

@@ -19,7 +19,7 @@
 
 sys.path.insert(0, os.path.abspath("../.."))
 project = "isabelle-client"
-version = "0.3.9"
+version = "0.3.10"
 copyright = "2021-2022, Boris Shminke"
 author = "Boris Shminke"
 extensions = ["sphinx.ext.autodoc", "sphinx.ext.coverage"]

isabelle_client/__init__.py

@@ -17,4 +17,4 @@
 from isabelle_client.socket_communication import IsabelleResponse
 from isabelle_client.utils import get_isabelle_client, start_isabelle_server
 
-__version__ = "0.3.9"
+__version__ = "0.3.10"