Merge pull request #59 from inpefess/add-preprint

Add preprint

.dockerignore

@@ -19,3 +19,6 @@ cicm2021paper/
 LICENSE
 tests/
 coverage.xml
+cicm2022paper/
+cicm2022talk/
+unpublished-pre-print/

.gitignore

@@ -22,3 +22,4 @@ coverage.xml
 *.nav
 *.snm
 *.toc
+_minted-*/

Dockerfile

@@ -1,4 +1,4 @@
-FROM makarius/isabelle:Isabelle2022
+FROM makarius/isabelle:Isabelle2022_X11_Latex
 ARG NB_USER=jovyan
 ARG NB_UID=1000
 ENV USER ${NB_USER}

doc/source/conf.py

@@ -19,7 +19,7 @@
 
 sys.path.insert(0, os.path.abspath("../.."))
 project = "isabelle-client"
-version = "0.3.12"
+version = "0.3.13"
 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.12"
+__version__ = "0.3.13"

pyproject.toml

@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "isabelle-client"
-version = "0.3.12"
+version = "0.3.13"
 description = "A client to Isabelle proof assistant server"
 authors = ["Boris Shminke <boris@shminke.ml>"]
 license = "Apache-2.0"
@@ -133,7 +133,7 @@ commands =
 github_url = "https://github.com/inpfess/isabelle-client/"
 
 [tool.tbump.version]
