Merge pull request #36 from inpefess/maintenance

Maintenance

.gitignore

@@ -6,4 +6,11 @@ __pycache__/
 .*~
 *~
 doc/build/
-.idea/
+.idea/
+*.bbl
+*.blg
+*.log
+*.pdf
+*.out
+*.aux
+*.cicmauthinsts

README.md

@@ -1,9 +1,50 @@
 [![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)
 
-Documentation is hosted [here](https://isabelle-client.readthedocs.io).
+# Python client for Isabelle server
 
-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).
+`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`:
+
+```sh
+pip install isabelle-client
+```
+
+# 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).
+
+# How to Contribute
+
+[Pull requests](https://github.com/inpefess/isabelle-client/pulls) are welcome. To start:
+
+```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](https://github.com/inpefess/isabelle-client/blob/master/examples/tty.gif).
+
+# 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).

cicm2021paper/bib.bib

@@ -0,0 +1,36 @@
+@article{DBLP:journals/sttt/DragomirPT20,
+  author    = {Iulia Dragomir and
+               Viorel Preoteasa and
+               Stavros Tripakis},
+  title     = {The Refinement Calculus of Reactive Systems Toolset},
+  journal   = {Int. J. Softw. Tools Technol. Transf.},
+  volume    = {22},
+  number    = {6},
+  pages     = {689--708},
+  year      = {2020},
+  url       = {https://doi.org/10.1007/s10009-020-00561-4},
+  doi       = {10.1007/s10009-020-00561-4},
+  timestamp = {Tue, 17 Nov 2020 11:22:15 +0100},
+  biburl    = {https://dblp.org/rec/journals/sttt/DragomirPT20.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@misc{Kaggle2020MLSurvey,
+  author = {Kaggle},
+  title = {State of Data Science and Machine Learning},
+  year = {2020},
+  publisher = {Kaggle},
+  note = {\url{https://www.kaggle.com/kaggle-survey-2020}}
+}
+
+@misc{ProvingContestBackends,
+  author = {Maximilian P.L. Haslbeck, Simon Wimmer},
+  title = {Platform for interactive theorem proving competitions},
+  publisher = {GitHub},
+  note = {\url{https://github.com/maxhaslbeck/proving-contest-backends}}
+}
+
+@manual{isabelle-system,
+  author = {Makarius Wenzel},
+  title = {The {Isabelle} System Manual},
+  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}

cicm2021paper/example.tex

@@ -0,0 +1,31 @@
+% This is an example of contribution.
+%
+% The TOOL, VERSION, PROGRAMMINGLANGUAGE, LICENSE AND URL fields are
+% mandatory, as well as a list of CICMauthor.
+%
+% After the \maketool command you can put a number of subsubsections.
+% Suggested ones are: ``Description'', ``Applications'',
+% ``Changes from previous version'' (when applicable)
+%
+% The contribution should exactly fit one page.
+%
+% You can provide a bib.bib file for the bibliography. The bibliography
+% will be consolidated at the end of the consolidated paper.
+
+\TOOL{Python client for Isabelle server}
+\VERSION{0.2.0}
+\PROGRAMMINGLANGUAGE{Python}
+\LICENSE{Apache 2.0}
+\URL{https://pypi.org/project/isabelle-client}
+\CICMauthor{Boris Shminke}{Université Côte d’Azur, CNRS, LJAD, France}
+
+\maketool
+
+\subsubsection{Description}
+Python client for Isabelle server gives researchers using Python as their primary programming language an opportunity to communicate with Isabelle server through TCP directly from a Python script. Since Python-based tools continue to dominate the machine learning (ML) frameworks~\cite{Kaggle2020MLSurvey}, this package, installable from The Python Package Index, can help researchers from the ML community to use the power of Isabelle proof assistant in their studies. Also, in other research domains where Isabelle can be helpful, Python as scripting languages remains preferable~\cite{DBLP:journals/sttt/DragomirPT20}. Some pieces of software written in Python and related to Isabelle (e.g.~\cite{ProvingContestBackends}) can include code for communication with the server, but they are hard to find, not easily reusable and well-documented.
+
+The client relies on a standard Python package \texttt{asyncio} for low-level communication with the server. It implements wrapper methods for all commands of Isabelle server listed in its manual~\cite{isabelle-system}. The package also includes a function for starting Isabelle server from Python script.
+
+\subsubsection{Applications} At the moment, the package is being used by its author for research in AI for algebra. It helps to check hundreds of working hypotheses, auto-generated by other Python scripts.
+
+\subsubsection{Acknowledgements} This work has been supported by the French government, through the 3IA Côte d’Azur Investments in the Future project managed by the National Research Agency (ANR) with the reference number ANR-19-P3IA-0002.