Merge pull request #34 from inpefess/how-to-cite

How to cite

README.md

@@ -1,69 +1,9 @@
 [![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)
 
-# Isabelle Client
+Documentation is hosted [here](https://isabelle-client.readthedocs.io).
 
-A 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/Isabelle2021/doc/system.pdf).
-
-For information on using this client see [documentation](https://isabelle-client.readthedocs.io).
-
-# How to install
-
-```bash
-pip install isabelle-client
-```
-
-# How to start Isabelle server
-
-```bash
-isabelle server > server.info
-```
-
-since we'll need server info for connecting to it with this client. Or:
-
-```Python
-from isabelle_client.utils import start_isabelle_server
-
-server_info, server_process = start_isabelle_server()
-``` 
-
-# How to connect to the server
-
-```Python
-from isabelle_client.utils import get_isabelle_client
-
-isabelle = get_isabelle_client(server_info)
-```
-
-# How to send a command to the server
-
-```Python
-isabelle.session_build(dirs=["."], session="examples")
-```
-
-Note that this method returns only the last reply from the server.
-
-# How to log all replies from the server
-
-We can add a standard Python logger to the client:
-
-```Python
-import logging
-
-isabelle.logger = logging.getLogger()
-isabelle.logger.setLevel(logging.INFO)
-isabelle.logger.addHandler(logging.FileHandler("out.log"))
-```
-
-Then all replies from the server will go to the file ``out.log``.
-
-# Examples
-
-For an example of using this package see the ``examples`` directory.
+If you're writing a research paper, you can cite Isabelle client (and Isabelle 2021) in the [following way](https://dblp.org/rec/conf/mkm/LiskaLNRSSSW21.bib).
 
 # Video example
 
 ![video tutorial](https://github.com/inpefess/isabelle-client/blob/master/examples/tty.gif).
-
-# Contributing
-
-Issues and PRs are welcome.

doc/source/how-to-cite.rst

@@ -0,0 +1,45 @@
+..
+  Copyright 2021 Boris Shminke
+
+  Licensed under the Apache License, Version 2.0 (the "License");
+  you may not use this file except in compliance with the License.
+  You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+  Unless required by applicable law or agreed to in writing, software
+  distributed under the License is distributed on an "AS IS" BASIS,
+  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+  See the License for the specific language governing permissions and
+  limitations under the License.
+
+How to cite
+************
+
+If you're writing a research paper, you can cite Isabelle client (and Isabelle 2021) in the following way::
+
+  @inproceedings{DBLP:conf/mkm/LiskaLNRSSSW21,
+  author    = {Martin L{\'{\i}}ska and
+  D{\'{a}}vid Lupt{\'{a}}k and
+  V{\'{\i}}t Novotn{\'{y}} and
+  Michal Ruzicka and
+  Boris Shminke and
+  Petr Sojka and
+  Michal Stef{\'{a}}nik and
+  Makarius Wenzel},
+  editor    = {Fairouz Kamareddine and
+  Claudio Sacerdoti Coen},
+  title     = {CICM'21 Systems Entries},
+  booktitle = {Intelligent Computer Mathematics - 14th International Conference,
+  {CICM} 2021, Timisoara, Romania, July 26-31, 2021, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {12833},
+  pages     = {245--248},
+  publisher = {Springer},
+  year      = {2021},
+  url       = {https://doi.org/10.1007/978-3-030-81097-9\_20},
+  doi       = {10.1007/978-3-030-81097-9\_20},
+  timestamp = {Wed, 21 Jul 2021 15:51:07 +0200},
+  biburl    = {https://dblp.org/rec/conf/mkm/LiskaLNRSSSW21.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+  }

doc/source/how-to-contribute.rst

@@ -0,0 +1,30 @@
+..
+  Copyright 2021 Boris Shminke
+
+  Licensed under the Apache License, Version 2.0 (the "License");
+  you may not use this file except in compliance with the License.
+  You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+  Unless required by applicable law or agreed to in writing, software
+  distributed under the License is distributed on an "AS IS" BASIS,
+  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+  See the License for the specific language governing permissions and
+  limitations under the License.
+
+How to contribute
+==================
+
+Pull requests are welcome. To start::
+
+    git clone https://github.com/inpefess/isabelle-client
+    cd isabelle-client
+    # activate python virtual environment with Python 3.6+
+    pip install -U pip
+    pip install -U setuptools wheel poetry
+    poetry install
+    # recommended but not necessary
+    pre-commit install
+
+To check the code quality before creating a pull request, one might run the script ``show_report.sh``. It locally does nearly the same as the CI pipeline after the PR is created.

doc/source/index.rst

@@ -13,59 +13,39 @@
   See the License for the specific language governing permissions and
   limitations under the License.
 
+
+##########################################
 Welcome to Isabelle client documentation!
-===========================================
+##########################################
 
-A client for `Isabelle`_ server. For more information about the server see part 4 of `the Isabelle system manual`_.
+`isabelle-client`_ is a TCP client for `Isabelle`_ server. For more information about the server see part 4 of `the Isabelle system manual`_.
 
-How to install
-===============
+Getting started
+****************
 
 The best way to install this client is to use ``pip``::
 
     pip install isabelle-client
 
-In what case to use
-====================
+Then follow :ref:`usage-example` or run `the script`_
 
-This client might be useful if:
-
-* you have an Isabelle server instance running
-* you have scripts for automatic generation of theory files in Python
-* you want to communicate with the server not using Scala and/or StandardML
-
-See also :ref:`usage-example`.
-
-How to contribute
-==================
-
-Pull requests are welcome. To start::
-
-    git clone https://github.com/inpefess/isabelle-client
-    cd isabelle-client
-    # activate python virtual environment with Python 3.6+
-    pip install -U pip
-    pip install -U setuptools wheel poetry
-    poetry install
-    # recommended but not necessary
-    pre-commit install
-
-To check the code quality before creating a pull request, one might run the script ``show_report.sh``. It locally does nearly the same as the CI pipeline after the PR is created.
-
-
 .. toctree::
-   :maxdepth: 2
+   :maxdepth: 3
    :caption: Contents:
-	     
+
    usage-example
    package-documentation
+   how-to-contribute
+   how-to-cite
 
 Indices and tables
-==================
+*******************
 
 * :ref:`genindex`
 * :ref:`modindex`
 * :ref:`search`
 
 .. _Isabelle: https://isabelle.in.tum.de
 .. _the Isabelle system manual: https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf
+.. _isabelle-client: https://pypi.org/project/isabelle-client
+.. _the script: https://github.com/inpefess/isabelle-client/blob/master/examples/example.py

doc/source/package-documentation.rst

@@ -15,35 +15,45 @@
 
 
 Package Documentation
-=====================
-
-Isabelle Response
------------------
-.. autoclass:: isabelle_client.IsabelleResponse
-   :special-members: __init__
-   :members:
-
+**********************
 
 Isabelle Client
----------------
+^^^^^^^^^^^^^^^^
 .. autoclass:: isabelle_client.IsabelleClient
    :special-members: __init__
    :members:
 
 socket_communication
---------------------
+^^^^^^^^^^^^^^^^^^^^^
 .. currentmodule:: isabelle_client.socket_communication
 
 A collection of functions for TCP communication.
 
+Isabelle Response
+==================
+.. autoclass:: isabelle_client.IsabelleResponse
+   :special-members: __init__
+   :members:
+
 .. autofunction:: get_response_from_isabelle
 .. autofunction:: get_final_message
 
 utils
------
+^^^^^^
 .. currentmodule:: isabelle_client.utils
 
 A collection of different useful functions.
 
 .. autofunction:: start_isabelle_server
 .. autofunction:: get_isabelle_client
+
+compatibility_helper
+^^^^^^^^^^^^^^^^^^^^^
+.. currentmodule:: isabelle_client.compatibility_helper
+
+A module helping to run `asyncio`_ in Python 3.6
+
+.. autofunction:: async_run
+
+
+.. _asyncio: https://docs.python.org/3/library/asyncio.html

doc/source/usage-example.rst

@@ -16,8 +16,17 @@
 .. _usage-example:
 
 Basic usage example
+********************
+
+In what case to use
 ====================
 
+This client might be useful if:
+
+* you have an Isabelle server instance running
+* you have scripts for automatic generation of theory files in Python
+* you want to communicate with the server not using Scala and/or StandardML
+
 First, we need to start an Isabelle server::
   
     from isabelle_client import start_isabelle_server
@@ -26,8 +35,10 @@ First, we need to start an Isabelle server::
         name="test", port=9999, log_file="server.log"
     )
 
-We could also start the server outside this script and use its info.
+We could also start the server outside this script and use its info::
 
+    isabelle server > server.info
+    
 Now let's create a client to our server ::
 
     from isabelle_client import get_isabelle_client

examples/example.py

@@ -23,7 +23,7 @@
 
 
 def main():
-    """ using ``isabelle`` client """
+    """ using Isabelle client """
     # first, we start Isabelle server
     server_info, _ = start_isabelle_server(
         name="test", port=9999, log_file="server.log"