-current = "0.3.12"
+current = "0.3.13"
 regex = '''
   (?P<major>\d+)
   \.

unpublished-pre-print/cicm2022.bib

@@ -0,0 +1,181 @@
+@article{haslbeck2019competitive,
+  title={Competitive Proving for Fun},
+  author={Haslbeck, Maximilian PL and Wimmer, Simon},
+  journal={Kalpa Publications in Computing},
+  volume={10},
+  pages={9--14},
+  year={2019},
+  publisher={EasyChair}
+}
+@article{DBLP:journals/corr/abs-2109-05264,
+  author    = {Wesley Fussner and
+               Boris Shminke},
+  title     = {Mining counterexamples for wide-signature algebras with an Isabelle
+               server},
+  journal   = {CoRR},
+  volume    = {abs/2109.05264},
+  year      = {2021},
+  url       = {https://arxiv.org/abs/2109.05264},
+  eprinttype = {arXiv},
+  eprint    = {2109.05264},
+  timestamp = {Tue, 21 Sep 2021 17:46:04 +0200},
+  biburl    = {https://dblp.org/rec/journals/corr/abs-2109-05264.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+@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 = {Mon, 03 Jan 2022 22:24:40 +0100},
+  biburl    = {https://dblp.org/rec/conf/mkm/LiskaLNRSSSW21.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+@misc{conda_forge_community_2015_4774216,
+  author       = {conda-forge community},
+  title        = {{The conda-forge Project: Community-based Software
+                   Distribution Built on the conda Package Format and
+                   Ecosystem}},
+  month        = jul,
+  year         = 2015,
+  publisher    = {Zenodo},
+  doi          = {10.5281/zenodo.4774216},
+  url          = {https://doi.org/10.5281/zenodo.4774216}
+}
+@InProceedings{10.1007/978-3-030-79876-5_37,
+author="Moura, Leonardo de
+and Ullrich, Sebastian",
+editor="Platzer, Andr{\'e}
+and Sutcliffe, Geoff",
+title="The Lean 4 Theorem Prover and Programming Language",
+booktitle="Automated Deduction -- CADE 28",
+year="2021",
+publisher="Springer International Publishing",
+address="Cham",
+pages="625--635",
+abstract="Lean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom proof automation procedures in Lean itself.",
+isbn="978-3-030-79876-5"
+}
+@misc{LeanClient,
+  author = {Jason Rute and
+            Patrick Massot and
+            Julian Berman and
+	    Frederic Le Roux},
+  title = {Lean client for Python},
+  month = aug,
+  year = 2021,
+  url = {https://github.com/leanprover-community/lean-client-python}
+}
+@misc{CoqClient,
+  author = {Emilio Jesus \relax{Gallego Arias} and
+            Thierry Martinez},
+  title = {PyCoq: Access Coq from Python!},
+  month = jan,
+  year = 2022,
+  url = {https://github.com/ejgallego/pycoq}
+}
+@misc{TIOBEIndex,
+  author = {\relax{TIOBE Software BV}},
+  title = {The TIOBE Programming Community index},
+  month = apr,
+  year = 2022,
+  url = {https://www.tiobe.com/tiobe-index/}
+}
+@software{the_coq_development_team_2022_5846982,
+  author       = {\relax{The Coq Development Team}},
+  title        = {The Coq Proof Assistant},
+  month        = jan,
+  year         = 2022,
+  publisher    = {Zenodo},
+  version      = {8.15},
+  doi          = {10.5281/zenodo.5846982},
+  url          = {https://doi.org/10.5281/zenodo.5846982}
+}
+@inproceedings{IsabelleServer,
+  author = {Makarius Wenzel},
+  title = {Isabelle/PIDE after 10 years of development},
+  booktitle = {13th International Workshop on User Interfaces for Theorem Provers (UITP 2018)},
+  series = {Federated Logic Conference 2018},
+  year = 2018,
+  url = {https://sketis.net/wp-content/uploads/2018/08/isabelle-pide-uitp2018.pdf}
+}
+@book{DBLP:books/sp/NipkowPW02,
+  author    = {Tobias Nipkow and
+               Lawrence C. Paulson and
+               Markus Wenzel},
+  title     = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2283},
+  publisher = {Springer},
+  year      = {2002},
+  url       = {https://doi.org/10.1007/3-540-45949-9},
+  doi       = {10.1007/3-540-45949-9},
+  isbn      = {3-540-43376-7},
+  timestamp = {Tue, 14 May 2019 10:00:35 +0200},
+  biburl    = {https://dblp.org/rec/books/sp/NipkowPW02.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+@InProceedings{ project_jupyter-proc-scipy-2018,
+  author    = { {P}roject {J}upyter and {M}atthias {B}ussonnier and {J}essica {F}orde and {J}eremy {F}reeman and {B}rian {G}ranger and {T}im {H}ead and {C}hris {H}oldgraf and {K}yle {K}elley and {G}ladys {N}alvarte and {A}ndrew {O}sheroff and {M} {P}acer and {Y}uvi {P}anda and {F}ernando {P}erez and {B}enjamin {R}agan-{K}elley and {C}arol {W}illing },
+  title     = { {B}inder 2.0 - {R}eproducible, interactive, sharable environments for science at scale },
+  booktitle = { {P}roceedings of the 17th {P}ython in {S}cience {C}onference },
+  pages     = { 113 - 120 },
+  year      = { 2018 },
+  editor    = { {F}atih {A}kici and {D}avid {L}ippa and {D}illon {N}iederhut and {M} {P}acer },
+  doi       = { 10.25080/Majora-4af1f417-011 }
+}
+@article{DBLP:journals/cse/GrangerP21,
+  author    = {Brian E. Granger and
+               Fernando P{\'{e}}rez},
+  title     = {Jupyter: Thinking and Storytelling With Code and Data},
+  journal   = {Comput. Sci. Eng.},
+  volume    = {23},
+  number    = {2},
+  pages     = {7--14},
+  year      = {2021},
+  url       = {https://doi.org/10.1109/MCSE.2021.3059263},
+  doi       = {10.1109/MCSE.2021.3059263},
+  timestamp = {Thu, 29 Apr 2021 15:14:54 +0200},
+  biburl    = {https://dblp.org/rec/journals/cse/GrangerP21.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+@misc{KaggleReport,
+  author = {\relax{Kaggle Inc.}},
+  title = {State of Data Science and Machine Learning 2021},
+  month = oct,
+  year = 2021,
+  url = {https://www.kaggle.com/kaggle-survey-2021}
+}
+@misc{IsabelleSystemManual,
+  author = {Makarius Wenzel},
+  title = {The Isabelle System Manual},
+  month = dec,
+  year = 2021,
+  url = {https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/system.pdf}
+}
+@software{boris_shminke_2022_6490275,
+  author       = {Boris Shminke},
+  title        = {Python client for Isabelle server},
+  month        = apr,
+  year         = 2022,
+  publisher    = {Zenodo},
+  version      = {0.3.5},
+  doi          = {10.5281/zenodo.6490275},
+  url          = {https://doi.org/10.5281/zenodo.6490275}
+}

unpublished-pre-print/cicm2022.tex

@@ -0,0 +1,84 @@
+\documentclass[runningheads]{llncs}
+\usepackage[T1]{fontenc}
+\usepackage{graphicx}
+\usepackage{minted}
+\usemintedstyle{friendly}
+\usepackage{hyperref}
+\usepackage{color}
+\renewcommand\UrlFont{\color{blue}\rmfamily}
+
+\begin{document}
+\title{Python client for Isabelle server\thanks{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.}}
+%
+%\titlerunning{Abbreviated paper title}
+% If the paper title is too long for the running head, you can set
+% an abbreviated paper title here
+%
+\author{Boris Shminke\inst{1}\orcidID{0000-0002-1291-9896}}
+\authorrunning{B. Shminke}
+\institute{Université Côte d'Azur, CNRS, LJAD, France \\
+\email{boris.shminke@univ-cotedazur.fr}}
+\maketitle
+
+\begin{abstract}
+We contribute a Python client for the Isabelle server, which gives researchers and students using Python as their primary programming language an opportunity to communicate with the Isabelle server through TCP directly from a Python script. Such an approach helps avoid the complexities of integrating the existing Python script with languages used for Isabelle development (ML and Scala). We also describe new features that appeared since the announcement of the first version of the client a year ago. Finally, we give examples of the client's applications in research and education and discuss known limitations and possible directions for future development.
+
+\keywords{Isabelle \and Python \and client-server architecture}
+\end{abstract}
+\section{Introduction}
+Isabelle~\cite{DBLP:books/sp/NipkowPW02} interactive theorem prover (ITP) has included the Isabelle server as part of its standard distribution since 2018~\cite{IsabelleServer}. The Isabelle server enables users to run multiple sessions and manage concurrent tasks to process Isabelle theory files through TCP. It makes, in principle, possible to communicate with the Isabelle server using any popular programming language~\cite{TIOBEIndex}, including Python. Python clients already exist for other major ITPs, for example, one~\cite{LeanClient} for Lean~\cite{10.1007/978-3-030-79876-5_37} or another one~\cite{CoqClient} for Coq~\cite{the_coq_development_team_2022_5846982}. To our best knowledge, the previous version (0.2.0) of the \texttt{isabelle-client} announced last year~\cite{DBLP:conf/mkm/LiskaLNRSSSW21} was the first Python client for Isabelle. This paper describes version 0.3.5 of the client (the digital artefact is available on Zenodo~\cite{boris_shminke_2022_6490275}).
+
+\section{How to use}
+A typical scenario of \texttt{isabelle-client} application is represented by Fig.~\ref{fig:architecture}. First, one should start the Isabelle server, for example, using a utility function \texttt{start\_isabelle\_server} from the package. Second, one creates an instance of \texttt{IsabelleClient} object, e.g. using the factory function \texttt{get\_isabelle\_client}. Finally, one can issue any command supported by the Isabelle server (see section 4.4 in~\cite{IsabelleSystemManual} for a full list) using \texttt{IsabelleClient} object, which implements all these commands as methods. Usually, these commands rely on existing Isabelle theory files, for example, generated by third-party Python scripts (not by \texttt{isabelle-client}). See also listing \ref{lst:example} for a basic code snippet.
+
+\begin{listing}[H]
+\begin{minted}{python}
+""" An example of the ``isabelle-client`` usage """
+from isabelle_client import get_isabelle_client, start_isabelle_server
+
+# first, we start Isabelle server
+server_info, _ = start_isabelle_server(
+    name="test", port=9999, log_file="server.log"
+)
+# then we create an ``IsabelleClient`` instance
+isabelle = get_isabelle_client(server_info)
+# now we can send theory files to the server and get a response
+isabelle.use_theories(theories=["Example"], master_dir=".")
+# or we can build a session document using ROOT and root.tex files
+isabelle.session_build(dirs=["."], session="examples")
+isabelle.shutdown()
+\end{minted}
+\caption{How to use \texttt{isabelle-client}.}
+\label{lst:example}
+\end{listing}
+
+Interested potential users of the client can also follow the package homepage~\footnote{\href{https://pypi.org/project/isabelle-client/}{https://pypi.org/project/isabelle-client/}} for more detailed information.
+
+\begin{figure}
+\includegraphics[width=\textwidth]{architecture}
+\caption{In a project where Python scripts are generating Isabelle theory files, \texttt{isabelle-client} can be used to start the Isabelle server, sending these files for parallel processing and getting back the results.} \label{fig:architecture}
+\end{figure}
+
+\section{New features since previous version}
+The first public version of this client~\cite{DBLP:conf/mkm/LiskaLNRSSSW21}, which appeared in March 2021, worked only for Python 3.7 on GNU/Linux and was supposed to be installed only with the \texttt{pip} package manager. The current version is available for any Python 3.6+ on GNU/Linux and Windows. Every new build is tested in a continuous integration workflow against each supported Python version. The package is hosted now not only on the Python Package Index (PyPI), but also on Conda Forge~\cite{conda_forge_community_2015_4774216}, which enables its installation with both \texttt{pip} and \texttt{conda} package managers. In addition, one can run the client inside a Docker container, for example, in a cloud using Binder~\cite{project_jupyter-proc-scipy-2018}. This option provides the client coupled with the Isabelle server and is particularly useful for students specialising in logic but not necessarily having much experience in information technologies.
+
+The current version of the client is tested to work with the latest Isabelle 2021-1 (released in December 2021). The last client version returns all server replies as a Python list, not only the last one as it was in the previous version giving more flexibility to the end-user. Last but not least, the current version arrives with detailed documentation pages and is nearly 100\% covered with unit tests using fixtures for emulating a working Isabelle server behaviour.
+
+\section{Known applications in research and education}
+The original system entry for \texttt{isabelle-client} expressed hope that it would be helpful to other projects. After the first year, we saw several applications confirming these aspirations. The most impressive one was a discovery of a proof~\cite{DBLP:journals/corr/abs-2109-05264} for an algebraic problem which stood open for two years despite the efforts of specialists in the field. For this project, the \texttt{isabelle-client} played a role of a bridge connecting Python scripts which generated relevant Isabelle theory files with the Isabelle server processing them.
+
+Another use case comes from higher education. The \texttt{isabelle-client} running in a Docker container on Binder was used during the practical sessions of the Advanced Logic course taught at the Université Côte d'Azur in the autumn of the 2021-2022 academic year. The client helped students not trained in functional programming languages used for Isabelle development to concentrate on understanding the Isabelle language syntax and consequently generating theory files in it with Python scripts without installing and running the Isabelle GUI on their laptops.
+
+Also, Fabian Huch used the \texttt{isabelle-client} for debugging the 'Proving for Fun' backend~\cite{haslbeck2019competitive}. The 'Proving for Fun' project already had in its codebase parts resembling the \texttt{isabelle-client}, but using the \texttt{socket} Python package that provides access to the BSD socket interface. The \texttt{isabelle-client} uses \texttt{asyncio}, providing a more high-level interface for TCP communications, and exists as a stand-alone piece of software striving to be easily reusable for different projects.
+
+\section{Known limitations, workarounds, and future work}
+The first thing one would want from a client-server application is running the server and the client on different machines (probably, with various operating systems) or, at least, in separate Docker containers. The attempts to do that with \texttt{isabelle-client} demonstrated that the current implementation of the Isabelle server doesn't support binding its IP address to anything but \texttt{localhost} for security reasons. A desirable solution is implementing an authentication mechanism for the remote Isabelle server (for example, with access tokens, as is done for the Jupyter~\cite{DBLP:journals/cse/GrangerP21} server). The current workaround is to use SSH tunnels or package the \texttt{isabelle-client} together with the Isabelle server in the same Docker container.
+
+Although the \texttt{isabelle-client} works perfectly on Windows for communication with the Isabelle server running on the same machine, it's impossible to start the Isabelle server on Windows with the utility function from the \texttt{isabelle-client} package. The reason is related to the fact that the Isabelle server on Windows runs under Cygwin and not as a proper Windows application. A possible solution could be to rewrite the Windows CMD file, which starts the Isabelle server, to make it pass the started server info from the Cygwin subsystem to the parent Windows process. The current workaround is to launch the Isabelle server manually.
+
+At some point, it became known that it's impossible to start a clean build of a session from the \texttt{isabelle-client}. The reason is that the Isabelle server (unlike \texttt{isabelle build} tool) lacks \texttt{-c} parameter in its API. Thus, achieving relative feature parity of the Isabelle server and other Isabelle tools seems to be an important direction in making the \texttt{isabelle-client} more applicable and interesting to its end users.
+\section{Conclusion}
+A year after its appearance \texttt{isabelle-client} became a more mature piece of software and found its applications in both scientific research and higher education. As shown in this paper, there are still many ways to improve it, and we hope for many possible occasions for its further application, not limited to but including machine learning (as a domain dominated by Python~\cite{KaggleReport}) for theorem proving.
+\bibliographystyle{splncs04}
+\bibliography{cicm2022}
+\end{document}