Leni Aniva: Pantograph

Stream: Lean Together 2025

[Jason Rute]

Discussion thread for the talk

[Jason Rute]

@Leni Aniva As for the question about the "tree structure" of proofs, you can extract that with for example @Kim Morrison's tool https://github.com/kim-em/lean-training-data
You can record things like where a tactic begins and ends, what the goal was before and after the tactic (note the same tactic may get run more than once because of tactic combinators like <;>), and the parent tactic. There may be multiple tree structures going on here including the proof tree and the syntax tree (which are not necessarily the same thing). I'm not exactly sure what tree the question was about, but I think you can record all of them.

[Jason Rute]

Good talk. It made me understand Pantograph a lot better.

[Leni Aniva]

Jason Rute said:

Leni Aniva As for the question about the "tree structure" of proofs, you can extract that with for example Kim Morrison's tool https://github.com/kim-em/lean-training-data
You can record things like where a tactic begins and ends, what the goal was before and after the tactic (note the same tactic may get run more than once because of tactic combinators like <;>), and the parent tactic. There may be multiple tree structures going on here including the proof tree and the syntax tree (which are not necessarily the same thing). I'm not exactly sure what tree the question was about, but I think you can record all of them.

Yes. The divergence between the syntax tree and proof tree is the primary reason why Pantograph doesn't have the feature of reading a proof tree directly from Lean code

[Bolton Bailey]

Is it possible to install PyPantograph with uv?

[Leni Aniva]

Bolton Bailey said:

Is it possible to install PyPantograph with uv?

probably, but pyp was not built with uv

[Bolton Bailey]

Ok, independently of that question, I am trying to install PyPantograph using the instructions here. I get the following:

~/Documents/MyDocuments/Professional/numina-all-files ..................................................................................................................................................................................... 17:59:33
> git clone https://github.com/stanford-centaur/PyPantograph.git
Cloning into 'PyPantograph'...
remote: Enumerating objects: 1703, done.
remote: Counting objects: 100% (313/313), done.
remote: Compressing objects: 100% (146/146), done.
remote: Total 1703 (delta 211), reused 208 (delta 167), pack-reused 1390 (from 2)
Receiving objects: 100% (1703/1703), 47.92 MiB | 15.92 MiB/s, done.
Resolving deltas: 100% (942/942), done.                                                                                                                                                                                                         /4.7s

~/Documents/MyDocuments/Professional/numina-all-files .................................................................................................................................................................................. 5s 17:59:49
> cd PyPantograph                                                                                                                                                                                                                               /0.0s

~/Documents/MyDocuments/Professional/numina-all-files/PyPantograph main ................................................................................................................................................................... 18:00:04
> poetry build

Creating virtualenv pantograph-eia5Nfbd-py3.10 in /Users/boltonbailey/Library/Caches/pypoetry/virtualenvs
Preparing build environment with build-system requirements poetry-core
Building pantograph (0.3.0)
  - Building sdist
  - Built pantograph-0.3.0.tar.gz
  - Building wheel
error: [root]: no configuration file with a supported extension:
././lakefile.lean
././lakefile.toml
Traceback (most recent call last):
  File "/Users/boltonbailey/Documents/MyDocuments/Professional/numina-all-files/PyPantograph/build-pantograph.py", line 15, in <module>
    shutil.copyfile(PATH_PANTOGRAPH / f".lake/build/bin/{repl_src}", path_executable)
  File "/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/shutil.py", line 254, in copyfile
    with open(src, 'rb') as fsrc:
FileNotFoundError: [Errno 2] No such file or directory: 'src/.lake/build/bin/repl'

Command '['/var/folders/93/qzgcbdz528j304066l79dqmw0000gn/T/tmp3kv9mog6/.venv/bin/python', 'build-pantograph.py']' returned non-zero exit status 1.                                                                                             /3.3s

~/Documents/MyDocuments/Professional/numina-all-files/PyPantograph main ................................................................................................................................................................ 3s 18:00:09
>

[Bolton Bailey]

Am I missing something here? Can Pantograph only be installed inside an existing lean project?

[Leni Aniva]

Did you read README.md?

[Bolton Bailey]

I see there are more instructions there which are not present in setup. Let me try running those.

[Bolton Bailey]

(It would be nice if the setup instructions also covered what's in the readme)

[Bolton Bailey]

Ok good news, looks like I got it installed and working with uv. However, I am getting the following error:

[Bolton Bailey]

    from pantograph import Server
ImportError: cannot import name 'Server' from 'pantograph' (/Users/boltonbailey/Documents/MyDocuments/Professional/numina-all-files/chain-of-thought/annotation-from-proof/scaffolding/.venv/lib/python3.10/site-packages/pantograph/__init__.py)

[Bolton Bailey]

(Hmm, perhaps uv installed the wrong version)

[Jesse Michael Han]

Hey Bolton, you might find this helpful: #Machine Learning for Theorem Proving > Serverless Pantograph on Morph Cloud @ 💬

This template is tested and gets a Lean environment + Pantograph installation set up with a pre-tested REST API wrapper, and it's easy to autoscale behind a load balancer. You can see more here: https://github.com/morph-labs/morphcloud-examples-public/tree/main/lean-server

[Bolton Bailey]

Further question, after setting up a repository on Lean v4.15 and using the line server = Server(project_path="./workspace-4-15/"), I am getting the error "AssertionError: Server failed to emit ready signal: ; This could be caused by Lean version mismatch between the project and Pantograph or insufficient timeout. " I see that the pantograph/ folder inside PyPantograph has a toolchain with v4.18.0, which seems to be generated by the build. Is there a way to build Pantograph at a lower version number?

[Leni Aniva]

Each Pantograph version only supports exactly one Lean version. I would have to explicitly backport Pantograph to v4.15.0 if you need it to work at v4.15.0.

[Bolton Bailey]

Ok, good to know, I may well be able to do most of what I want to do just using lean 4.18, so let me try that.