Basic usage example.

In what case to use

This client might be useful if:

• you have a machine with Isabelle installed

• you have scripts for automatic generation of theory files in Python

• you want to communicate with the server not using Scala and/or Standard ML

In what environment to use

The client works well in scripts and in Jupyter notebooks. For the latter, one has to enable nested event loops first. Please refer to nest_asyncio documentation.

Starting Isabelle server

First, we need to start an Isabelle server

from isabelle_client import start_isabelle_server

server_info, _ = start_isabelle_server(
    name="test", port=9999, log_file="server.log"
)

Warning

When using start_isabelle_server utility function in Python REPL or terminal IPython, shutting the server down within the same session is known to cause a runtime error on exit from the session. This behaviour is related to a well known issue.

We could also start the server outside this script and use its info (on Windows, this is done in Cygwin):

isabelle server

Interacting with Isabelle server

Let’s create a client to our server

from isabelle_client import get_isabelle_client

isabelle = get_isabelle_client(server_info)

We will log all the messages from the server to a file

import logging

isabelle.logger = logging.getLogger()
isabelle.logger.setLevel(logging.INFO)
isabelle.logger.addHandler(logging.FileHandler("session.log"))

Isabelle client supports all the commands implemented in Isabelle server

from pprint import pprint

pprint(isabelle.help())

[IsabelleResponse(response_type='OK',
                  response_body='{"isabelle_id":"b5f3d1051b13","isabelle_name":"Isabelle2023"}',
                  response_length=None),
 IsabelleResponse(response_type='OK',
                  response_body='["cancel","echo","help","purge_theories","session_build","session_start","session_stop","shutdown","use_theories"]',
                  response_length=118)]

Let’s suppose we have a Example.thy theory file in our working directory which we, e.g. generated with another Python script

theory Example
imports Main
begin
lemma "\<forall> x. \<exists> y. x = y"
by auto
end

We can send this theory file to the server and get a response

pprint(isabelle.use_theories(theories=["Example"], master_dir="."))

[IsabelleResponse(response_type='OK',
                  response_body='{"isabelle_id":"b5f3d1051b13","isabelle_name":"Isabelle2023"}',
                  response_length=None),
 IsabelleResponse(response_type='OK',
                  response_body='{"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5"}',
                  response_length=None),
 IsabelleResponse(response_type='NOTE',
                  response_body='{"percentage":14,"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5","message":"theory '
                                'Draft.Example '
                                '14%","kind":"writeln","session":"","theory":"Draft.Example"}',
                  response_length=161),
 IsabelleResponse(response_type='NOTE',
                  response_body='{"percentage":42,"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5","message":"theory '
                                'Draft.Example '
                                '42%","kind":"writeln","session":"","theory":"Draft.Example"}',
                  response_length=161),
 IsabelleResponse(response_type='NOTE',
                  response_body='{"percentage":99,"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5","message":"theory '
                                'Draft.Example '
                                '99%","kind":"writeln","session":"","theory":"Draft.Example"}',
                  response_length=161),
 IsabelleResponse(response_type='NOTE',
                  response_body='{"percentage":100,"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5","message":"theory '
                                'Draft.Example '
                                '100%","kind":"writeln","session":"","theory":"Draft.Example"}',
                  response_length=163),
 IsabelleResponse(response_type='FINISHED',
                  response_body='{"ok":true,"errors":[],"nodes":[{"messages":[{"kind":"writeln","message":"theorem '
                                '\\\\<forall>x. \\\\<exists>y. x = '
                                'y","pos":{"line":5,"offset":59,"end_offset":61,"file":"Example.thy"}}],"exports":[],"status":{"percentage":100,"unprocessed":0,"running":0,"finished":7,"failed":0,"total":7,"consolidated":true,"canceled":false,"ok":true,"warned":0},"theory_name":"Draft.Example","node_name":"Example.thy"}],"task":"9ea417a7-81c2-4a70-a6ee-e7da5ff58af5"}',
                  response_length=458)]

or we can build a session document using ./ROOT file

session examples = HOL +
  options [document = pdf, document_output = "output"]
  theories
    Example
  document_files
    "root.tex"

and ./document/root.tex file

\documentclass{article}
\usepackage{isabelle,isabellesym}
\begin{document}
\input{session}
\end{document}

import json

pprint(
    json.loads(
        isabelle.session_build(dirs=["."], session="examples")[
            -1
        ].response_body
    )
)

{'ok': True,
 'return_code': 0,
 'sessions': [{'ok': True,
               'return_code': 0,
               'session': 'Pure',
               'timeout': False,
               'timing': {'cpu': 0, 'elapsed': 0, 'gc': 0}},
              {'ok': True,
               'return_code': 0,
               'session': 'HOL',
               'timeout': False,
               'timing': {'cpu': 0, 'elapsed': 0, 'gc': 0}},
              {'ok': True,
               'return_code': 0,
               'session': 'examples',
               'timeout': False,
               'timing': {'cpu': 14.567, 'elapsed': 9.41, 'gc': 0}}],
 'task': 'e36e45b8-6f6b-42a7-9c95-3873b2fd9b89'}

One can also issue a free-form command, e.g.

import asyncio

pprint(asyncio.run(isabelle.execute_command("echo 42", asynchronous=False)))

[IsabelleResponse(response_type='OK',
                  response_body='{"isabelle_id":"b5f3d1051b13","isabelle_name":"Isabelle2023"}',
                  response_length=None),
 IsabelleResponse(response_type='OK', response_body='42', response_length=None)]

Finally, we can shut the server down.

pprint(isabelle.shutdown())

[IsabelleResponse(response_type='OK',
                  response_body='{"isabelle_id":"b5f3d1051b13","isabelle_name":"Isabelle2023"}',
                  response_length=None),
 IsabelleResponse(response_type='OK', response_body='', response_length=None)]