Setup

Install poetry. Then, run

poetry build

This builds a wheel of Pantograph in dist which can then be installed. For example, a downstream project could have this line in its pyproject.toml

pantograph = { file = "path/to/wheel/dist/pantograph-0.2.19-cp312-cp312-manylinux_2_40_x86_64.whl" }

To run the examples and experiments, setup a poetry shell:

poetry install
poetry shell

This drops the current shell into an environment where the development packages are available.

All interactions with Lean pass through the Server class. Create an instance with

from pantograph import Server
server = Server()

Lean Dependencies

The server created from Server() is sufficient for basic theorem proving tasks reliant on Lean’s Init library. Some users may find this insufficient and want to use non-builtin libraries such as Aesop or Mathlib4.

To use external Lean dependencies such as Mathlib4, Pantograph relies on an existing Lean repository. Instructions for creating this repository can be found here.

After creating this initial Lean repository, execute in the repository

lake build

to build all files from the repository. This step is necessary after any file in the repository is modified.

Then, feed the repository’s path to the server

server = Server(project_path="./path-to-lean-repo/")

For a complete example, see examples/.