Compare commits
No commits in common. "doc/rationale" and "dev" have entirely different histories.
doc/ration
...
dev
13
README.md
13
README.md
|
|
@ -7,8 +7,6 @@ A Machine-to-Machine interaction system for Lean 4.
|
||||||
Pantograph provides interfaces to execute proofs, construct expressions, and
|
Pantograph provides interfaces to execute proofs, construct expressions, and
|
||||||
examine the symbol list of a Lean project for machine learning.
|
examine the symbol list of a Lean project for machine learning.
|
||||||
|
|
||||||
See [documentations](doc/) for design rationale and references.
|
|
||||||
|
|
||||||
## Installation
|
## Installation
|
||||||
|
|
||||||
For Nix users, run
|
For Nix users, run
|
||||||
|
|
@ -17,9 +15,7 @@ nix build .#{sharedLib,executable}
|
||||||
```
|
```
|
||||||
to build either the shared library or executable.
|
to build either the shared library or executable.
|
||||||
|
|
||||||
Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
|
Install `elan` and `lake`, and run
|
||||||
run
|
|
||||||
|
|
||||||
``` sh
|
``` sh
|
||||||
lake build
|
lake build
|
||||||
```
|
```
|
||||||
|
|
@ -28,12 +24,9 @@ This builds the executable in `.lake/build/bin/pantograph-repl`.
|
||||||
## Executable Usage
|
## Executable Usage
|
||||||
|
|
||||||
``` sh
|
``` sh
|
||||||
pantograph-repl MODULES|LEAN_OPTIONS
|
pantograph MODULES|LEAN_OPTIONS
|
||||||
```
|
```
|
||||||
|
|
||||||
The `pantograph-repl` executable must be run with a list of modules to import.
|
|
||||||
It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
|
|
||||||
|
|
||||||
The REPL loop accepts commands as single-line JSON inputs and outputs either an
|
The REPL loop accepts commands as single-line JSON inputs and outputs either an
|
||||||
`Error:` (indicating malformed command) or a JSON return value indicating the
|
`Error:` (indicating malformed command) or a JSON return value indicating the
|
||||||
result of a command execution. The command can be passed in one of two formats
|
result of a command execution. The command can be passed in one of two formats
|
||||||
|
|
@ -44,6 +37,8 @@ command { ... }
|
||||||
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
|
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
|
||||||
empty command aborts the REPL.
|
empty command aborts the REPL.
|
||||||
|
|
||||||
|
The `pantograph` executable must be run with a list of modules to import. It can
|
||||||
|
also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
|
||||||
|
|
||||||
Example: (~5k symbols)
|
Example: (~5k symbols)
|
||||||
```
|
```
|
||||||
|
|
|
||||||
184
doc/icon.svg
184
doc/icon.svg
|
|
@ -4,17 +4,17 @@
|
||||||
<svg
|
<svg
|
||||||
width="256"
|
width="256"
|
||||||
height="256"
|
height="256"
|
||||||
viewBox="0 0 67.733332 67.733333"
|
viewBox="0 0 55.900957 55.900957"
|
||||||
version="1.1"
|
version="1.1"
|
||||||
id="svg1"
|
id="svg21534"
|
||||||
|
xml:space="preserve"
|
||||||
|
inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
|
||||||
sodipodi:docname="icon.svg"
|
sodipodi:docname="icon.svg"
|
||||||
inkscape:version="1.3.2 (091e20ef0f, 2023-11-25, custom)"
|
|
||||||
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||||
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||||
xmlns="http://www.w3.org/2000/svg"
|
xmlns="http://www.w3.org/2000/svg"
|
||||||
xmlns:svg="http://www.w3.org/2000/svg">
|
xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
|
||||||
<sodipodi:namedview
|
id="namedview21536"
|
||||||
id="namedview1"
|
|
||||||
pagecolor="#ffffff"
|
pagecolor="#ffffff"
|
||||||
bordercolor="#111111"
|
bordercolor="#111111"
|
||||||
borderopacity="1"
|
borderopacity="1"
|
||||||
|
|
@ -23,135 +23,51 @@
|
||||||
inkscape:pagecheckerboard="1"
|
inkscape:pagecheckerboard="1"
|
||||||
inkscape:deskcolor="#d1d1d1"
|
inkscape:deskcolor="#d1d1d1"
|
||||||
inkscape:document-units="px"
|
inkscape:document-units="px"
|
||||||
showguides="true"
|
showgrid="true"
|
||||||
inkscape:zoom="5.1882633"
|
inkscape:zoom="5.1754899"
|
||||||
inkscape:cx="81.819286"
|
inkscape:cx="158.82554"
|
||||||
inkscape:cy="132.22151"
|
inkscape:cy="91.682142"
|
||||||
inkscape:window-width="3774"
|
inkscape:window-width="3777"
|
||||||
inkscape:window-height="2126"
|
inkscape:window-height="2093"
|
||||||
inkscape:window-x="0"
|
inkscape:window-x="0"
|
||||||
inkscape:window-y="0"
|
inkscape:window-y="0"
|
||||||
inkscape:window-maximized="1"
|
inkscape:window-maximized="1"
|
||||||
inkscape:current-layer="layer2">
|
inkscape:current-layer="layer1"><inkscape:grid
|
||||||
<sodipodi:guide
|
type="xygrid"
|
||||||
position="33.866666,69.8437"
|
id="grid23833"
|
||||||
orientation="-1,0"
|
spacingx="3.4938098"
|
||||||
id="guide1"
|
spacingy="3.4938098"
|
||||||
inkscape:locked="false"
|
empspacing="4" /></sodipodi:namedview><defs
|
||||||
inkscape:label=""
|
id="defs21531" /><g
|
||||||
inkscape:color="rgb(0,134,229)" />
|
inkscape:label="Layer 1"
|
||||||
<sodipodi:guide
|
|
||||||
position="-27.673679,33.866666"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide2"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="16.933333,29.94582"
|
|
||||||
orientation="-1,0"
|
|
||||||
id="guide3"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="50.799999,37.44627"
|
|
||||||
orientation="-1,0"
|
|
||||||
id="guide4"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="31.336956,16.933333"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide5"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="24.528038,25.4"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide6"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="33.866666,50.799999"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide7"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="32.770414,55.033333"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide8"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="25.347689,33.866666"
|
|
||||||
orientation="1,0"
|
|
||||||
id="guide9"
|
|
||||||
inkscape:locked="false" />
|
|
||||||
<sodipodi:guide
|
|
||||||
position="25.347689,42.333333"
|
|
||||||
orientation="0,1"
|
|
||||||
id="guide10"
|
|
||||||
inkscape:locked="false"
|
|
||||||
inkscape:label=""
|
|
||||||
inkscape:color="rgb(0,134,229)" />
|
|
||||||
</sodipodi:namedview>
|
|
||||||
<defs
|
|
||||||
id="defs1" />
|
|
||||||
<g
|
|
||||||
inkscape:groupmode="layer"
|
inkscape:groupmode="layer"
|
||||||
id="layer4"
|
id="layer1"><rect
|
||||||
inkscape:label="bg" />
|
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
|
||||||
<g
|
id="rect26805"
|
||||||
inkscape:groupmode="layer"
|
width="11.502316"
|
||||||
id="layer1"
|
height="2.2512667"
|
||||||
inkscape:label="Circle">
|
x="33.344425"
|
||||||
<path
|
y="7.6690259"
|
||||||
id="path1"
|
ry="0.28140834"
|
||||||
style="fill:#666b98;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.0191989;stroke-miterlimit:3.4;fill-opacity:1"
|
rx="0.47926313" /><path
|
||||||
d="M 33.866666 0.009818522 A 33.857067 33.857067 0 0 0 0.009818522 33.866666 A 33.857067 33.857067 0 0 0 33.866666 67.723514 A 33.857067 33.857067 0 0 0 67.723514 33.866666 A 33.857067 33.857067 0 0 0 33.866666 0.009818522 z M 33.866666 4.2416015 A 29.624933 29.624933 0 0 1 63.491731 33.866666 A 29.624933 29.624933 0 0 1 33.866666 63.491731 A 29.624933 29.624933 0 0 1 4.2416015 33.866666 A 29.624933 29.624933 0 0 1 33.866666 4.2416015 z " />
|
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
|
||||||
</g>
|
d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
|
||||||
<g
|
id="path27381"
|
||||||
inkscape:groupmode="layer"
|
sodipodi:nodetypes="csccccscc" /><path
|
||||||
id="layer2"
|
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
|
||||||
inkscape:label="Pantograph-Core">
|
d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
|
||||||
<rect
|
id="path27479" /><path
|
||||||
style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
|
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
|
||||||
id="rect8"
|
d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
|
||||||
width="16.942858"
|
id="path27481" /><rect
|
||||||
height="4.2257233"
|
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
|
||||||
x="33.866665"
|
id="rect27483"
|
||||||
y="12.7"
|
width="36.38942"
|
||||||
rx="0.58070719"
|
height="3.6217353"
|
||||||
ry="0.34097314" />
|
x="13.953447"
|
||||||
<rect
|
y="43.009739"
|
||||||
style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
|
rx="0.43672624"
|
||||||
id="rect1"
|
ry="0.43672624" /><path
|
||||||
width="33.885715"
|
style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
|
||||||
height="8.4211359"
|
d="M -2.1119274,7.666599 H 64.179192"
|
||||||
x="16.933332"
|
id="path27487" /></g></svg>
|
||||||
y="42.333332"
|
|
||||||
rx="0.58070719"
|
|
||||||
ry="0.34097314" />
|
|
||||||
<path
|
|
||||||
style="fill:#666b98;fill-opacity:1;stroke:none;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
|
|
||||||
d="m 42.338095,16.925724 -16.990406,8.474275 13.121218,16.923808 -4.602241,0.0095 -4.254289,0.0015 -8.564029,-16.934789 17.310554,-8.464751 z"
|
|
||||||
id="path10"
|
|
||||||
sodipodi:nodetypes="cccccccc" />
|
|
||||||
<path
|
|
||||||
style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
|
|
||||||
d="M 46.53445,16.925724 26.018901,26.73418"
|
|
||||||
id="path11" />
|
|
||||||
<path
|
|
||||||
style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
|
|
||||||
d="m 21.048348,25.399999 4.352167,16.934808"
|
|
||||||
id="path12"
|
|
||||||
sodipodi:nodetypes="cc" />
|
|
||||||
</g>
|
|
||||||
</svg>
|
|
||||||
|
|
|
||||||
|
Before Width: | Height: | Size: 5.2 KiB After Width: | Height: | Size: 3.5 KiB |
|
|
@ -1,30 +0,0 @@
|
||||||
# Design Rationale
|
|
||||||
|
|
||||||
A great problem in machine learning is to use ML agents to automatically prove
|
|
||||||
mathematical theorems. This sort of proof necessarily involves *search*.
|
|
||||||
Compatibility for search is the main reason for creating Pantograph. The Lean 4
|
|
||||||
LSP interface is not conducive to search. Pantograph is designed with this in
|
|
||||||
mind. It emphasizes the difference between 3 views of a proof:
|
|
||||||
|
|
||||||
- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and
|
|
||||||
math papers are almost always written in this form.
|
|
||||||
- **Search View**: The view of a proof exploration trajectory. This is not
|
|
||||||
explicitly supported by Lean LSP.
|
|
||||||
- **Kernel View**: The proof viewed as a set of metavariables.
|
|
||||||
|
|
||||||
Pantograph enables proof agents to operate on the search view.
|
|
||||||
|
|
||||||
## Name
|
|
||||||
|
|
||||||
The name Pantograph is a pun. It means two things
|
|
||||||
- A pantograph is an instrument for copying down writing. As an agent explores
|
|
||||||
the vast proof search space, Pantograph records the current state to ensure
|
|
||||||
the proof is sound.
|
|
||||||
- A pantograph is also an equipment for an electric train. It supplies power to
|
|
||||||
a locomotive. In comparison the (relatively) simple Pantograph software powers
|
|
||||||
theorem proving projects.
|
|
||||||
|
|
||||||
## References
|
|
||||||
|
|
||||||
* [Pantograph Paper](https://arxiv.org/abs/2410.16429)
|
|
||||||
|
|
||||||
Loading…
Reference in New Issue