Skip to content

Commit

Permalink
Merge pull request #40 from inpefess/list-responses
Browse files Browse the repository at this point in the history
List responses
  • Loading branch information
inpefess committed Dec 12, 2021
2 parents 493dc03 + e3259e7 commit 7219ff9
Show file tree
Hide file tree
Showing 10 changed files with 327 additions and 326 deletions.
58 changes: 0 additions & 58 deletions README.md

This file was deleted.

97 changes: 97 additions & 0 deletions README.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
|PyPI version| |CircleCI| |Documentation Status| |codecov| |Binder|

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/Isabelle2021/doc/system.pdf>`__.

How to Install
==============

The best way to install this package is to use ``pip``:

.. code:: sh
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 `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
=================

`Pull requests <https://github.com/inpefess/isabelle-client/pulls>`__
are welcome. To start:

.. code:: sh
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 <https://github.com/inpefess/isabelle-client/blob/master/show_report.sh>`__.
It locally does nearly the same as the CI pipeline after the PR is
created.

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
=============

|video tutorial|.

How to cite
===========

If you’re writing a research paper, you can cite Isabelle client (and
Isabelle 2021) using the `following
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
.. |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=example.ipynb
.. |video tutorial| image:: ../../examples/tty.gif
82 changes: 1 addition & 81 deletions doc/source/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -13,85 +13,7 @@
See the License for the specific language governing permissions and
limitations under the License.


=================================
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/Isabelle2021/doc/system.pdf>`__.

How to Install
==============

The best way to install this package is to use ``pip``:

.. code:: sh
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 `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
=================

`Pull requests <https://github.com/inpefess/isabelle-client/pulls>`__
are welcome. To start:

.. code:: sh
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 <https://github.com/inpefess/isabelle-client/blob/master/show_report.sh>`__.
It locally does nearly the same as the CI pipeline after the PR is
created.

Reporting issues or problems with the software
==============================================

Questions and bug reports are welcome on `the
tracker <https://github.com/inpefess/isabelle-client/issues>`__.

Video example
=============

|video tutorial|.

How to cite
===========

If you’re writing a research paper, you can cite Isabelle client (and
Isabelle 2021) using the `following
DOI <https://doi.org/10.1007/978-3-030-81097-9_20>`__.
.. include:: ../../README.rst

.. toctree::
:maxdepth: 3
Expand All @@ -106,5 +28,3 @@ Indices and tables
* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`

.. |video tutorial| image:: ../../examples/tty.gif
Binary file modified examples/tty.gif
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion examples/video_example/char_by_char.py
Original file line number Diff line number Diff line change
Expand Up @@ -24,4 +24,4 @@
else:
for char in line:
print(char, end="", flush=True)
time.sleep(60 / 600)
time.sleep(70 / 600)
21 changes: 11 additions & 10 deletions examples/video_example/example.txt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Hi! This is an example of using ``isabelle-client`` package
ipython
SLEEP 1
SLEEP 3
# first, we need to start an Isabelle server
from isabelle_client import start_isabelle_server

Expand All @@ -19,20 +19,21 @@ import logging
isabelle.logger = logging.getLogger()
isabelle.logger.setLevel(logging.INFO)
isabelle.logger.addHandler(logging.FileHandler("session.log"))
# let's suppose that we also have another Python script which generates
# some theory files
# let's suppose that we also have another Python script
# which generates some theory files
!cat Example.thy
# now we can build a session document using ROOT and root.tex files
!ls document
!cat ROOT
isabelle.session_build(dirs=["."], session="examples")
SLEEP 3
# note that the client returns only the last reply from the server
# all other messages are saved to the log file
# we also can issue a free-form command through TCP
SLEEP 12
# all these messages are also saved to the log file
!ls output
# in addition, we can issue a free-form command through TCP
from isabelle_client import async_run

async_run(isabelle.execute_command("echo 42", asynchronous=False))
isabelle.shutdown()
exit()
# our sessions was logged to the file:
cat session.log & sleep 3
!cat session.log
SLEEP 3
bye

0 comments on commit 7219ff9

Please sign in to comment.