Merge pull request #37 from inpefess/python3.10-support

Python3.10 support

.circleci/config.yml

@@ -1,30 +1,26 @@
 version: 2.1
 
-orbs:
-  python: circleci/python@0.2.1
-
 jobs:
   build-and-test:
     docker:
-      - image: circleci/python:3.9.1
+      - image: cimg/python:3.10.0
     working_directory: ~/repo
     steps:
       - checkout
       - restore_cache:
           keys:
-            - v1-dependencies-{{ checksum "poetry.lock" }}
-            - v1-dependencies-
+            - v2-dependencies-{{ checksum "poetry.lock" }}
       - run:
           name: install dependencies
           command: |
-            python3 -m venv venv
+            python -m venv venv
             . venv/bin/activate
             pip install -U pip poetry
             poetry install
       - save_cache:
           paths:
             - ./venv
-          key: v1-dependencies-{{ checksum "poetry.lock" }}
+          key: v2-dependencies-{{ checksum "poetry.lock" }}
       - run:
           name: run tests
           command: |

.dockerignore

@@ -0,0 +1,14 @@
+Dockerfile
+venv*/
+dist/
+doc/build/
+.mypy_cache/
+.pytest_cache/
+__pycache__/
+examples/tty.gif
+examples/video_example/
+examples/output/
+examples/session.log
+examples/.mypy_cache/
+examples/.ipynb_checkpoints/
+.idea/

.gitignore

@@ -14,3 +14,4 @@ doc/build/
 *.out
 *.aux
 *.cicmauthinsts
+.ipynb_checkpoints/

Dockerfile

@@ -0,0 +1,10 @@
+FROM makarius/isabelle:Isabelle2021
+ENV HOME=/home/isabelle
+ENV PATH=${HOME}/.local/bin:${HOME}/Isabelle/bin:${PATH}
+USER root
+RUN apt-get update
+RUN apt-get install -y python3-pip
+USER isabelle
+RUN pip install -U pip isabelle-client jupyterlab
+COPY examples ${HOME}
+ENTRYPOINT []

README.md

@@ -1,4 +1,5 @@
 [![PyPI version](https://badge.fury.io/py/isabelle-client.svg)](https://badge.fury.io/py/isabelle-client) [![CircleCI](https://circleci.com/gh/inpefess/isabelle-client.svg?style=svg)](https://circleci.com/gh/inpefess/isabelle-client) [![Documentation Status](https://readthedocs.org/projects/isabelle-client/badge/?version=latest)](https://isabelle-client.readthedocs.io/en/latest/?badge=latest) [![codecov](https://codecov.io/gh/inpefess/isabelle-client/branch/master/graph/badge.svg)](https://codecov.io/gh/inpefess/isabelle-client)
+[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/inpefess/isabelle-client/HEAD?labpath=example.ipynb)
 
 # Python client for Isabelle server
 
@@ -12,9 +13,16 @@ The best way to install this package is to use `pip`:
 pip install isabelle-client
 ```
 
+One can also download and run the client together with Isabelle in a Docker contanier:
+
+```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 --no-browser
+```
+
 # How to use
 
-Follow the [usage example](https://isabelle-client.readthedocs.io/en/latest/usage-example.html#usage-example) from documentation or run the [script](https://github.com/inpefess/isabelle-client/blob/master/examples/example.py).
+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=example.ipynb).
 
 # How to Contribute
 

doc/source/index.rst

@@ -14,7 +14,7 @@
   limitations under the License.
 
 
-=================================
+=================================  
 Python client for Isabelle server
 =================================
 
@@ -32,11 +32,25 @@ The best way to install this package is to use ``pip``:
 
    pip install 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 --no-browser
+
 How to use
 ==========
 
-Follow the :ref:`usage-example` from documentation or run the
-`script <https://github.com/inpefess/isabelle-client/blob/master/examples/example.py>`__.
+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=example.ipynb>`__.
 
 How to Contribute
 =================
@@ -67,12 +81,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
 =============
 

doc/source/usage-example.rst

@@ -55,9 +55,9 @@ We will log all the messages from the server to a file ::
 
 This client has several methods implemented to communicate with the server Python-style, e.g.::
 
-    isabelle.use_theories(theories=["Dummy"], master_dir=".")
+    isabelle.use_theories(theories=["Example"], master_dir=".")
 
-In this command it's supposed that we have a ``Dummy.thy`` theory file in our working directory which we, e.g. generated with another Python script.
+In this command it's supposed that we have a ``Example.thy`` theory file in our working directory which we, e.g. generated with another Python script.
 
 One can also issue a free-form command, e.g.::
 

examples/Example.thy

@@ -0,0 +1,6 @@
+theory Example
+imports Main
+begin
+lemma "\<forall> x. \<exists> y. x = y"
+by auto
+end

examples/ROOT

@@ -1,6 +1,6 @@
 session examples = HOL +
   options [document = pdf, document_output = "output"]
   theories
-    Dummy
+    Example
   document_files
     "root.tex"