A Lean Machine-to-Machine Interface
Go to file
Leni Ven 2ec4efde55 Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
Pantograph Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
.gitignore Initial commit 2023-05-07 15:19:45 -07:00
Main.lean Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
Pantograph.lean Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
README.md Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
lakefile.lean Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
lean-toolchain Initial commit 2023-05-07 15:19:45 -07:00

README.md

Pantograph

An interaction system for Lean 4.

Installation

Install elan and lean4. Then, execute

lake build

In order to use mathlib, its binary must also be built

lake build Qq
lake build aesop
lake build std
lake build mathlib

Usage

The binary must be run inside a lake env environment.

Example: (~5k symbols)

$ lake env build/bin/Pantograph
{"cmd": "create", "payload": {"imports": ["Init"]}}
{"cmd": "catalog", "payload": {"id": 0}}

Example with mathlib (~90k symbols)

$ lake env build/bin/Pantograph
{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
{"cmd": "catalog", "payload": {"id": 0}}

Troubleshooting

If lean encounters stack overflow problems when printing catalog, execute this before running lean:

ulimit -s unlimited