Merge pull request #6 from inpefess/add-example

Add example

README.md

@@ -3,3 +3,5 @@
 # Isabelle Client
 
 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).

doc/source/index.rst

@@ -1,18 +1,36 @@
+	..
+	   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
+
+	   http://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.
+
 Welcome to Isabelle client documentation!
 ===========================================
 
 A client for `Isabelle`_ server. For more information about the server see part 4 of `the Isabelle system manual`_.
 
-Basic use-case:
+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 outside Scala and/or StandardML
+* you want to communicate with the server not using Scala and/or StandardML
+
+See also :ref:`usage-example`.
 
 .. toctree::
    :maxdepth: 2
    :caption: Contents:
-
+
+   usage-example
    package-documentation
 
 Indices and tables

doc/source/package-documentation.rst

@@ -1,3 +1,19 @@
+	..
+	   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
+
+	   http://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.
+
+
 Package Documentation
 =====================
 

doc/source/usage-example.rst

@@ -0,0 +1,47 @@
+	..
+	   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
+
+	   http://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.
+
+.. _usage-example:
+
+Basic usage example
+====================
+
+Let's suppose that Isabelle binary is on our ``PATH`` and we started an Isabelle server in working directory with the following command::
+
+  isabelle server > server.pid
+
+Now we can get an instance of Isabelle client to talk to this server from Python in a very simple way::
+
+  from isabelle_client import get_isabelle_client_from_server_info
+  
+  isabelle = get_isabelle_client_from_server_info("server.pid")
+
+It might be useful to log all replies from the server somewhere, e.g.::
+
+    import logging
+    import sys
+
+    logger = logging.getLogger()
+    logger.addHandler(logging.StreamHandler(sys.stdout))
+    logger.setLevel(logging.INFO)
+    isabelle.logger = logger
+
+This client has several methods implemented to communicate with the server Python-style, e.g.::
+
+  isabelle.use_theories(theories=["dummy"], master_dir=".")
+
+One can also issue a free-form command, e.g.::
+
+  isabelle.execute_command("echo 42", asynchronous=False)

examples/dummy.thy

@@ -0,0 +1,6 @@
+theory dummy
+imports HOL.Nitpick
+begin
+lemma "1 ~= 0"
+oops
+end

examples/example.py

@@ -0,0 +1,39 @@
+"""
+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
+
+    http://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.
+"""
+import logging
+import sys
+
+from isabelle_client import get_isabelle_client_from_server_info
+
+
+def main():
+    """ using ``isabelle`` client """
+    # first, run Isabelle server in the same directory as this script:
+    # isabelle server > server.pid
+    isabelle = get_isabelle_client_from_server_info("server.pid")
+    # we will log all the messages from the server to stdout
+    logger = logging.getLogger()
+    logger.addHandler(logging.StreamHandler(sys.stdout))
+    logger.setLevel(logging.INFO)
+    isabelle.logger = logger
+    # now we can send a theory file from this directory to the server
+    # and get a response
+    isabelle.use_theories(theories=["dummy"], master_dir=".")
+    isabelle.execute_command("echo 42", asynchronous=False)
+
+
+if __name__ == "__main__":
+    main()

isabelle_client/__init__.py

@@ -13,5 +13,8 @@
 See the License for the specific language governing permissions and
 limitations under the License.
 """
-from isabelle_client.isabelle_client import IsabelleClient
+from isabelle_client.isabelle_client import (
+    IsabelleClient,
+    get_isabelle_client_from_server_info,
+)
 from isabelle_client.utils import IsabelleResponse