update to include tracks, remove scoring on hf

.dockerignore

@@ -1,12 +1,10 @@
-PyPantograph/.venv
-PyPantograph/dist
-PyPantograph/pantograph/pantograph-repl
-PyPantograph/src/.lake
-lean-project-copy
-lean-project/.lake
-cslib/.lake
-cslib/.git
-cslib_docker_test
-**/__pycache__
-**/*.pyc
 .git
+.gitignore
+.gitattributes
+.claude
+CLAUDE.md
+__pycache__
+*.pyc
+.DS_Store
+README.md
+leaderboard.json

.gitattributes

@@ -36,3 +36,5 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 assets/icon.png filter=lfs diff=lfs merge=lfs -text
 assets/sponsors/cslib.png filter=lfs diff=lfs merge=lfs -text
 assets/sponsors/PhysLibLogo.jpeg filter=lfs diff=lfs merge=lfs -text
+assets/benchmarks/cslib.png filter=lfs diff=lfs merge=lfs -text
+assets/benchmarks/putnambench.png filter=lfs diff=lfs merge=lfs -text

.gitignore

@@ -7,23 +7,3 @@ gradio_cached_examples/
 flagged/
 leaderboard.json
 .leaderboard.*.json
-
-# Lean build artifacts — rebuilt inside the Docker image (lake cache get / build),
-# never pushed to the Space.
-lean-project/.lake/
-lean-project-copy/
-cslib/.lake/
-
-# Local cslib compilation-test scaffolding (Docker build contexts + logs).
-cslib_docker_test/build_ctx/
-cslib_docker_test/build_ctx_submit/
-cslib_docker_test/*.log
-
-# cslib files not needed by the Space (kept on disk, excluded from the repo).
-cslib/.github/
-cslib/.vscode/
-cslib/scripts/
-cslib/docs/
-cslib/eval_cslib_long.jsonl
-cslib/eval_cslib_long_optimized.jsonl
-cslib/make_eval_jsonl.py

Dockerfile

@@ -1,60 +1,19 @@
 FROM python:3.11-slim
 
-# System packages: curl for elan install, git for lake deps later, ca-certs for HTTPS
-RUN apt-get update && apt-get install -y --no-install-recommends \
-      curl ca-certificates git \
-    && rm -rf /var/lib/apt/lists/*
-
 RUN useradd -m -u 1000 user
 USER user
 ENV HOME=/home/user \
-    PATH=/home/user/.elan/bin:/home/user/.local/bin:$PATH
+    PATH=/home/user/.local/bin:$PATH
 
 WORKDIR $HOME/app
 
-# Python deps first (cached layer, rarely changes). uv is needed to build
-# PyPantograph's wheel (which triggers the poetry-core build hook that
-# compiles the pantograph-repl Lean binary).
-RUN pip install --no-cache-dir --user "gradio>=5,<6" "uv>=0.4"
-
-# Install elan (Lean toolchain manager). No default toolchain; the
-# project's `lean-toolchain` file controls the version.
-RUN curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-      | sh -s -- -y --default-toolchain none --no-modify-path
-
-# Copy the Lean project skeleton, materialize the toolchain, fetch Mathlib
-# source + transitive deps, and download pre-built oleans (~5 GB). All of
-# this is baked into a Docker layer so cold starts on HF are instant.
-COPY --chown=user lean-project /home/user/lean-project
-WORKDIR /home/user/lean-project
-RUN lake --version \
- && lake update \
- && lake exe cache get
+# UI-only image: all Lean compilation and scoring runs on a dedicated
+# evaluation worker that exchanges jobs/results with this Space through the
+# shared storage bucket mounted at /data. Nothing Lean-related is installed.
+RUN pip install --no-cache-dir --user "gradio>=5,<6"
 
-# Bake the CSLib project for path-bearing benchmark rows (compiled in place,
-# not in the empty lean-project). Fresh copy — `.lake` is excluded via
-# .dockerignore — so deps are materialized from the committed manifest, Mathlib
-# oleans are fetched, and the library is built here. app.py compiles
-# project-resident submissions against /home/user/cslib (CSLIB_PROJECT_ROOT).
-COPY --chown=user cslib /home/user/cslib
-WORKDIR /home/user/cslib
-RUN lake exe cache get \
- && lake build
-
-# Build PyPantograph: copy the source, invoke `uv build` which runs the
-# poetry-core build hook (build-pantograph.py → `lake build repl` inside
-# PyPantograph/src/) and packages the resulting binary into a wheel. Then
-# `pip install` that wheel into the user site-packages alongside gradio.
-COPY --chown=user PyPantograph /home/user/PyPantograph
-WORKDIR /home/user/PyPantograph
-RUN uv build \
- && pip install --no-cache-dir --user /home/user/PyPantograph/dist/pantograph-*.whl
-
-# App
-WORKDIR $HOME/app
-COPY --chown=user app.py utils.py benchmark.py leaderboard.py versions.py \
-                  pantograph_server.py project_compile.py \
-                  benchmark_data_new.jsonl benchmark_heartbeats.jsonl .
+COPY --chown=user app.py benchmark.py leaderboard.py contribution.md \
+                  benchmark_data_warmup.jsonl benchmark_heartbeats.jsonl .
 COPY --chown=user assets /home/user/app/assets
 
 EXPOSE 7860

PyPantograph/.github/workflows/doc.yaml

@@ -1,54 +0,0 @@
-name: deploy-doc
-
-on:
-  push:
-    branches:
-    - main
-
-# This job installs dependencies, builds the book, and pushes it to `gh-pages`
-jobs:
-  deploy-book:
-    runs-on: ubuntu-latest
-    permissions:
-      pages: write
-      id-token: write
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: true
-
-    - name: Install Python
-      uses: actions/setup-python@v4
-      with:
-        python-version: 3.11
-
-    - name: Install elan
-      run: |
-        set -o pipefail
-        curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-        ./elan-init -y --default-toolchain none
-        echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
-
-    - name: Install Lean
-      run: |
-        elan toolchain install $(<src/lean-toolchain)
-
-    - name: Install uv
-      run: |
-        curl -LsSf https://astral.sh/uv/install.sh | sh
-        uv sync
-
-    - name: Build documentations
-      run: |
-        uv run --group dev jupyter-book build doc
-
-    # Upload the book's HTML as an artifact
-    - name: Upload artifact
-      uses: actions/upload-pages-artifact@v3
-      with:
-        path: "doc/_build/html"
-
-    # Deploy the book's HTML to GitHub Pages
-    - name: Deploy to GitHub Pages
-      id: deployment
-      uses: actions/deploy-pages@v4

PyPantograph/.github/workflows/test.yaml

@@ -1,38 +0,0 @@
-name: Unit Tests
-on: [push]
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    permissions:
-      pages: write
-      id-token: write
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: true
-
-    - name: Install Python
-      uses: actions/setup-python@v4
-      with:
-        python-version: 3.11
-
-    - name: Install elan
-      run: |
-        set -o pipefail
-        curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-        ./elan-init -y --default-toolchain none
-        echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
-
-    - name: Install Lean
-      run: |
-        elan toolchain install $(<src/lean-toolchain)
-
-    - name: Install uv
-      run: |
-        curl -LsSf https://astral.sh/uv/install.sh | sh
-        uv sync
-
-    - name: Run tests
-      run: |
-        uv run pytest

PyPantograph/.gitignore

@@ -1,11 +0,0 @@
-.*
-!.gitignore
-!.github
-
-# Python
-*.py[cod]
-*.egg-info
-
-# Output
-/dist
-/venv

PyPantograph/LICENSE

@@ -1,190 +0,0 @@
-                                 Apache License
-                           Version 2.0, January 2004
-                        http://www.apache.org/licenses/
-
-   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
-
-   1. Definitions.
-
-      "License" shall mean the terms and conditions for use, reproduction,
-      and distribution as defined by Sections 1 through 9 of this document.
-
-      "Licensor" shall mean the copyright owner or entity authorized by
-      the copyright owner that is granting the License.
-
-      "Legal Entity" shall mean the union of the acting entity and all
-      other entities that control, are controlled by, or are under common
-      control with that entity. For the purposes of this definition,
-      "control" means (i) the power, direct or indirect, to cause the
-      direction or management of such entity, whether by contract or
-      otherwise, or (ii) ownership of fifty percent (50%) or more of the
-      outstanding shares, or (iii) beneficial ownership of such entity.
-
-      "You" (or "Your") shall mean an individual or Legal Entity
-      exercising permissions granted by this License.
-
-      "Source" form shall mean the preferred form for making modifications,
-      including but not limited to software source code, documentation
-      source, and configuration files.
-
-      "Object" form shall mean any form resulting from mechanical
-      transformation or translation of a Source form, including but
-      not limited to compiled object code, generated documentation,
-      and conversions to other media types.
-
-      "Work" shall mean the work of authorship, whether in Source or
-      Object form, made available under the License, as indicated by a
-      copyright notice that is included in or attached to the work
-      (an example is provided in the Appendix below).
-
-      "Derivative Works" shall mean any work, whether in Source or Object
-      form, that is based on (or derived from) the Work and for which the
-      editorial revisions, annotations, elaborations, or other modifications
-      represent, as a whole, an original work of authorship. For the purposes
-      of this License, Derivative Works shall not include works that remain
-      separable from, or merely link (or bind by name) to the interfaces of,
-      the Work and Derivative Works thereof.
-
-      "Contribution" shall mean any work of authorship, including
-      the original version of the Work and any modifications or additions
-      to that Work or Derivative Works thereof, that is intentionally
-      submitted to Licensor for inclusion in the Work by the copyright owner
-      or by an individual or Legal Entity authorized to submit on behalf of
-      the copyright owner. For the purposes of this definition, "submitted"
-      means any form of electronic, verbal, or written communication sent
-      to the Licensor or its representatives, including but not limited to
-      communication on electronic mailing lists, source code control systems,
-      and issue tracking systems that are managed by, or on behalf of, the
-      Licensor for the purpose of discussing and improving the Work, but
-      excluding communication that is conspicuously marked or otherwise
-      designated in writing by the copyright owner as "Not a Contribution."
-
-      "Contributor" shall mean Licensor and any individual or Legal Entity
-      on behalf of whom a Contribution has been received by Licensor and
-      subsequently incorporated within the Work.
-
-   2. Grant of Copyright License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      copyright license to reproduce, prepare Derivative Works of,
-      publicly display, publicly perform, sublicense, and distribute the
-      Work and such Derivative Works in Source or Object form.
-
-   3. Grant of Patent License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      (except as stated in this section) patent license to make, have made,
-      use, offer to sell, sell, import, and otherwise transfer the Work,
-      where such license applies only to those patent claims licensable
-      by such Contributor that are necessarily infringed by their
-      Contribution(s) alone or by combination of their Contribution(s)
-      with the Work to which such Contribution(s) was submitted. If You
-      institute patent litigation against any entity (including a
-      cross-claim or counterclaim in a lawsuit) alleging that the Work
-      or a Contribution incorporated within the Work constitutes direct
-      or contributory patent infringement, then any patent licenses
-      granted to You under this License for that Work shall terminate
-      as of the date such litigation is filed.
-
-   4. Redistribution. You may reproduce and distribute copies of the
-      Work or Derivative Works thereof in any medium, with or without
-      modifications, and in Source or Object form, provided that You
-      meet the following conditions:
-
-      (a) You must give any other recipients of the Work or
-          Derivative Works a copy of this License; and
-
-      (b) You must cause any modified files to carry prominent notices
-          stating that You changed the files; and
-
-      (c) You must retain, in the Source form of any Derivative Works
-          that You distribute, all copyright, patent, trademark, and
-          attribution notices from the Source form of the Work,
-          excluding those notices that do not pertain to any part of
-          the Derivative Works; and
-
-      (d) If the Work includes a "NOTICE" text file as part of its
-          distribution, then any Derivative Works that You distribute must
-          include a readable copy of the attribution notices contained
-          within such NOTICE file, excluding those notices that do not
-          pertain to any part of the Derivative Works, in at least one
-          of the following places: within a NOTICE text file distributed
-          as part of the Derivative Works; within the Source form or
-          documentation, if provided along with the Derivative Works; or,
-          within a display generated by the Derivative Works, if and
-          wherever such third-party notices normally appear. The contents
-          of the NOTICE file are for informational purposes only and
-          do not modify the License. You may add Your own attribution
-          notices within Derivative Works that You distribute, alongside
-          or as an addendum to the NOTICE text from the Work, provided
-          that such additional attribution notices cannot be construed
-          as modifying the License.
-
-      You may add Your own copyright statement to Your modifications and
-      may provide additional or different license terms and conditions
-      for use, reproduction, or distribution of Your modifications, or
-      for any such Derivative Works as a whole, provided Your use,
-      reproduction, and distribution of the Work otherwise complies with
-      the conditions stated in this License.
-
-   5. Submission of Contributions. Unless You explicitly state otherwise,
-      any Contribution intentionally submitted for inclusion in the Work
-      by You to the Licensor shall be under the terms and conditions of
-      this License, without any additional terms or conditions.
-      Notwithstanding the above, nothing herein shall supersede or modify
-      the terms of any separate license agreement you may have executed
-      with Licensor regarding such Contributions.
-
-   6. Trademarks. This License does not grant permission to use the trade
-      names, trademarks, service marks, or product names of the Licensor,
-      except as required for reasonable and customary use in describing the
-      origin of the Work and reproducing the content of the NOTICE file.
-
-   7. Disclaimer of Warranty. Unless required by applicable law or
-      agreed to in writing, Licensor provides the Work (and each
-      Contributor provides its Contributions) on an "AS IS" BASIS,
-      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-      implied, including, without limitation, any warranties or conditions
-      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
-      PARTICULAR PURPOSE. You are solely responsible for determining the
-      appropriateness of using or redistributing the Work and assume any
-      risks associated with Your exercise of permissions under this License.
-
-   8. Limitation of Liability. In no event and under no legal theory,
-      whether in tort (including negligence), contract, or otherwise,
-      unless required by applicable law (such as deliberate and grossly
-      negligent acts) or agreed to in writing, shall any Contributor be
-      liable to You for damages, including any direct, indirect, special,
-      incidental, or consequential damages of any character arising as a
-      result of this License or out of the use or inability to use the
-      Work (including but not limited to damages for loss of goodwill,
-      work stoppage, computer failure or malfunction, or any and all
-      other commercial damages or losses), even if such Contributor
-      has been advised of the possibility of such damages.
-
-   9. Accepting Warranty or Additional Liability. While redistributing
-      the Work or Derivative Works thereof, You may choose to offer,
-      and charge a fee for, acceptance of support, warranty, indemnity,
-      or other liability obligations and/or rights consistent with this
-      License. However, in accepting such obligations, You may act only
-      on Your own behalf and on Your sole responsibility, not on behalf
-      of any other Contributor, and only if You agree to indemnify,
-      defend, and hold each Contributor harmless for any liability
-      incurred by, or claims asserted against, such Contributor by reason
-      of your accepting any such warranty or additional liability.
-
-   END OF TERMS AND CONDITIONS
-
-   Copyright 2024 Leni Aniva
-
-   Licensed under the Apache License, Version 2.0 (the "License");
-   you may not use this file except in compliance with the License.
-   You may obtain a copy of the License at
-
-       http://www.apache.org/licenses/LICENSE-2.0
-
-   Unless required by applicable law or agreed to in writing, software
-   distributed under the License is distributed on an "AS IS" BASIS,
-   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-   See the License for the specific language governing permissions and
-   limitations under the License.

PyPantograph/README.md

@@ -1,77 +0,0 @@
-# PyPantograph
-
-[![arXiv](https://img.shields.io/badge/cs.LO-2410.16429-b31b1b?logo=arxiv&logoColor=red)](https://arxiv.org/abs/2410.16429)
-
-A Machine-to-Machine Interaction System for Lean 4.
-
-Features:
-- Programmatically execute tactics (`goal_tactic`)
-- Handling of metavariable coupling
-- Whole file specification conformity check (`check_track`)
-- Extraction of tactic invocation data
-- Inspection of Lean constants
-
-## Installation
-
-1. Install `uv`
-2. Install `elan`: See [Lean Manual](https://docs.lean-lang.org/lean4/doc/setup.html)
-
-### Install as a project dependency
-
-3. Add the package to your project:
-```sh
-uv add git+https://github.com/stanford-centaur/PyPantograph
-uv sync
-```
-
-### Build wheels from source
-
-3. Clone this repository with submodules:
-```sh
-git clone --recurse-submodules <repo-path>
-```
-4. Execute
-```sh
-cd <repo-path>
-uv build
-```
-5. Built wheels can be found at `dist/*.whl`
-
-## Documentation
-
-Build the documentations by
-```sh
-uv run --group dev jupyter-book build doc
-```
-Then serve
-```sh
-python3 -m http.server -d doc/_build/html
-```
-
-### Examples
-
-For API interaction examples, see `examples/README.md`.
-
-### Contributing
-
-Execute unit tests with
-
-```sh
-uv run pytest
-```
-
-## Reference
-
-[Paper Link](https://arxiv.org/abs/2410.16429)
-
-```bib
-@misc{pantograph,
-      title={Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4},
-      author={Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo},
-      year={2024},
-      eprint={2410.16429},
-      archivePrefix={arXiv},
-      primaryClass={cs.LO},
-      url={https://arxiv.org/abs/2410.16429},
-}
-```

PyPantograph/build-pantograph.py

@@ -1,25 +0,0 @@
-#!/usr/bin/env python3
-
-import subprocess, shutil, os, stat
-from pathlib import Path
-
-# -- Define paths for Pantograph source and Pantograph Python interface
-PATH_PANTOGRAPH = Path("./src")
-PATH_PY = Path("./pantograph")
-
-# -- Build the REPL
-with subprocess.Popen(["lake", "build", "repl"], cwd=PATH_PANTOGRAPH) as p:
-    p.wait()
-    if p.returncode != 0:
-        raise Exception(f"Error: 'lake build repl' failed with exit code {p.returncode}.")
-
-# -- Copy the REPL executable to the specified path
-path_executable = PATH_PY / "pantograph-repl"
-repl_src = "repl.exe" if os.name == "nt" else "repl"
-shutil.copyfile(PATH_PANTOGRAPH / f".lake/build/bin/{repl_src}", path_executable)
-
-# -- Make the REPL executable executable
-os.chmod(path_executable, os.stat(path_executable).st_mode | stat.S_IEXEC)
-
-# -- Copy the Lean toolchain file to the specified path
-shutil.copyfile(PATH_PANTOGRAPH / "lean-toolchain", PATH_PY / "lean-toolchain")

PyPantograph/doc/.gitignore

@@ -1 +0,0 @@
-/_build

PyPantograph/doc/_config.yml

@@ -1,71 +0,0 @@
-# Book settings
-# Learn more at https://jupyterbook.org/customize/config.html
-# Comprehensive example: https://github.com/executablebooks/jupyter-book/blob/master/docs/_config.yml
-
-title: PyPantograph
-author: Leni Aniva
-#logo: logo.png
-
-# Force re-execution of notebooks on each build.
-# See https://jupyterbook.org/content/execute.html
-execute:
-  execute_notebooks: 'off'
-
-# Define the name of the latex output file for PDF builds
-latex:
-  latex_documents:
-    targetname: book.tex
-
-# Add a bibtex file so that we can create citations
-#bibtex_bibfiles:
-#  - references.bib
-
-# Information about where the book exists on the web
-repository:
-  url: https://github.com/lenianiva/PyPantograph  # Online location of your book
-  path_to_book: docs  # Optional path to your book, relative to the repository root
-  branch: main  # Which branch of the repository should be used when creating links (optional)
-
-# Add GitHub buttons to your book
-# See https://jupyterbook.org/customize/config.html#add-a-link-to-your-repository
-html:
-  use_issues_button: true
-  use_repository_button: true
-
-sphinx:
-  config:
-    intersphinx_mapping:
-      ebp:
-        - "https://executablebooks.org/en/latest/"
-        - null
-      myst-parser:
-        - "https://myst-parser.readthedocs.io/en/latest/"
-        - null
-      myst-nb:
-        - "https://myst-nb.readthedocs.io/en/latest/"
-        - null
-      sphinx:
-        - "https://www.sphinx-doc.org/en/master"
-        - null
-      nbformat:
-        - "https://nbformat.readthedocs.io/en/latest"
-        - null
-      sd:
-        - "https://sphinx-design.readthedocs.io/en/latest"
-        - null
-      sphinxproof:
-        - "https://sphinx-proof.readthedocs.io/en/latest/"
-        - null
-    hoverxref_intersphinx:
-     - "sphinxproof"
-    mathjax3_config:
-      tex:
-        macros:
-          "N": "\\mathbb{N}"
-          "floor": ["\\lfloor#1\\rfloor", 1]
-          "bmat": ["\\left[\\begin{array}"]
-          "emat": ["\\end{array}\\right]"]
-
-  extra_extensions:
-    - sphinx.ext.intersphinx
-    - sphinx.ext.autodoc

PyPantograph/doc/_toc.yml

@@ -1,16 +0,0 @@
-format: jb-book
-root: intro
-parts:
-- caption: Features
-  chapters:
-  - file: setup
-  - file: goal
-  - file: agent-search
-  - file: frontend
-- caption: API Documentation
-  chapters:
-  - file: api-message
-  - file: api-server
-  - file: api-expr
-  - file: api-data
-  - file: api-search

PyPantograph/doc/agent-search.ipynb

@@ -1,155 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "markdown",
-   "id": "ec3abb52-d7cd-471f-b3b7-2d9681c79360",
-   "metadata": {},
-   "source": [
-    "# Search\n",
-    "\n",
-    "Pantograph supports basic proof search. In this case, Pantograph treats goals as nodes on an and-or tree. The user supplies an agent which should provide two functions:\n",
-    "\n",
-    "1. *Tactic*: Which tactic should be used on a goal?\n",
-    "2. *Guidance*: What is the search priority on a goal?\n",
-    "\n",
-    "The user agent should inherit from `pantograph.search.Agent`. Here is a brute force agent example:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "id": "959458f5-02e4-4f73-ae28-16a756aebed9",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "from typing import Optional\n",
-    "import collections\n",
-    "from pantograph import Server\n",
-    "from pantograph.search import Agent\n",
-    "from pantograph.expr import GoalState, Tactic"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 2,
-   "id": "8b402602-3ae5-43e4-9a62-2fa9e2c039fa",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "class DumbAgent(Agent):\n",
-    "\n",
-    "    def __init__(self):\n",
-    "        super().__init__()\n",
-    "\n",
-    "        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)\n",
-    "        self.intros = [\n",
-    "            \"intro\",\n",
-    "        ]\n",
-    "        self.tactics = [\n",
-    "            \"intro h\",\n",
-    "            \"cases h\",\n",
-    "            \"apply Or.inl\",\n",
-    "            \"apply Or.inr\",\n",
-    "        ]\n",
-    "        self.no_space_tactics = [\n",
-    "            \"assumption\",\n",
-    "        ]\n",
-    "\n",
-    "    def next_tactic(\n",
-    "            self,\n",
-    "            state: GoalState,\n",
-    "            goal_id: int,\n",
-    "    ) -> Optional[Tactic]:\n",
-    "        key = (state.state_id, goal_id)\n",
-    "        i = self.goal_tactic_id_map[key]\n",
-    "\n",
-    "        target = state.goals[goal_id].target\n",
-    "        if target.startswith('∀'):\n",
-    "            tactics = self.intros\n",
-    "        elif ' ' in target:\n",
-    "            tactics = self.tactics\n",
-    "        else:\n",
-    "            tactics = self.no_space_tactics\n",
-    "\n",
-    "        if i >= len(tactics):\n",
-    "            return None\n",
-    "\n",
-    "        self.goal_tactic_id_map[key] = i + 1\n",
-    "        return tactics[i]"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "665db9d0-5fff-4b26-9cea-32d06a6e1e04",
-   "metadata": {},
-   "source": [
-    "Execute the search with `agent.search`."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 3,
-   "id": "1c7961d1-b1fa-498c-ab75-16feb784ca2c",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16)"
-      ]
-     },
-     "execution_count": 3,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "server = Server()\n",
-    "agent = DumbAgent()\n",
-    "goal_state = server.goal_start(\"∀ (p q: Prop), Or p q -> Or q p\")\n",
-    "agent.search(server=server, goal_state=goal_state, verbose=False)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "141e0116-cbb6-4957-aaea-2a1100f80ece",
-   "metadata": {},
-   "source": [
-    "## Automatic and Manual Modes\n",
-    "\n",
-    "The agent chooses one goal and executes a tactic on this goal. What happens to the other goals that are not chosen? By default, the server runs in automatic mode. In automatic mode, all other goals are automatically inherited by a child state, so a user agent could declare a proof finished when there are no more goals remaining in the current goal state.\n",
-    "\n",
-    "Some users may wish to handle sibling goals manually. For example, Aesop's treatment of metavariable coupling is not automatic. To do this, pass the flag `options={ \"automaticMode\" : False }` to the `Server` constructor."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "2090e538-d196-4923-937c-b83fedf1d9a2",
-   "metadata": {},
-   "outputs": [],
-   "source": []
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Python 3 (ipykernel)",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.12.6"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}

PyPantograph/doc/api-data.rst

@@ -1,5 +0,0 @@
-Data
-=============
-
-.. automodule:: pantograph.data
-    :members:

PyPantograph/doc/api-expr.rst

@@ -1,8 +0,0 @@
-Expr
-=============
-
-.. automodule:: pantograph.expr
-    :members:
-
-.. autodata:: pantograph.expr.Expr
-.. autodata:: pantograph.expr.Tactic

PyPantograph/doc/api-message.rst

@@ -1,5 +0,0 @@
-Message
-=============
-
-.. automodule:: pantograph.message
-    :members:

PyPantograph/doc/api-search.rst

@@ -1,5 +0,0 @@
-Search
-=============
-
-.. automodule:: pantograph.search
-    :members:

PyPantograph/doc/api-server.rst

@@ -1,5 +0,0 @@
-Server
-=============
-
-.. automodule:: pantograph.server
-    :members:

PyPantograph/doc/frontend.ipynb

@@ -1,401 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "markdown",
-   "id": "fe7a3037-5c49-4097-9a5d-575b958cc7f8",
-   "metadata": {},
-   "source": [
-    "# Data Extraction"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "id": "fc68ad1d-e64c-48b7-9461-50d872d30473",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "import os\n",
-    "from pathlib import Path\n",
-    "from pantograph.server import Server"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "fd13c644-d731-4f81-964e-584bbd43e51c",
-   "metadata": {},
-   "source": [
-    "## Tactic Invocation\n",
-    "\n",
-    "Pantograph can extract tactic invocation data from a Lean file. A **tactic\n",
-    "invocation** is a tuple containing the before and after goal states, and the\n",
-    "tactic which converts the \"before\" state to the \"after\" state.\n",
-    "\n",
-    "To extract tactic invocation data, use `server.tactic_invocations(file_name)`\n",
-    "and supply the file name of the input Lean file."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 2,
-   "id": "6282dc6f-4eac-4263-8277-9d54d19ad1a5",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "$PWD: /Users/aniva/Projects/matp/PyPantograph/examples/Example\n"
-     ]
-    }
-   ],
-   "source": [
-    "project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'\n",
-    "print(f\"$PWD: {project_path}\")\n",
-    "server = await Server.create(imports=['Example'], project_path=project_path)\n",
-    "units = await server.tactic_invocations_async(project_path / \"Example.lean\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "c3c1be91-27a5-4481-b09d-a32dbb94b058",
-   "metadata": {},
-   "source": [
-    "The function returns a list of `CompilationUnit` objects, corresponding to each compilation unit in the input Lean file. For performance reasons only the text boundaries are loaded into `CompilationUnit`s."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 3,
-   "id": "e994aa2b-5d5e-4f86-af6c-40e0b3a032d2",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "#0: [14,85]\n",
-      "/-- Ensure that Aesop is running -/\n",
-      "example : α → α :=\n",
-      "  by aesop\n",
-      "\n",
-      "\n",
-      "#1: [85,254]\n",
-      "example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
-      "  intro p q h\n",
-      "  -- Here are some comments\n",
-      "  cases h\n",
-      "  . apply Or.inr\n",
-      "    assumption\n",
-      "  . apply Or.inl\n",
-      "    assumption\n",
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "with open(project_path / \"Example.lean\", 'rb') as f:\n",
-    "    content = f.read()\n",
-    "    for i, unit in enumerate(units):\n",
-    "        print(f\"#{i}: [{unit.i_begin},{unit.i_end}]\")\n",
-    "        unit_text = content[unit.i_begin:unit.i_end].decode('utf-8')\n",
-    "        print(unit_text)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "52e650fc-4a87-445f-8aa8-707ed9e36c03",
-   "metadata": {},
-   "source": [
-    "Each `CompilationUnit` includes a list of `TacticInvocation`s, which contains the `.before` (corresponding to the state before the tactic), `.after` (corresponding to the state after the tactic), and `.tactic` (tactic executed) fields. "
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 4,
-   "id": "8e0f0def-dd3c-4550-8a7c-b4aec6c7fd7f",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[Before]\n",
-      "α : Sort ?u.7\n",
-      "⊢ α → α\n",
-      "[Tactic]\n",
-      "aesop (using [])\n",
-      "[After]\n",
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "for i in units[0].invocations:\n",
-    "    print(f\"[Before]\\n{i.before}\")\n",
-    "    print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
-    "    print(f\"[After]\\n{i.after}\")"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 5,
-   "id": "51f5398b-5416-4dc1-81cd-6d2514758232",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[Before]\n",
-      "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
-      "[Tactic]\n",
-      "intro p q h (using [])\n",
-      "[After]\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "[Before]\n",
-      "p q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ q ∨ p\n",
-      "[Tactic]\n",
-      "cases h (using ['Eq.refl', 'Or'])\n",
-      "[After]\n",
-      "case inl\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "case inr\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n",
-      "[Before]\n",
-      "case inl\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "[Tactic]\n",
-      "apply Or.inr (using ['Or.inr'])\n",
-      "[After]\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "[Before]\n",
-      "case inl.h\n",
-      "p q : Prop\n",
-      "h✝ : p\n",
-      "⊢ p\n",
-      "[Tactic]\n",
-      "assumption (using [])\n",
-      "[After]\n",
-      "\n",
-      "[Before]\n",
-      "case inr\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n",
-      "[Tactic]\n",
-      "apply Or.inl (using ['Or.inl'])\n",
-      "[After]\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "[Before]\n",
-      "case inr.h\n",
-      "p q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q\n",
-      "[Tactic]\n",
-      "assumption (using [])\n",
-      "[After]\n",
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "for i in units[1].invocations:\n",
-    "    print(f\"[Before]\\n{i.before}\")\n",
-    "    print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
-    "    print(f\"[After]\\n{i.after}\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "3a8b5b28-a012-4d83-a6a9-ed017a8e1fc2",
-   "metadata": {},
-   "source": [
-    "## Check Compilation\n",
-    "\n",
-    "Use `check_compile` to check if some Lean code compiles.\n",
-    "\n",
-    "Keep in mind that Lean compilation can execute arbitrary code."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 6,
-   "id": "87e99da0-6e16-48c3-a462-1bfacb0d0cc7",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "[CompilationUnit(i_begin=0, i_end=31, messages=[], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None)]"
-      ]
-     },
-     "execution_count": 6,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "server = await Server.create()\n",
-    "code = \"\"\"\n",
-    "example : 1 + 1 = 2 := by rfl\n",
-    "\"\"\"\n",
-    "await server.check_compile_async(code)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "adf0dee9-33de-4640-b35a-3e093e590963",
-   "metadata": {},
-   "source": [
-    "If there are no error messages, it means the unit compiles."
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "14e42793-e177-447b-89d3-edb16931f6e9",
-   "metadata": {},
-   "source": [
-    "## Loading Definitions\n",
-    "\n",
-    "Pantograph keeps track of a global environment. `Server.load_definitions` adds new definitions to the environment."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 7,
-   "id": "9d322474-6a6e-4c32-945b-9e7942b78826",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "{'type': {'pp': 'Nat → Nat'},\n",
-       " 'sourceStart': {'line': 2, 'column': 0},\n",
-       " 'sourceEnd': {'line': 2, 'column': 42},\n",
-       " 'isUnsafe': False}"
-      ]
-     },
-     "execution_count": 7,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "code = \"\"\"\n",
-    "def mystery : Nat -> Nat := fun x => x + 1\n",
-    "\"\"\"\n",
-    "await server.load_definitions_async(code)\n",
-    "await server.env_inspect_async(\"mystery\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "93536793-c7df-4caa-bd03-74fd3b97d987",
-   "metadata": {},
-   "source": [
-    "## Track Checking\n",
-    "\n",
-    "We can check if one file conforms to the definition and theorems of another. If the result object has no `failure`s or error messages, the check has passed."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 8,
-   "id": "67aa959c-3c7c-4844-9ffb-9b730ae07f8a",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "CheckTrackResult(src_messages=[], dst_messages=[], failure=None)"
-      ]
-     },
-     "execution_count": 8,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "src = \"\"\"\n",
-    "def f : Nat -> Nat := sorry\n",
-    "theorem property (n : Nat) : f n = n + 1 := sorry\n",
-    "\"\"\"\n",
-    "dst = \"\"\"\n",
-    "def f (x : Nat) := x + 1\n",
-    "theorem property (n : Nat) : f n = n + 1 := rfl\n",
-    "\"\"\"\n",
-    "await server.check_track_async(src, dst)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 9,
-   "id": "5d56a22d-feb8-4d3b-bd5b-4f675991a550",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "CheckTrackResult(src_messages=[], dst_messages=[], failure='Type clash of property')"
-      ]
-     },
-     "execution_count": 9,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "src = \"\"\"\n",
-    "def f : Nat -> Nat := sorry\n",
-    "theorem property (n : Nat) : f n = n + 1 := sorry\n",
-    "\"\"\"\n",
-    "# Tampering!\n",
-    "dst = \"\"\"\n",
-    "def f (x : Nat) := x + 1\n",
-    "theorem property (n : Nat) : 0 = 0 := rfl\n",
-    "\"\"\"\n",
-    "await server.check_track_async(src, dst)"
-   ]
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Python 3 (ipykernel)",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.12.7"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}

PyPantograph/doc/goal.ipynb

@@ -1,662 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "markdown",
-   "id": "c5106980-4850-4bea-a333-5a1b2e4d1dc5",
-   "metadata": {},
-   "source": [
-    "# Goals and Tactics\n",
-    "\n",
-    "Executing tactics in Pantograph is simple. To start a proof, call the\n",
-    "`Server.goal_start` function and supply an expression."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 1,
-   "id": "3257de2b-41ca-4cfe-b66c-1ef4781c98b0",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "from pantograph import Server\n",
-    "from pantograph.expr import Site, TacticHave, TacticExpr, TacticMode"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 2,
-   "id": "6783d478-d8c7-4c4e-a56e-8170384297ef",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "server = await Server.create()\n",
-    "state0 = await server.goal_start_async(\"forall (p q: Prop), Or p q -> Or q p\")"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "bfe5a9df-33c2-4538-a9ce-fc0e02c92ff2",
-   "metadata": {},
-   "source": [
-    "This creates a *goal state*, which consists of some goals. In this\n",
-    "case since it is the beginning of a state, it has only one goal."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 3,
-   "id": "eefc9094-9574-4f92-9aa2-c39beb85389b",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n",
-      "⊢ forall (p q: Prop), Or p q -> Or q p\n"
-     ]
-    }
-   ],
-   "source": [
-    "print(state0)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "26dbe212-e09e-42dd-ab15-65ee2fba6234",
-   "metadata": {},
-   "source": [
-    "To execute a tactic on a goal state, use `Server.goal_tactic`. This function\n",
-    "takes a state, a tactic, and an optional site (see below). Most Lean tactics are strings."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 4,
-   "id": "c907dbb6-4d6a-4aa7-b173-60220165ba9e",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "a : Prop\n",
-      "⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
-     ]
-    }
-   ],
-   "source": [
-    "state1 = await server.goal_tactic_async(state0, \"intro a\")\n",
-    "print(state1)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "9978fdcf-a12b-4f22-9551-5e04c262e5e0",
-   "metadata": {},
-   "source": [
-    "Executing a tactic produces a new goal state. If this goal state has no goals,\n",
-    "the proof is complete. You can recover the usual form of a goal with `str()`"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 5,
-   "id": "16595c5e-2285-49d5-8340-397ad1e6c9e7",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "a : Prop\n",
-      "⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
-     ]
-    }
-   ],
-   "source": [
-    "print(state1.goals[0])"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "837dae74-b2d7-4e81-a318-86641dd016f9",
-   "metadata": {},
-   "source": [
-    "Starting in v0.3.5, you can run multiple tactics in one shot. Use `?_` to mark goals to be solved later."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 6,
-   "id": "6c70dbe0-e7ad-4bc2-bafe-0e59d78ccd3a",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "inl\n",
-      "p : Prop\n",
-      "q : Prop\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "inr\n",
-      "p : Prop\n",
-      "q : Prop\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n"
-     ]
-    }
-   ],
-   "source": [
-    "state2 = await server.goal_tactic_async(state0, \"intro p q\\nintro h\\ncases h\")\n",
-    "print(state2)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 7,
-   "id": "529edf1a-27bc-45a2-bbac-01e8756310a2",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "refine_2.inl\n",
-      "p : Prop\n",
-      "q : Prop\n",
-      "random : 1 + 1 = 2\n",
-      "h✝ : p\n",
-      "⊢ q ∨ p\n",
-      "refine_2.inr\n",
-      "p : Prop\n",
-      "q : Prop\n",
-      "random : 1 + 1 = 2\n",
-      "h✝ : q\n",
-      "⊢ q ∨ p\n",
-      "refine_1\n",
-      "p : Prop\n",
-      "q : Prop\n",
-      "h : p ∨ q\n",
-      "⊢ 1 + 1 = 2\n"
-     ]
-    }
-   ],
-   "source": [
-    "state2 = await server.goal_tactic_async(state0, \"intro p q h\\nhave random : 1 + 1 = 2 := ?_\\ncases h\")\n",
-    "print(state2)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "67f2a75d-6851-4393-bac9-a091400f1906",
-   "metadata": {},
-   "source": [
-    "## Error Handling and GC\n",
-    "\n",
-    "When a tactic fails, it throws an exception (`TacticFailure`) which contains a list of either `str`s or `Message` objects in `e.args[0]`."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 8,
-   "id": "c9784ba2-3810-4f80-a6c4-33d5eef3003e",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[Message(data=\"tactic 'assumption' failed\\na : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a\", pos=Position(line=0, column=0), pos_end=None, severity=<Severity.ERROR: 3>, kind=None)]\n",
-      "0:0: error: tactic 'assumption' failed\n",
-      "a : Prop\n",
-      "⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
-     ]
-    }
-   ],
-   "source": [
-    "from pantograph.message import TacticFailure\n",
-    "try:\n",
-    "    state2 = await server.goal_tactic_async(state1, \"assumption\")\n",
-    "    print(\"Should not reach this\")\n",
-    "except TacticFailure as e:\n",
-    "    print(e)\n",
-    "    for msg in e.args[0]:\n",
-    "        print(msg)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "1ae60d9e-8656-4f26-b495-d04bced250fc",
-   "metadata": {},
-   "source": [
-    "A state with no goals is considered solved"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 9,
-   "id": "1cb96b19-d3bb-4533-abeb-a7dbc5bc8c3e",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "GoalState(#7, goals=[], _sentinel=#4"
-      ]
-     },
-     "execution_count": 9,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state0 = await server.goal_start_async(\"forall (p : Prop), p -> p\")\n",
-    "state1 = await server.goal_tactic_async(state0, \"intro\")\n",
-    "state2 = await server.goal_tactic_async(state1, \"intro h\")\n",
-    "state3 = await server.goal_tactic_async(state2, \"exact h\")\n",
-    "state3"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "a2945e71-e583-4ae0-9c0f-83035f0492f2",
-   "metadata": {},
-   "source": [
-    "Execute `server.gc()` once in a while to delete unused goals."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 10,
-   "id": "d53624ff-c720-4847-98f7-28e109eb76e7",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "await server.gc_async()"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "0b59e05e-7d8c-4fad-b8ca-375ea995ea5b",
-   "metadata": {},
-   "source": [
-    "## Special Tactics\n",
-    "\n",
-    "Lean has special provisions for some tactics. This includes `have`, `let`,\n",
-    "`calc`. To execute one of these tactics, create a `TacticHave`, `TacticLet`,\n",
-    "instance and feed it into `server.goal_tactic`.\n",
-    "\n",
-    "Technically speaking `have` and `let` are not tactics in Lean, so their execution requires special attention. In v0.3.5, they can be run under the normal tactic function as well (see above)."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 11,
-   "id": "526d620b-064f-4ec0-a7b2-6a1ef3c6f6e7",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n",
-      "⊢ 2 = 1 + 1\n",
-      "h : 2 = 1 + 1\n",
-      "⊢ 1 + 1 = 2\n"
-     ]
-    }
-   ],
-   "source": [
-    "state0 = await server.goal_start_async(\"1 + 1 = 2\")\n",
-    "state1 = await server.goal_tactic_async(state0, TacticHave(branch=\"2 = 1 + 1\", binder_name=\"h\"))\n",
-    "print(state1)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "c415d436-ed0d-475f-bf5e-b8dc63954c7e",
-   "metadata": {},
-   "source": [
-    "The `TacticExpr` \"tactic\" parses an expression and assigns it to the current\n",
-    "goal.  This leverages Lean's type unification system and is as expressive as\n",
-    "Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression\n",
-    "and tactic forms."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 12,
-   "id": "e1f06441-4d77-45a7-a1c3-b800b96a8105",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "state0 = await server.goal_start_async(\"forall (p : Prop), p -> p\")\n",
-    "state1 = await server.goal_tactic_async(state0, \"intro p\")\n",
-    "state2 = await server.goal_tactic_async(state1, TacticExpr(\"fun h => h\"))\n",
-    "print(state2)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "2ed8ea8f-708d-4d30-a7c4-fae20f07fd91",
-   "metadata": {},
-   "source": [
-    "### Drafting\n",
-    "\n",
-    "Pantograph supports drafting (technically the sketch step) from\n",
-    "[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).\n",
-    "Pantograph's drafting feature is more powerful. At any place in the proof, you\n",
-    "can replace an expression with `sorry`, and the `sorry` will become a goal. Any type errors will also become goals. In order to detect whether type errors have occurred, the user can look at the messages from each compilation unit.\n",
-    "\n",
-    "At this point we must introduce the idea of compilation units. Each Lean\n",
-    "definition, theorem, constant, etc., is a *compilation unit*. When Pantograph\n",
-    "extracts data from Lean source code, it sections the data into these compilation\n",
-    "units.\n",
-    "\n",
-    "For example, consider this sketch produced by a language model prover:\n",
-    "```lean\n",
-    "by\n",
-    "   intros n m\n",
-    "   induction n with\n",
-    "   | zero =>\n",
-    "     have h_base: 0 + m = m := sorry\n",
-    "     have h_symm: m + 0 = m := sorry\n",
-    "     sorry\n",
-    "   | succ n ih =>\n",
-    "     have h_inductive: n + m = m + n := sorry\n",
-    "     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n",
-    "     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n",
-    "     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry\n",
-    "     sorry\n",
-    "```\n",
-    "There are some `sorry`s that we want to solve automatically with hammer tactics. We can do this by drafting.\n",
-    "\n",
-    "Pantograph can also load `sorry`s from a code snippet, which provides an alternative way for proof initiation. Warning: `load_sorry` does not work with `example` declarations."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 13,
-   "id": "e435456b-892a-42e7-a8a9-4968c8202c83",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n",
-      "⊢ ∀ (n m : Nat), n + m = m + n\n"
-     ]
-    }
-   ],
-   "source": [
-    "sketch = \"\"\"\n",
-    "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry\n",
-    "\"\"\"\n",
-    "unit, = await server.load_sorry_async(sketch)\n",
-    "print(unit.goal_state)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 14,
-   "id": "efce284c-35d0-453f-9857-aebe7b09bf3e",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "n : Nat\n",
-      "m : Nat\n",
-      "⊢ 0 + m = m\n",
-      "n : Nat\n",
-      "m : Nat\n",
-      "h_base : 0 + m = m\n",
-      "⊢ m + 0 = m\n",
-      "n : Nat\n",
-      "m : Nat\n",
-      "h_base : 0 + m = m\n",
-      "h_symm : m + 0 = m\n",
-      "⊢ 0 + m = m + 0\n",
-      "n✝ : Nat\n",
-      "m : Nat\n",
-      "n : Nat\n",
-      "ih : n + m = m + n\n",
-      "⊢ n + 1 + m = m + (n + 1)\n"
-     ]
-    }
-   ],
-   "source": [
-    "step = \"\"\"\n",
-    "by\n",
-    "   -- Consider some n and m in Nats.\n",
-    "   intros n m\n",
-    "   -- Perform induction on n.\n",
-    "   induction n with\n",
-    "   | zero =>\n",
-    "     -- Base case: When n = 0, we need to show 0 + m = m + 0.\n",
-    "     -- We have the fact 0 + m = m by the definition of addition.\n",
-    "     have h_base: 0 + m = m := sorry\n",
-    "     -- We also have the fact m + 0 = m by the definition of addition.\n",
-    "     have h_symm: m + 0 = m := sorry\n",
-    "     -- Combine facts to close goal\n",
-    "     sorry\n",
-    "   | succ n ih =>\n",
-    "     sorry\n",
-    "\"\"\"\n",
-    "from pantograph.expr import TacticDraft\n",
-    "tactic = TacticDraft(step)\n",
-    "state1 = await server.goal_tactic_async(unit.goal_state, tactic)\n",
-    "print(state1)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "2cb11505-4076-481f-8736-e0d6d4e67ffc",
-   "metadata": {},
-   "source": [
-    "### Search Target Distillation\n",
-    "\n",
-    "Sometimes, we want to search for an object (witness) along with proofs (companions) of properties about the object. This problem is known as **companion generation**. In Pantograph, `load_sorry` will automatically pair companions to create coupled search targets. Note that this is only available for flat dependency structures, where one object has a list of properties."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 15,
-   "id": "d66afe22-541e-4464-86ce-b462272d76d2",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n",
-      "⊢ { f // ∀ (n : Nat), f n = n + 1 }\n"
-     ]
-    }
-   ],
-   "source": [
-    "sketch = \"\"\"\n",
-    "def f : Nat -> Nat := sorry\n",
-    "theorem property (n : Nat) : f n = n + 1 := sorry\n",
-    "\"\"\"\n",
-       "target, = await server.load_sorry_async(sketch, ignore_values=True)\n",
-    "print(target.goal_state)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "efabd1ad-88aa-4bc1-90ac-2d7af58d9a07",
-   "metadata": {},
-   "source": [
-    "## Sites\n",
-    "\n",
-    "The optional `site` argument to `goal_tactic` controls the area of effect of a tactic. Site controls what the tactic sees when it asks Lean for the current goal. Most tactics only act on a single goal, but tactics acting on multiple goals are plausible as well.\n",
-    "\n",
-    "The `auto_resume` field defaults to the server option's `automaticMode` (which defaults to `True`). When this field is true, Pantograph will not deliberately hide other goals away from the tactic. This is the usual modus operandi of tactic proofs in Lean. When `auto_resume` is set to `False`, Pantograph will set other goals to dormant. This can be useful in limiting the area of effect of a tactic. However, dormanting a goal comes with the extra burden that it has to be activated (\"resume\") later, via `goal_resume`."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 16,
-   "id": "6806db59-bf2e-4c72-9903-200621ec1661",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "left\n",
-      "p : Prop\n",
-      "h : p\n",
-      "⊢ p\n",
-      "right\n",
-      "p : Prop\n",
-      "h : p\n",
-      "⊢ p ∨ p\n"
-     ]
-    }
-   ],
-   "source": [
-    "state = await server.goal_start_async(\"forall (p : Prop), p -> And p (Or p p)\")\n",
-    "state = await server.goal_tactic_async(state, \"intro p h\")\n",
-    "state = await server.goal_tactic_async(state, \"apply And.intro\")\n",
-    "print(state)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "4e2f9539-bac0-4721-9f86-752090f3ed24",
-   "metadata": {},
-   "source": [
-    "In the example below, we set `auto_resume` to `False`, and the sibling goal is dormanted."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 17,
-   "id": "aebb6f3d-e2b2-4104-8d67-5adce5d2ea78",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "\n"
-     ]
-    }
-   ],
-   "source": [
-    "state1 = await server.goal_tactic_async(state, \"exact h\", site=Site(goal_id=0, auto_resume=False))\n",
-    "print(state1)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "a1db5a24-1f98-47f6-ab26-d00e94d3b57f",
-   "metadata": {},
-   "source": [
-    "In the example below, we preferentially operate on the second goal. Note that the first goal is still here."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 18,
-   "id": "cb0e30db-f7fd-49df-82a9-09e2eeef2885",
-   "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "right.h\n",
-      "p : Prop\n",
-      "h : p\n",
-      "⊢ p\n",
-      "left\n",
-      "p : Prop\n",
-      "h : p\n",
-      "⊢ p\n"
-     ]
-    }
-   ],
-   "source": [
-    "state2 = await server.goal_tactic_async(state, \"apply Or.inl\", site=Site(goal_id=1))\n",
-    "print(state2)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "acd74351-e9d5-497c-af6f-fc5709edb54d",
-   "metadata": {},
-   "source": [
-    "## Tactic Modes\n",
-    "\n",
-    "Pantograph has special provisions for handling `conv` and `calc` tactics. The commonality of these tactics is incremental feedback: The tactic can run half way and produce some goal. Pantograph supports this via tactic modes. Every goal carries around with it a `TacticMode`, and the user is free to switch between modes. By default, the mode is `TacticMode.TACTIC`."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": 19,
-   "id": "30b85bc4-a4ff-4156-b0bb-5c3496bd9472",
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "GoalState(#24, goals=[Goal(id='_uniq.381', variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + 1 + 1', sibling_dep=None, name='calc', mode=<TacticMode.TACTIC: 1>), Goal(id='_uniq.400', variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='a + 1 + 1 = a + b', sibling_dep=None, name=None, mode=<TacticMode.CALC: 3>)], _sentinel=#14"
-      ]
-     },
-     "execution_count": 19,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "state = await server.goal_start_async(\"∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b\")\n",
-    "\n",
-    "state = await server.goal_tactic_async(state, \"intro a b h\")\n",
-    "state = await server.goal_tactic_async(state, TacticMode.CALC)\n",
-    "state = await server.goal_tactic_async(state, \"1 + a + 1 = a + 1 + 1\")\n",
-    "state"
-   ]
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Python 3 (ipykernel)",
-   "language": "python",
-   "name": "python3"
-  },
-  "language_info": {
-   "codemirror_mode": {
-    "name": "ipython",
-    "version": 3
-   },
-   "file_extension": ".py",
-   "mimetype": "text/x-python",
-   "name": "python",
-   "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython3",
-   "version": "3.12.7"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}

PyPantograph/doc/intro.md

@@ -1,79 +0,0 @@
-# Introduction
-
-This is Pantograph, an machine-to-machine interaction interface for Lean 4.
-Its main purpose is to train and evaluate theorem proving agents. The main
-features of Pantograph are:
-
-1. Writing mixed expression and tactic style proofs
-2. Exposing the minimum amount of information for a search agent
-3. Handling of metavariable coupling
-4. Reading/Adding symbols from the environment
-5. Extraction of tactic training data
-6. Drafting incomplete proofs
-
-## 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.
-
-## Design Rationale
-
-The Lean 4 interface is not conducive to search. Readers familiar with Coq may
-know that the Coq Serapi was superseded by CoqLSP. In the opinion of the
-authors, this is a mistake. An interface conducive for human operators to write
-proofs is often not an interface conductive to machine learning agents for
-searching.
-
-All of Pantograph's business logic is written in Lean, allowing coupling between
-the data extraction and proof search components.
-
-## Caveats and Limitations
-
-Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
-flexibility it offers.  To support tree search means Pantograph has to act
-differently from Lean in some times, but never at the sacrifice of soundness.
-
-- When Lean LSP says "don't know how to synthesize placeholder", this indicates
-  the human operator needs to manually move the cursor to the placeholder and
-  type in the correct expression. This error therefore should not halt the proof
-  process, and the placeholder should be turned into a goal.
-- When Lean LSP says "unresolved goals", that means a proof cannot finish where
-  it is supposed to finish at the end of a `by` block. Pantograph will raise the
-  error in this case, since it indicates the termination of a proof search branch.
-
-Pantograph cannot perform things that are inherently constrained by Lean. These
-include:
-
-- If a tactic loses track of metavariables, it will not be caught until the end
-  of the proof search. This is a bug in the tactic itself.
-- Lean's concurrency model is coöperative, which means a tactic is responsible
-  for checking a cancellation flag if it runs for a long time. Pantograph's
-  built-in timeout feature requires such behaviour. A tactic which hangs without
-  checking the flag cannot be timeouted.
-- Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system.
-
-Each Pantograph version is anchored to a Lean version specified in
-`src/lean-toolchain`. Features can be backported to older Lean versions upon
-request.
-
-## Referencing
-
-[Paper Link](https://arxiv.org/abs/2410.16429)
-
-```bib
-@misc{pantograph,
-      title={Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4},
-      author={Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo},
-      year={2024},
-      eprint={2410.16429},
-      archivePrefix={arXiv},
-      primaryClass={cs.LO},
-      url={https://arxiv.org/abs/2410.16429},
-}
-```

PyPantograph/doc/setup.md

@@ -1,85 +0,0 @@
-# Setup
-
-1. Install `uv`
-2. Clone this repository with submodules:
-```sh
-git clone --recurse-submodules <repo-path>
-```
-3. Install `elan` and `lake`: See [Lean Manual](https://docs.lean-lang.org/lean4/doc/setup.html)
-4. Execute
-```sh
-cd <repo-path>
-uv sync
-```
-
-`uv build` 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`
-
-```toml
-pantograph = { file = "path/to/wheel/dist/pantograph-0.3.0-cp312-cp312-manylinux_2_40_x86_64.whl" }
-```
-
-All interactions with Lean pass through the `Server` class. Create an instance of Pantograph using
-```python
-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. In this case, feed in a
-list of module names via the `imports` parameter e.g. `imports=["Mathlib"]`. Due
-to inherent restrictions in Lean, importing a module that has not been imported
-before after the server has already started is not allowed and will trigger
-initializer exceptions. It may be possible to circumvent this if Lean relaxes
-this constraint.
-
-To use external Lean dependencies such as
-[Mathlib4](https://github.com/leanprover-community/mathlib4), Pantograph relies
-on an existing Lean repository. Instructions for creating this repository can be
-found [here](https://docs.lean-lang.org/lean4/doc/setup.html#lake).
-
-After creating this initial Lean repository, execute in the repository
-```sh
-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
-```python
-server = Server(project_path="./path-to-lean-repo/")
-```
-
-For a complete example, see `examples/`.
-
-## Server Parameters
-
-The server has some additional options.
-
-- `core_options`: These options are passed to Lean's kernel. For example
-  `set_option pp.all true` in Lean corresponds to passing `pp.all=true` to
-  `core_options`.
-- `options`: These options are given to Pantograph itself. See below.
-- `timeout`: This timeout controls the maximum wait time for the server
-  instance. If the server instance does not respond within this timeout limit,
-  it gets terminated. In some cases it is necessary to increase this if loading
-  a Lean project takes too long.
-
-A special note about running in Jupyter: Use the asynchronous version of each
-function.
-
-```python
-server = await Server.create()
-unit, = await server.load_sorry_async(sketch)
-print(unit.goal_state)
-```
-
-### Options
-
-- `automaticMode`: Set to false to disable automatic goal continuation.
-- `timeout`: Set to a positive integer to set tactic execution timeout.
-- `printDependentMVars`: Set to true to explicitly store goal inter-dependencies

PyPantograph/examples/Example/.gitignore

@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-packages/*

PyPantograph/examples/Example/Example.lean

@@ -1,14 +0,0 @@
-import Aesop
-
-/-- Ensure that Aesop is running -/
-example : α → α :=
-  by aesop
-
-example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
-  intro p q h
-  -- Here are some comments
-  cases h
-  . apply Or.inr
-    assumption
-  . apply Or.inl
-    assumption

PyPantograph/examples/Example/lake-manifest.json

@@ -1,25 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/aesop.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc4",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "Example",
- "lakeDir": ".lake"}

PyPantograph/examples/Example/lakefile.lean

@@ -1,10 +0,0 @@
-import Lake
-open Lake DSL
-
-require aesop from git
-  "https://github.com/leanprover-community/aesop.git" @ "v4.22.0"
-
-package Example
-
-@[default_target]
-lean_lib Example

PyPantograph/examples/Example/lean-toolchain

@@ -1 +0,0 @@
-../../src/lean-toolchain

PyPantograph/examples/README.md

@@ -1,24 +0,0 @@
-# Examples
-
-This example showcases how to bind library dependencies and execute the `Aesop`
-tactic in Lean. First build the example project:
-``` sh
-pushd Example
-lake build
-popd
-```
-This would generate compiled `.olean` files. Then run one of the examples from the
-project root:
-``` sh
-poetry run examples/aesop.py
-poetry run examples/sketch.py
-```
-
-Warning: If you make modifications to any Lean files, you must re-run `lake
-build`! Moreover, the version of the Lean used in the example folder (including
-dependencies in `lakefile.lean` and `lean-toolchain`) **must match exactly**
-with the version in `src/`!
-
-* `aesop.py`: Example of how to use the `aesop` tactic
-* `sketch.py`: Example of loading a sketch
-

PyPantograph/examples/aesop.py

@@ -1,14 +0,0 @@
-#!/usr/bin/env python3
-
-from pathlib import Path
-from pantograph.server import Server
-
-# This example shows how to use project dependencies
-
-if __name__ == '__main__':
-    project_path = Path(__file__).parent.resolve() / 'Example'
-    print(f"$PWD: {project_path}")
-    server = Server(imports=['Example'], project_path=project_path)
-    state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
-    state1 = server.goal_tactic(state0, tactic="aesop")
-    assert state1.is_solved

PyPantograph/examples/branch-sorry.py

@@ -1,13 +0,0 @@
-#!/usr/bin/env python3
-
-from pantograph.server import Server
-from pantograph.expr import TacticHave
-
-# This example shows what happens when a tactic generates a sorry.
-if __name__ == '__main__':
-    server = Server(imports=['Init'])
-    state0 = server.goal_start("1 = 0")
-    state1 = server.goal_tactic(state0, tactic=TacticHave("1 = 0"))
-    print(state1)
-    state1b = server.goal_tactic(state1, tactic="apply?")
-    print(state1b)

PyPantograph/examples/simple.py

@@ -1,7 +0,0 @@
-from pantograph.server import Server
-
-if __name__ == '__main__':
-    server = Server(imports=['Init'])
-    state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
-    state1 = server.goal_tactic(state0, tactic="intro")
-    print(state1)

PyPantograph/examples/sketch.py

@@ -1,41 +0,0 @@
-#!/usr/bin/env python3
-
-from pantograph.server import Server
-from pantograph.expr import TacticDraft
-
-root = """
-theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
-"""
-
-sketch = """
-by
-  -- Consider some n and m in Nats.
-  intros n m
-  -- Perform induction on n.
-  induction n with
-  | zero =>
-    sorry
-  | succ n ih =>
-    -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.
-    -- By the inductive hypothesis, we have n + m = m + n.
-    have h_inductive: n + m = m + n := sorry
-    -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.
-    have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry
-    -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.
-    have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry
-    -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.
-    have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry
-    -- Combine facts to close goal
-    sorry
-"""
-
-if __name__ == '__main__':
-    server = Server()
-    unit, = server.load_sorry(root)
-    print(unit.goal_state)
-
-    # Send the draft payload using `TacticDraft`
-    state1 = server.goal_tactic(
-        unit.goal_state,
-        tactic=TacticDraft(sketch))
-    print(state1)

PyPantograph/pantograph/.gitignore

@@ -1,2 +0,0 @@
-pantograph-repl
-lean-toolchain

PyPantograph/pantograph/__init__.py

@@ -1 +0,0 @@
-from pantograph.server import Server

PyPantograph/pantograph/data.py

@@ -1,113 +0,0 @@
-from pantograph.message import Severity, Message
-from pantograph.expr import GoalState
-
-from typing import Optional, Tuple
-from dataclasses import dataclass, field
-from enum import Enum
-
-@dataclass(frozen=True)
-class TacticInvocation:
-    """
-    One tactic invocation with the before/after goals extracted from Lean source
-    code.
-    """
-    before: str
-    after: str
-    tactic: str
-    used_constants: list[str]
-
-    @staticmethod
-    def parse(payload: dict):
-        return TacticInvocation(
-            before=payload["goalBefore"],
-            after=payload["goalAfter"],
-            tactic=payload["tactic"],
-            used_constants=payload.get('usedConstants', []),
-        )
-
-@dataclass(frozen=True)
-class CompilationUnit:
-
-    # Byte boundaries [begin, end[ of each compilation unit.
-    i_begin: int
-    i_end: int
-
-    messages: list[Message] = field(default_factory=lambda: [])
-
-    invocations: Optional[list[TacticInvocation]] = None
-    # If `goal_state` is none, maybe error has occurred. See `messages`
-    goal_state: Optional[GoalState] = None
-    goal_src_boundaries: Optional[list[Tuple[int, int]]] = None
-
-    new_constants: Optional[list[str]] = None
-
-    @staticmethod
-    def parse(payload: dict, goal_state_sentinel=None, invocations=None):
-        i_begin = payload["boundary"][0]
-        i_end = payload["boundary"][1]
-        messages = [Message.parse(m) for m in payload["messages"]]
-
-        if invocations:
-            invocations = [
-                TacticInvocation.parse(i) for i in invocations
-            ]
-        else:
-            invocations = None
-
-        if (state_id := payload.get("goalStateId")) is not None:
-            goal_state = GoalState.parse_inner(int(state_id), payload["goals"], [], goal_state_sentinel)
-            goal_src_boundaries = payload["goalSrcBoundaries"]
-        else:
-            goal_state = None
-            goal_src_boundaries = None
-
-        new_constants = payload.get("newConstants")
-
-        return CompilationUnit(
-            i_begin,
-            i_end,
-            messages,
-            invocations,
-            goal_state,
-            goal_src_boundaries,
-            new_constants
-        )
-
-@dataclass
-class CheckTrackResult:
-
-    src_messages : list[Message]
-    dst_messages : list[Message]
-    failure : Optional[str] = None
-
-    @property
-    def hasSrcError(self):
-        return any(m.severity == Severity.ERROR for m in self.src_messages)
-    @property
-    def hasDstError(self):
-        return any(m.severity == Severity.ERROR for m in self.dst_messages)
-    @property
-    def succeeded(self):
-        return not self.hasSrcError and not self.hasDstError and self.failure is None
-    @property
-    def feedback(self):
-        """
-        Feedback based on the dst
-        """
-        result = [str(s) for s in self.dst_messages]
-        if self.failure:
-            result.append(self.failure)
-        return result
-
-@dataclass(frozen=True)
-class SearchTarget:
-    goal_state: GoalState
-
-    @staticmethod
-    def parse(payload: dict, goal_state_sentinel=None):
-        state_id = payload.get("stateId")
-        goal_state = GoalState.parse_inner(int(state_id), payload["goals"], [], goal_state_sentinel)
-
-        return SearchTarget(
-            goal_state,
-        )

PyPantograph/pantograph/expr.py

@@ -1,202 +0,0 @@
-"""
-Data structuers for expressions and goals
-"""
-from pantograph.message import Message
-
-from dataclasses import dataclass, field
-from enum import Enum
-from typing import Optional, TypeAlias
-
-Expr: TypeAlias = str
-
-def parse_expr(payload: dict) -> Expr:
-    """
-    :meta private:
-    """
-    return payload["pp"]
-
-class TacticMode(Enum):
-    """
-    Current execution mode
-    """
-    TACTIC = 1
-    CONV = 2
-    CALC = 3
-
-    def serial(self):
-        match self:
-            case TacticMode.TACTIC: return "tactic"
-            case TacticMode.CONV: return "conv"
-            case TacticMode.CALC: return "calc"
-
-@dataclass(frozen=True)
-class Variable:
-    t: Expr
-    v: Optional[Expr] = None
-    name: Optional[str] = None
-
-    @staticmethod
-    def parse(payload: dict):
-        name = payload.get("userName")
-        t = parse_expr(payload["type"])
-        v = payload.get("value")
-        if v:
-            v = parse_expr(v)
-        return Variable(t, v, name)
-
-    def __str__(self):
-        """
-        :meta public:
-        """
-        result = self.name if self.name else "_"
-        result += f" : {self.t}"
-        if self.v:
-            result += f" := {self.v}"
-        return result
-
-@dataclass(frozen=True)
-class Goal:
-    id: str
-    variables: list[Variable]
-    target: Expr
-    sibling_dep: Optional[set[int]] = field(default_factory=lambda: None)
-    name: Optional[str] = None
-    mode: TacticMode = TacticMode.TACTIC
-
-    @staticmethod
-    def sentence(id: str, target: Expr):
-        """
-        :meta public:
-        """
-        return Goal(id=id, variables=[], target=target)
-
-    @staticmethod
-    def parse(payload: dict, sibling_map: dict[str, int]):
-        id = payload["name"]
-        name = payload.get("userName")
-        variables = [Variable.parse(v) for v in payload["vars"]]
-        target = parse_expr(payload["target"])
-        mode = TacticMode[payload["fragment"].upper()]
-
-        sibling_dep = None
-        for e in [payload["target"]] \
-                + [v["type"] for v in payload["vars"]] \
-                + [v["value"] for v in payload["vars"] if "value" in v]:
-            dependents = e.get("dependentMVars")
-            if dependents is None:
-                continue
-            deps = [sibling_map[d] for d in dependents if d in sibling_map]
-            if sibling_dep:
-                sibling_dep = {*sibling_dep, *deps}
-            else:
-                sibling_dep = {*deps}
-
-        return Goal(id, variables, target, sibling_dep, name, mode)
-
-    def __str__(self):
-        head = f"case {self.name}\n" if self.name else ""
-        front = "|" if self.mode == TacticMode.CONV else "⊢"
-        return head +\
-            "\n".join(str(v) for v in self.variables) +\
-            f"\n{front} {self.target}"
-
-@dataclass(frozen=True)
-class GoalState:
-    state_id: int
-    goals: list[Goal]
-    messages: list[Message]
-
-    # For tracking memory usage
-    _sentinel: list[int]
-
-    def __del__(self):
-        self._sentinel.append(self.state_id)
-    def __repr__(self):
-        cls = self.__class__.__name__
-        messages = f"messages={repr(self.messages)}, " if self.messages else ""
-        return f"{cls}(#{self.state_id}, goals={repr(self.goals)}{messages}, _sentinel=#{len(self._sentinel)}"
-
-    @property
-    def is_solved(self) -> bool:
-        """
-        WARNING: Does not handle dormant goals.
-
-        :meta public:
-        """
-        return not self.goals
-
-    @staticmethod
-    def parse_inner(state_id: int, goals: list, messages: list[dict], _sentinel: list[int]):
-        assert _sentinel is not None
-        goal_names = { g["name"]: i for i, g in enumerate(goals) }
-        goals = [Goal.parse(g, goal_names) for g in goals]
-        messages = [Message.parse(m) for m in messages]
-        return GoalState(state_id, goals, messages, _sentinel)
-    @staticmethod
-    def parse(payload: dict, messages: list[dict], _sentinel: list[int]):
-        return GoalState.parse_inner(payload["nextStateId"], payload["goals"], messages, _sentinel)
-
-    def __str__(self):
-        """
-        :meta public:
-        """
-        return "\n".join([str(g) for g in self.goals])
-
-@dataclass(frozen=True)
-class Site:
-    """
-    Acting area of a tactic
-    """
-    goal_id: Optional[int] = None
-    auto_resume: Optional[bool] = None
-
-    def serial(self) -> dict:
-        result = {}
-        if self.goal_id is not None:
-            result["goalId"] = self.goal_id
-        if self.auto_resume is not None:
-            result["autoResume"] = self.auto_resume
-        return result
-
-class Subsumption(Enum):
-    """
-    Subsumption result
-    """
-    NONE = 1
-    SUBSUMED = 2
-    CYCLE = 3
-
-@dataclass(frozen=True)
-class TacticHave:
-    """
-    The `have` tactic, equivalent to
-    ```lean
-    have {binder_name} : {branch} := ...
-    ```
-    """
-    branch: str
-    binder_name: Optional[str] = None
-@dataclass(frozen=True)
-class TacticLet:
-    """
-    The `let` tactic, equivalent to
-    ```lean
-    let {binder_name} : {branch} := ...
-    ```
-    """
-    branch: str
-    binder_name: Optional[str] = None
-@dataclass(frozen=True)
-class TacticExpr:
-    """
-    Assigns an expression to the current goal
-    """
-    expr: str
-@dataclass(frozen=True)
-class TacticDraft:
-    """
-    Assigns an expression to the current goal
-    """
-    expr: str
-
-Tactic: TypeAlias = str | TacticHave | TacticLet | TacticExpr | TacticDraft | TacticMode

PyPantograph/pantograph/message.py

@@ -1,73 +0,0 @@
-from dataclasses import dataclass
-from enum import Enum
-from typing import Optional, Self
-
-class Severity(Enum):
-    INFORMATION = 1
-    WARNING = 2
-    ERROR = 3
-
-    def __str__(self):
-        cls = self.__class__.__name__
-        return super(Severity, self).__str__()[len(cls)+1:].lower()
-
-@dataclass(frozen=True)
-class Position:
-    """
-    Position in a file
-    """
-    line: int
-    column: int
-
-    @staticmethod
-    def parse(d: Optional[dict]) -> Optional[Self]:
-        if d is None:
-            return None
-        return Position(line=d["line"], column=d["column"])
-
-@dataclass(frozen=True)
-class Message:
-    data: str
-    pos: Position
-    pos_end: Optional[Position] = None
-    severity: Severity = Severity.ERROR
-    kind: Optional[str] = None
-
-    @staticmethod
-    def parse(d: dict) -> Self:
-        kind = None if d["kind"] == "[anonymous]" else d["kind"]
-        return Message(
-            severity=Severity[d["severity"].upper()],
-            pos=Position.parse(d["pos"]),
-            pos_end=Position.parse(d.get("endPos")),
-            kind=kind,
-            data=d["data"],
-        )
-
-    def __str__(self) -> str:
-        if self.pos_end is not None:
-            pos_end = f"-{self.pos_end.line}:{self.pos_end.column}"
-        else:
-            pos_end = ""
-        match self.severity:
-            case Severity.INFORMATION:
-                prefix = ""
-            case Severity.WARNING:
-                prefix = "warning: "
-            case Severity.ERROR:
-                prefix = "error: "
-        return f"{self.pos.line}:{self.pos.column}{pos_end}: {prefix}{self.data}"
-
-
-class TacticFailure(Exception):
-    """
-    Indicates a tactic failed to execute
-    """
-class ParseError(Exception):
-    """
-    Indicates a logical error in the server.
-    """
-class ServerError(Exception):
-    """
-    Indicates a logical error in the server.
-    """

PyPantograph/pantograph/search.py

@@ -1,450 +0,0 @@
-from .server import Server, TacticFailure, ServerError
-from .expr import Expr, Tactic, GoalState, Site
-
-import random
-from abc import abstractmethod
-import time
-from dataclasses import dataclass
-from typing import Optional, List
-import collections
-from math import log, sqrt
-
-
-
-@dataclass
-class SearchState:
-
-    goal_state: GoalState
-    parent: Optional["SearchState"]
-    parent_goal_id: Optional[int]
-    priorities: list[float]
-    children: Optional[List["SearchState"]] = None
-    tested_tactics: Optional[List[Tactic]] = None
-    total_value: Optional[float] = None
-    tactic_feedback: Optional[str] = None
-
-    def __post_init__(self):
-        assert len(self.priorities) == len(self.goal_state.goals)
-        self.solved = [False for _ in self.goal_state.goals]
-        self.trials = [0 for _ in self.goal_state.goals]
-        self.tested_tactics = [] if self.tested_tactics is None else self.tested_tactics
-        self.children = [] if self.children is None else self.children
-        self.visit_count = 1
-        self.exhausted = False
-        self.subtree_exhausted = False
-
-    @property
-    def next_goal_id(self) -> int:
-        goal_id, _ = max(
-            ((i, prio) for i, prio in enumerate(self.priorities) if not self.solved[i]),
-            key=lambda x: x[1])
-        return goal_id
-
-    @property
-    def is_root(self) -> bool:
-        return self.parent is None
-
-    @property
-    def is_solved(self) -> bool:
-        return all(self.solved)
-
-@dataclass(frozen=True)
-class SearchResult:
-
-    n_goals_root: int
-    duration: float
-    success: bool
-    steps: int
-
-class Agent:
-    """
-    An agent interface for proof search
-    """
-
-    @abstractmethod
-    def next_tactic(
-            self,
-            state: GoalState,
-            goal_id: int,
-        ) -> Optional[Tactic]:
-        """
-        Implement this function to generate the next tactic for a goal
-        """
-
-    @abstractmethod
-    def guidance(self, state: GoalState) -> list[float]:
-        """
-        Return a list of priorities determining which goal should be searched
-        first. This will not be called on states with one or zero goals.
-        """
-        return [0.0 for _ in state.goals]
-    @abstractmethod
-    def reset(self):
-        """
-        Called after search
-        """
-
-    def search(self,
-               server: Server,
-               goal_state: GoalState,
-               max_steps: int = 100,
-               max_trials_per_goal: int = 5,
-               verbose: bool = False) -> SearchResult:
-        """
-        Executes proof search on this state
-        """
-
-        assert server.is_automatic(), "Search must be run in automatic mode"
-
-        n_goals_root = len(goal_state.goals)
-        time_start = time.time()
-
-        initial_state = SearchState(
-            goal_state,
-            parent=None,
-            parent_goal_id=None,
-            priorities=[0.0 for _ in goal_state.goals]
-        )
-        search_stack = [initial_state]
-        for i_step in range(max_steps):
-            assert search_stack, "No states in search stack"
-
-            if verbose:
-                print(f"I={i_step}: len(S) = {len(search_stack)}")
-            search_state = search_stack[-1]
-
-            assert isinstance(search_state, SearchState)
-
-            if search_state.is_solved:
-                return SearchResult(
-                    n_goals_root=n_goals_root,
-                    duration=time.time() - time_start,
-                    success=True,
-                    steps=i_step,
-                )
-
-            # Find the unsolved goal with the highest priority
-            goal_id = search_state.next_goal_id
-
-            if search_state.trials[goal_id] > max_trials_per_goal:
-                # force halt the search
-                tactic = None
-            else:
-                # Generate tactic for this goal
-                tactic = self.next_tactic(search_state.goal_state, goal_id)
-
-            if verbose:
-                print(f"Next tactic: {tactic}")
-            if not tactic:
-                # resets the feedback
-                search_state.tactic_feedback = None
-                # pop the current state and continue to the next
-                search_stack.pop(-1)
-                if not search_stack:
-                    if verbose:
-                        print("Search stack has been exhausted")
-                    self.reset()
-                    return SearchResult(
-                        n_goals_root=n_goals_root,
-                        duration=time.time() - time_start,
-                        success=False,
-                        steps=i_step,
-                    )
-                continue
-
-            try:
-                search_state.trials[goal_id] += 1
-                goal_state = search_state.goal_state
-                if verbose:
-                    print(f"{goal_state.state_id}.{goal_id}: {tactic} on {goal_state.goals[goal_id]}")
-                next_goal_state = server.goal_tactic(goal_state, tactic, site=Site(goal_id, auto_resume=False))
-                # Generate priorities for the next goal state
-                priorities = [0.0 for _ in next_goal_state.goals] \
-                    if len(next_goal_state.goals) <= 1 else \
-                    self.guidance(next_goal_state)
-                parent = len(search_stack) - 1
-                next_state = SearchState(
-                    goal_state=next_goal_state,
-                    parent=search_state,
-                    parent_goal_id=goal_id,
-                    priorities=priorities
-                )
-                search_stack.append(next_state)
-
-            except TacticFailure as t:
-                if verbose:
-                    print(f"Tactic failed: {t}")
-                search_state.tactic_feedback = str(t)
-                # try the next tactic. this one failed
-            except ServerError as e:
-                raise RuntimeError(f"While executing tactic: {tactic}") from e
-
-        if verbose:
-            print("Search iteration limit exhausted")
-
-        self.reset()
-        return SearchResult(
-            n_goals_root=n_goals_root,
-            duration=time.time() - time_start,
-            success=False,
-            steps=max_steps,
-        )
-
-
-class MCTSAgent(Agent):
-    """
-    An agent interface for proof search using monte carlo tree search
-    """
-
-    @abstractmethod
-    def next_tactic(
-            self,
-            state: GoalState,
-            goal_id: int,
-            tested: Optional[List[Tactic]] = None,
-        ) -> Optional[Tactic]:
-        """
-        Implement this function to generate the next tactic for a goal given tactics already tested
-        """
-
-    @abstractmethod
-    def reset(self):
-        """
-        Called after search
-        """
-
-    @abstractmethod
-    def estimate(self, state: SearchState) -> SearchState:
-        """
-        Implement this function to estimate the value of a state
-        """
-
-    @abstractmethod
-    def select(self, state: SearchState) -> list[SearchState]:
-        """
-        Implement this function to select the best node within the subtree of the state.
-        Returns the path to the selected node from the given state.
-        """
-
-    def backup(self, states: list[SearchState], value: float):
-        """
-        Backup value of the state at the end of the states list.
-        """
-        for state in states:
-            state.total_value += value
-            state.visit_count += 1
-            state.subtree_exhausted = all(child.subtree_exhausted for child in state.children) and state.exhausted
-
-    def search(self,
-               server: Server,
-               goal_state: GoalState,
-               max_steps: int = 100,
-               max_trials_per_goal: int = 5,
-               verbose: bool = False) -> SearchResult:
-        """
-        Executes proof search on this state
-        """
-
-        assert server.is_automatic(), "Search must be run in automatic mode"
-
-        n_goals_root = len(goal_state.goals)
-        time_start = time.time()
-
-        initial_state = SearchState(
-            goal_state=goal_state,
-            parent=None,
-            parent_goal_id=None,
-            priorities=[0.0 for _ in goal_state.goals]
-        )
-        initial_state = self.estimate(initial_state)
-        search_root = initial_state
-
-        for i_step in range(max_steps):
-            search_trajectory = self.select(search_root)
-            search_state = search_trajectory[-1]
-            assert isinstance(search_state, SearchState)
-
-            if search_state.is_solved:
-                return SearchResult(
-                    n_goals_root=n_goals_root,
-                    duration=time.time() - time_start,
-                    success=True,
-                    steps=i_step,
-                )
-
-            # Find the unsolved goal with the highest priority
-            goal_id = search_state.next_goal_id
-
-            if search_state.trials[goal_id] > max_trials_per_goal:
-                # force halt the search
-                tactic = None
-            else:
-                # Generate tactic for this goal
-                tactic = self.next_tactic(search_state.goal_state, goal_id, search_state.tested_tactics)
-
-            if verbose:
-                print(f"Next tactic: {tactic}")
-            if not tactic:
-                # resets the feedback
-                search_state.tactic_feedback = None
-                search_state.exhausted = True
-                search_state.subtree_exhausted = all(child.subtree_exhausted for child in search_state.children)
-                continue
-            assert tactic not in search_state.tested_tactics, "Tactic already seen!"
-            search_state.tested_tactics.append(tactic)
-
-            try:
-                search_state.trials[goal_id] += 1
-                state = search_state.goal_state
-                if verbose:
-                    print(f"{state.state_id}.{goal_id}: {tactic} on {search_state.goal_state.goals[goal_id]}")
-                next_goal_state = server.goal_tactic(goal_state, tactic, site=Site(goal_id, auto_resume=False))
-                # Generate priorities for the next goal state
-                priorities = [0.0 for _ in next_goal_state.goals] \
-                    if len(next_goal_state.goals) <= 1 else \
-                    self.guidance(next_goal_state)
-                parent = -1
-                next_state = SearchState(
-                    goal_state=next_goal_state,
-                    parent=parent,
-                    parent_goal_id=goal_id,
-                    priorities=priorities
-                )
-                next_state = self.estimate(next_state)
-                search_state.children.append(next_state)
-                self.backup(search_trajectory, next_state.total_value)
-            except TacticFailure as t:
-                if verbose:
-                    print(f"Tactic failed: {t}")
-                search_state.tactic_feedback = str(t)
-                # try the next tactic. this one failed
-            except ServerError as e:
-                raise RuntimeError(f"While executing tactic: {tactic}") from e
-
-        if verbose:
-            print("Search iteration limit exhausted")
-
-        self.reset()
-        return SearchResult(
-            n_goals_root=n_goals_root,
-            duration=time.time() - time_start,
-            success=False,
-            steps=max_steps,
-        )
-
-
-class DumbAgent(Agent):
-
-    def __init__(self):
-        super().__init__()
-
-        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
-        self.intros = [
-            "intro",
-        ]
-        self.tactics = [
-            "intro h",
-            "cases h",
-            "apply Or.inl",
-            "apply Or.inr",
-        ]
-        self.no_space_tactics = [
-            "assumption",
-        ]
-
-    def next_tactic(
-            self,
-            state: GoalState,
-            goal_id: int,
-    ) -> Optional[Tactic]:
-        key = (state.state_id, goal_id)
-        i = self.goal_tactic_id_map[key]
-
-        target = state.goals[goal_id].target
-        if target.startswith('∀'):
-            tactics = self.intros
-        elif ' ' in target:
-            tactics = self.tactics
-        else:
-            tactics = self.no_space_tactics
-
-        if i >= len(tactics):
-            return None
-
-        self.goal_tactic_id_map[key] = i + 1
-        return tactics[i]
-
-class DumbMCTSAgent(MCTSAgent):
-    def __init__(self):
-        super().__init__()
-
-        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
-        self.intros = [
-            "intro",
-        ]
-        self.tactics = [
-            "intro h",
-            "cases h",
-            "apply Or.inl",
-            "apply Or.inr",
-        ]
-        self.no_space_tactics = [
-            "assumption",
-        ]
-        self.c = 0.6
-
-    def estimate(self, state: SearchState) -> SearchState:
-        state.total_value = random.random()
-        return state
-
-    def select(self, state: SearchState) -> list[SearchState]:
-        """
-        UCB scoring with taking the current state as one option, i.e. one child
-        """
-        state_trajectory = [state]
-        current_state = state
-        current_state_ucb = (state.total_value / state.visit_count) + self.c * sqrt((log(state.visit_count) / state.visit_count))
-        while current_state.children:
-            avg_val = [child.total_value / child.visit_count for child in current_state.children]
-            visit_portions = [sqrt(log(current_state.visit_count) / child.visit_count) for child in current_state.children]
-            ucbs = [avg + self.c * visit for avg, visit in zip(avg_val, visit_portions, strict=True)]
-            child_idcs = [idx for idx in range(len(current_state.children)) if not current_state.children[idx].subtree_exhausted]
-            if not child_idcs:
-                return state_trajectory
-            child_idx = child_idcs[0]
-            for i in child_idcs:
-                if ucbs[i] > ucbs[child_idx]:
-                    child_idx = i
-            if ucbs[child_idx] < current_state_ucb and not current_state.exhausted:
-                return state_trajectory
-            current_state_ucb = ucbs[child_idx]
-            current_state = current_state.children[child_idx]
-            state_trajectory.append(current_state)
-        return state_trajectory
-
-    def next_tactic(
-            self,
-            state: GoalState,
-            goal_id: int,
-            tested: Optional[List[Tactic]] = None
-    ) -> Optional[Tactic]:
-        key = (state.state_id, goal_id)
-        i = self.goal_tactic_id_map[key]
-        target = state.goals[goal_id].target
-        if target.startswith('∀'):
-            tactics = self.intros
-        elif ' ' in target:
-            tactics = self.tactics
-        else:
-            tactics = self.no_space_tactics
-
-        if i >= len(tactics):
-            return None
-        self.goal_tactic_id_map[key] = i + 1
-        while tactics[i] in tested:
-            i += 1
-            if i >= len(tactics):
-                return None
-        return tactics[i]
-
-

PyPantograph/pantograph/server.py

@@ -1,695 +0,0 @@
-"""
-Class which manages a Pantograph instance. All calls to the kernel uses this
-interface.
-"""
-from .message import (
-    Position,
-    Severity,
-    Message,
-    TacticFailure,
-    ParseError,
-    ServerError,
-)
-from .expr import (
-    parse_expr,
-    Expr,
-    Variable,
-    Goal,
-    GoalState,
-    Site,
-    Subsumption,
-    Tactic,
-    TacticHave,
-    TacticLet,
-    TacticMode,
-    TacticExpr,
-    TacticDraft,
-)
-from .utils import (
-    to_sync,
-    _get_proc_cwd,
-    _get_proc_path,
-    get_lean_path_async,
-    get_lean_path,
-)
-from .data import (
-    CheckTrackResult,
-    CompilationUnit,
-    SearchTarget,
-)
-
-import json, os, asyncio, tempfile
-from typing import Union, List, Optional, Dict, List, Any, Tuple
-from pathlib import Path
-
-class Server:
-    """
-    Main interaction instance with Pantograph.
-
-    Asynchronous and synchronous versions are provided for each function.
-    """
-
-    def __init__(
-            self,
-            imports: List[str]=["Init"],
-            project_path: Optional[str]=None,
-            lean_path: Optional[str]=None,
-            # Options for executing the REPL.
-            options: Dict[str, Any]={},
-            # Options supplied to the Lean core
-            core_options: List[str]=[],
-            timeout: int=60,
-            buffer_limit: Optional[int]=1000000,
-            _sync_init: bool=True):
-        """
-        options: Given to Pantograph
-        core_options: Given to Lean core
-        timeout: Amount of time to wait for execution (in seconds)
-        maxread: Maximum number of characters to read (especially important for large proofs and catalogs)
-        """
-        self.timeout = timeout
-        self.imports = imports
-        self.project_path = project_path if project_path else _get_proc_cwd()
-        if _sync_init and project_path and not lean_path:
-            lean_path = get_lean_path(project_path)
-        self.lean_path = lean_path
-        self.buffer_limit = buffer_limit
-        self.proc_path = _get_proc_path()
-
-        self.options = options
-        self.core_options = core_options
-        self.args = imports + [f'--{opt}' for opt in core_options]
-        self.proc = None
-        if _sync_init:
-            self.restart()
-
-        # List of goal states that should be garbage collected
-        self.to_remove_goal_states = []
-
-    @classmethod
-    async def create(
-            cls,
-            imports: List[str]=["Init"],
-            project_path: Optional[str]=None,
-            lean_path: Optional[str]=None,
-            # Options for executing the REPL.
-            # Set `{ "automaticMode" : False }` to handle resumption by yourself.
-            options: Dict[str, Any]={},
-            core_options: List[str]=[],
-            timeout: int=120,
-            buffer_limit: Optional[int]=1000000,
-            start: bool=True) -> 'Server':
-        """
-        timeout: Amount of time to wait for execution (in seconds)
-        maxread: Maximum number of characters to read (especially important for large proofs and catalogs)
-        """
-        self = cls(
-            imports,
-            project_path,
-            lean_path,
-            options,
-            core_options,
-            timeout,
-            buffer_limit,
-            _sync_init=False
-        )
-        if project_path and not lean_path:
-            lean_path = await get_lean_path_async(project_path)
-        self.lean_path = lean_path
-        if start:
-            await self.restart_async()
-        return self
-
-    def __enter__(self) -> "Server":
-        return self
-
-    def __exit__(self, exc_type: Any, exc_val: Any, exc_tb: Any) -> None:
-        self._close()
-
-    def __del__(self):
-        pass #self._close()
-
-    def _close(self):
-        if not self.proc:
-            return
-
-        self.proc.terminate()
-        self.proc = None
-
-    def is_automatic(self):
-        """
-        Check if the server is running in automatic mode
-        """
-        return self.options.get("automaticMode", True)
-
-    async def restart_async(self):
-        """
-        Restart the server
-        """
-        self._close()
-        env = os.environ
-        if self.lean_path:
-            env = env | {'LEAN_PATH': self.lean_path}
-
-        self.proc = await asyncio.create_subprocess_exec(
-            self.proc_path,
-            *self.args,
-            stdin=asyncio.subprocess.PIPE,
-            stdout=asyncio.subprocess.PIPE,
-            #stderr=asyncio.subprocess.PIPE,
-            cwd=self.project_path,
-            env=env,
-            limit=self.buffer_limit,
-        )
-        await self.proc.stdin.drain()
-        try:
-            ready = await asyncio.wait_for(self.proc.stdout.readline(), self.timeout)
-            ready = ready.decode().strip()
-            assert ready == "ready.", f"Server failed to emit ready signal: {ready}; This could be caused by Lean version mismatch between the project and Pantograph or insufficient timeout."
-        except asyncio.TimeoutError as ex:
-            raise RuntimeError("Server failed to emit ready signal in time") from ex
-
-        if self.options:
-            await self.run_async("options.set", self.options)
-
-    restart = to_sync(restart_async)
-
-    async def run_async(self, cmd, payload):
-        """
-        Runs a raw JSON command. Preferably use one of the commands below.
-
-        :meta private:
-        """
-        assert self.proc, "Server not running."
-
-        s = json.dumps(payload, ensure_ascii=False)
-        command = f"{cmd} {s}\n"
-        self.proc.stdin.write(command.encode())
-        await self.proc.stdin.drain()
-        line = ""
-        try:
-            line = await asyncio.wait_for(self.proc.stdout.readline(), self.timeout)
-        except asyncio.TimeoutError as e:
-            self._close()
-            raise ServerError("Server reached timeout limit") from e
-
-        try:
-            line = line.decode().strip()
-            return json.loads(line)
-        except UnicodeDecodeError as e:
-            self._close()
-            raise ServerError(f"Could not decode process output: {line}") from e
-        except json.JSONDecodeError as e:
-            self._close()
-            raise ServerError(f"Cannot decode Json object from: {line}") from e
-
-    run = to_sync(run_async)
-
-    async def gc_async(self):
-        """
-        Garbage collect deleted goal states to free up memory.
-        """
-        if not self.to_remove_goal_states:
-            return
-        result = await self.run_async('goal.delete', {'stateIds': self.to_remove_goal_states})
-        self.to_remove_goal_states.clear()
-        if "error" in result:
-            raise ServerError(result)
-
-    gc = to_sync(gc_async)
-
-    async def expr_type_async(self, expr: Expr) -> Expr:
-        """
-        Evaluate the type of a given expression. This gives an error if the
-        input `expr` is ill-formed.
-        """
-        result = await self.run_async('expr.echo', {"expr": expr})
-        if "error" in result:
-            raise ServerError(result)
-        return parse_expr(result["type"])
-
-    expr_type = to_sync(expr_type_async)
-
-    async def goal_start_async(self, expr: Expr) -> GoalState:
-        """
-        Create a goal state with one root goal, whose target is `expr`
-        """
-        result = await self.run_async('goal.start', {"expr": str(expr)})
-        if "error" in result:
-            print(f"Cannot start goal: {expr}")
-            raise ServerError(result)
-        return GoalState(
-            state_id=result["stateId"],
-            goals=[Goal.sentence(result["root"], expr)],
-            messages=[],
-            _sentinel=self.to_remove_goal_states,
-        )
-
-    goal_start = to_sync(goal_start_async)
-
-    async def goal_root_async(self, state: GoalState) -> Optional[Expr]:
-        """
-        Print the root expression of a goal state
-        """
-        args = {"stateId": state.state_id, "rootExpr": True}
-        result = await self.run_async('goal.print', args)
-        if "error" in result:
-            raise ServerError(result)
-        root = result.get('root')
-        if root is None:
-            return None
-        return parse_expr(root)
-
-    goal_root = to_sync(goal_root_async)
-
-    async def goal_tactic_async(self, state: GoalState, tactic: Tactic, site: Site = Site()) -> GoalState:
-        """
-        Execute a tactic on `goal_id` of `state`
-        """
-        args = {"stateId": state.state_id, **site.serial()}
-        match tactic:
-            case str():
-                args["tactic"] = tactic
-            case TacticHave():
-                args["have"] = tactic.branch
-                if tactic.binder_name:
-                    args["binderName"] = tactic.binder_name
-            case TacticLet():
-                args["let"] = tactic.branch
-                if tactic.binder_name:
-                    args["binderName"] = tactic.binder_name
-            case TacticExpr():
-                args["expr"] = tactic.expr
-            case TacticDraft():
-                args["draft"] = tactic.expr
-            case TacticMode():
-                args["mode"] = tactic.serial()
-            case _:
-                raise RuntimeError(f"Invalid tactic type: {type(tactic)}")
-        result = await self.run_async('goal.tactic', args)
-        next_state_id = result.get("nextStateId")
-        if "error" in result:
-            raise ServerError(result)
-        if "parseError" in result:
-            raise TacticFailure(result)
-
-        messages = result.get("messages")
-        if "goals" not in result:
-            raise TacticFailure([Message.parse(m) for m in messages])
-
-        if result["hasSorry"]:
-            await self.run_async('goal.delete', {'stateIds': [next_state_id]})
-            raise TacticFailure("Tactic generated sorry", messages)
-        if result["hasUnsafe"]:
-            await self.run_async('goal.delete', {'stateIds': [next_state_id]})
-            raise TacticFailure("Tactic generated unsafe", messages)
-
-        return GoalState.parse(result, messages, self.to_remove_goal_states)
-
-    goal_tactic = to_sync(goal_tactic_async)
-
-    async def goal_continue_async(self, target: GoalState, branch: GoalState) -> GoalState:
-        """
-        After finish searching `target`, resume search on `branch`
-        """
-        result = await self.run_async('goal.continue', {
-            "target": target.state_id,
-            "branch": branch.state_id,
-        })
-        if "error" in result:
-            raise ServerError(result)
-        if "tacticErrors" in result:
-            raise ServerError(result)
-        if "parseError" in result:
-            raise ServerError(result)
-        return GoalState.parse(result, [], self.to_remove_goal_states)
-
-    goal_continue = to_sync(goal_continue_async)
-
-    async def goal_resume_async(self, state: GoalState, goals: list[Goal]) -> GoalState:
-        """
-        Bring `goals` back into scope
-        """
-        result = await self.run_async('goal.continue', {
-            "target": state.state_id,
-            "goals": [goal.name for goal in goals],
-        })
-        if "error" in result:
-            raise ServerError(result)
-        if "tacticErrors" in result:
-            raise ServerError(result)
-        if "parseError" in result:
-            raise ServerError(result)
-        return GoalState.parse(result, [], self.to_remove_goal_states)
-    goal_resume = to_sync(goal_resume_async)
-
-    async def goal_subsume_async(
-            self,
-            state: GoalState,
-            goal: Goal,
-            candidates: list[Goal],
-            src_state: Optional[GoalState]=None
-    ) -> (Subsumption, Optional[GoalState], Optional[Goal]):
-        """
-        Detect subsumption by candidate goals
-
-        The candidate goals must all exist in `src_state`. If `src_state` is not
-        provided, they must exist in `state`. Returns a new goal state if a
-        subsumption does not lead to a cycle, and the subsumptor if there is any
-        subsumption happening.
-        """
-        args = {
-            "stateId": state.state_id,
-            "goal": goal.id,
-            "candidates": [g.id for g in candidates],
-        }
-        if src_state:
-            args["srcStateId"] = src_state.state_id
-        result = await self.run_async('goal.subsume', args)
-        if "error" in result:
-            raise ServerError(result)
-        nextState = None
-        if state_id := result.get("stateId"):
-            nextState = GoalState(
-                state_id=state_id,
-                goals=[g for g in state.goals if g.id != goal.id],
-                messages=[],
-                _sentinel=self.to_remove_goal_states,
-            )
-        sub = Subsumption[result["result"].upper()]
-        subsumptor = None
-        if subsumptor := result.get("subsumptor"):
-            gen = (g for g in candidates if g.id == subsumptor)
-            subsumptor = next(gen)
-            if subsumptor is None:
-                raise ServerError("Subsumptor should not be none")
-        return (sub, nextState, subsumptor)
-
-    goal_subsume = to_sync(goal_subsume_async)
-
-    async def env_add_async(
-            self, name: str, levels: list[str],
-            t: Expr, v: Expr, is_theorem: bool = True):
-        """
-        Adds a definition to the environment.
-
-        NOTE: May have to accept additional parameters if the definition
-        contains universe mvars.
-        """
-        result = await self.run_async('env.add', {
-            "name": name,
-            "levels": levels,
-            "type": t,
-            "value": v,
-            "isTheorem": is_theorem,
-            "typeErrorsAsGoals": False,
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-
-    env_add = to_sync(env_add_async)
-
-    async def env_catalog_async(
-            self,
-            module_prefix: str | None = None,
-            invert_filter: bool = False
-    ) -> list[str]:
-        """
-        Print all symbols in environment.
-        """
-        with tempfile.NamedTemporaryFile('r') as tmp_file:
-            result = await self.run_async('env.catalog', {
-                'filename': tmp_file.name,
-                'modulePrefix': module_prefix,
-                'invertFilter': invert_filter,
-            })
-            if "error" in result:
-                raise ServerError(result["desc"])
-            return [line.strip() for line in tmp_file.readlines()]
-    env_catalog = to_sync(env_catalog_async)
-
-    async def env_inspect_async(
-            self,
-            name: str,
-            print_value: bool = False,
-            print_dependency: bool = False) -> Dict:
-        """
-        Print the type and dependencies of a constant.
-        """
-        result = await self.run_async('env.inspect', {
-            "name": name,
-            "value": print_value,
-            "dependency": print_dependency,
-            "source": True,
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-        return result
-    env_inspect = to_sync(env_inspect_async)
-
-    async def env_module_read_async(self, module: str) -> dict:
-        """
-        Reads the content from one Lean module including what constants are in
-        it.
-        """
-        result = await self.run_async('env.module_read', {
-            "module": module
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-        return result
-    env_module_read = to_sync(env_module_read_async)
-
-    async def env_parse_async(self, src: str, category: str = "tactic") -> Tuple[str, str]:
-        """
-        Parse an input using a syntax category's parser. Returns the parsed
-        component and the tail.
-        """
-        result = await self.run_async('env.parse', {
-            "input": src,
-            "category": category,
-        })
-        if "error" in result:
-            if result['error'] == 'parse':
-                raise ParseError(result["desc"])
-            raise ServerError(result["desc"])
-        pos = result["pos"]
-        s = src.encode()
-        return s[:pos].decode(), s[pos:].decode()
-
-    env_parse = to_sync(env_parse_async)
-
-    async def env_save_async(self, path: str):
-        """
-        Save the current environment to a file
-        """
-        result = await self.run_async('env.save', {
-            "path": os.path.abspath(path),
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-    env_save = to_sync(env_save_async)
-
-    async def env_load_async(self, path: str):
-        """
-        Load the current environment from a file
-        """
-        result = await self.run_async('env.load', {
-            "path": os.path.abspath(path),
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-
-    env_load = to_sync(env_load_async)
-
-    async def goal_save_async(self, goal_state: GoalState, path: str):
-        """
-        Save a goal state to a file
-        """
-        result = await self.run_async('goal.save', {
-            "id": goal_state.state_id,
-            "path": os.path.abspath(path),
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-
-    goal_save = to_sync(goal_save_async)
-
-    async def goal_load_async(self, path: str) -> GoalState:
-        """
-        Load a goal state from a file.
-
-        User is responsible for keeping track of the environment.
-        """
-        result = await self.run_async('goal.load', {
-            "path": os.path.abspath(path),
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-        state_id = result['id']
-        result = await self.run_async('goal.print', {
-            'stateId': state_id,
-            'goals': True,
-        })
-        if "error" in result:
-            raise ServerError(result["desc"])
-        return GoalState.parse_inner(
-            state_id,
-            result['goals'], [],
-            self.to_remove_goal_states,
-        )
-
-    goal_load = to_sync(goal_load_async)
-
-    async def tactic_invocations_async(self, file_name: Union[str, Path]) -> list[CompilationUnit]:
-        """
-        Collect tactic invocation points in file, and return them.
-        """
-        with tempfile.TemporaryDirectory() as tempdirname:
-            invocation_file_name = f"{tempdirname}/invocations.json"
-            result = await self.run_async('frontend.process', {
-                'fileName': str(file_name),
-                'invocations': invocation_file_name,
-                "readHeader": True,
-                "inheritEnv": False,
-                "newConstants": False,
-            })
-            if "error" in result:
-                raise ServerError(result)
-
-            with open(invocation_file_name, "r") as f:
-                data_units = json.load(f)
-                units = [
-                    CompilationUnit.parse(payload, invocations=data_unit["invocations"])
-                    for payload, data_unit in zip(result['units'], data_units['units'])
-                ]
-                return units
-
-    tactic_invocations = to_sync(tactic_invocations_async)
-
-    async def load_header_async(self, header: str):
-        """
-        Loads the environment from a header. Set `imports` to `[]` during
-        server creation to use this function.
-        """
-        result = await self.run_async('frontend.process', {
-            'file': header,
-            "newConstants": False,
-            "readHeader": True,
-            "inheritEnv": True,
-        })
-        if "error" in result:
-            raise ServerError(result)
-
-    load_header = to_sync(load_header_async)
-
-    async def load_definitions_async(self, snippet: str):
-        """
-        Loads definitions in some Lean code and update the environment.
-
-        Existing goal states will not automatically inherit said definitions.
-        """
-        result = await self.run_async('frontend.process', {
-            'file': snippet,
-            "newConstants": False,
-            "readHeader": False,
-            "inheritEnv": True,
-        })
-        if "error" in result:
-            raise ServerError(result)
-
-    load_definitions = to_sync(load_definitions_async)
-
-    async def check_compile_async(
-            self,
-            code: str,
-            new_constants: bool = False,
-            read_header: bool = False):
-        """
-        Check if some Lean code compiles
-        """
-        result = await self.run_async('frontend.process', {
-            'file': code,
-            "newConstants": new_constants,
-            "readHeader": read_header,
-            "inheritEnv": False,
-        })
-        if "error" in result:
-            raise ServerError(result)
-        units = [
-            CompilationUnit.parse(payload, goal_state_sentinel=self.to_remove_goal_states)
-            for payload in result['units']
-        ]
-        return units
-
-    check_compile = to_sync(check_compile_async)
-
-    async def load_sorry_async(
-            self,
-            src: str,
-            binder_name: Optional[str] = None,
-            ignore_values: bool = False) -> list[SearchTarget]:
-        """
-        Condense search target into goals
-        """
-        args = {"file": src, "ignoreValues": ignore_values}
-        if binder_name is not None:
-            args["binderName"] = binder_name
-        result = await self.run_async('frontend.distil', args)
-        if "error" in result:
-            raise ServerError(result)
-        units = [
-            SearchTarget.parse(payload, goal_state_sentinel=self.to_remove_goal_states)
-            for payload in result['targets']
-        ]
-        return units
-
-    load_sorry = to_sync(load_sorry_async)
-
-    async def check_track_async(self, src: str, dst: str) -> CheckTrackResult:
-        """
-        Checks if `dst` file conforms to the specifications in `src`
-        """
-        result = await self.run_async('frontend.track', {"src": src, "dst": dst})
-        if "error" in result:
-            raise ServerError(result)
-        src_messages = [Message.parse(d) for d in result["srcMessages"]]
-        dst_messages = [Message.parse(d) for d in result["dstMessages"]]
-        return CheckTrackResult(
-            src_messages,
-            dst_messages,
-            failure=result.get("failure"),
-        )
-
-    check_track = to_sync(check_track_async)
-
-    async def refactor_search_target_async(
-            self,
-            code: str,
-            core_options: list[str] = []) -> str:
-        """
-        Combine multiple `sorry`s into one `sorry` using subtyping. It only
-        supports flat dependency structures.
-
-        This feature is experimental and depends on the round-trip capabilities
-        of the delaborator.
-        """
-        result = await self.run_async('frontend.refactor', {
-            'file': code,
-            'coreOptions': core_options,
-        })
-        if "error" in result:
-            raise ServerError(result)
-        return result["file"]
-
-    refactor_search_target = to_sync(refactor_search_target_async)
-
-def get_version() -> str:
-    """
-    Returns the current Pantograph version for diagnostics purposes.
-    """
-    import subprocess
-    with subprocess.Popen([_get_proc_path(), "--version"],
-                          stdout=subprocess.PIPE,
-                          cwd=_get_proc_cwd()) as p:
-        return p.communicate()[0].decode('utf-8').strip()

PyPantograph/pantograph/test_message.py

@@ -1,25 +0,0 @@
-from .message import *
-import unittest
-
-class TestMessage(unittest.TestCase):
-
-    def test_severity(self):
-        self.assertEqual(str(Severity.ERROR), "error")
-    def test_message(self):
-        m = Message(
-            data="hi",
-            pos=Position(12, 34),
-            pos_end=Position(56, 78),
-            severity=Severity.WARNING,
-        )
-        self.assertEqual(str(m), "12:34-56:78: warning: hi")
-
-        m = Message(
-            data="hi",
-            pos=Position(0, 0),
-            severity=Severity.ERROR,
-        )
-        self.assertEqual(str(m), "0:0: error: hi")
-
-if __name__ == '__main__':
-    unittest.main()

PyPantograph/pantograph/test_search.py

@@ -1,55 +0,0 @@
-from .search import *
-import unittest
-
-class TestSearch(unittest.TestCase):
-
-    def test_solve(self):
-
-        server = Server()
-        agent = DumbAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), p -> p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
-        self.assertTrue(flag)
-    def test_solve_big(self):
-
-        server = Server()
-        agent = DumbAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        self.assertTrue(flag)
-
-class TestMCTSSearch(unittest.TestCase):
-
-    def test_solve(self):
-
-        server = Server()
-        agent = DumbMCTSAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), p -> p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            verbose=False)
-        #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
-        self.assertTrue(flag)
-    def test_solve_big(self):
-
-        server = Server()
-        agent = DumbMCTSAgent()
-        goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p")
-        flag = agent.search(
-            server=server,
-            goal_state=goal_state,
-            max_steps=200,
-            verbose=False)
-        self.assertTrue(flag)
-
-
-if __name__ == '__main__':
-    unittest.main()

PyPantograph/pantograph/test_server.py

@@ -1,381 +0,0 @@
-from .server import *
-import unittest
-
-class TestServer(unittest.TestCase):
-
-    def test_version(self):
-        """
-        NOTE: Update this after upstream updates.
-        """
-        self.assertEqual(get_version(), "0.3.10")
-
-    def test_server_init_del(self):
-        import warnings
-        with warnings.catch_warnings():
-            warnings.simplefilter("error", ResourceWarning)
-            server = Server()
-            server.expr_type("forall (n m: Nat), n + m = m + n")
-            del server
-            server = Server()
-            server.expr_type("forall (n m: Nat), n + m = m + n")
-            del server
-            server = Server()
-            server.expr_type("forall (n m: Nat), n + m = m + n")
-            del server
-
-    def test_expr_type(self):
-        server = Server()
-        t = server.expr_type("forall (n m: Nat), n + m = m + n")
-        self.assertEqual(t, "Prop")
-
-    def test_goal_start(self):
-        server = Server()
-        state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
-        self.assertEqual(len(server.to_remove_goal_states), 0)
-        self.assertEqual(state0.state_id, 0)
-        state1 = server.goal_tactic(state0, tactic="intro a")
-        self.assertEqual(state1.state_id, 1)
-        self.assertEqual(state1.goals, [Goal(
-            "_uniq.11",
-            variables=[Variable(name="a", t="Prop")],
-            target="∀ (q : Prop), a ∨ q → q ∨ a",
-            name=None,
-        )])
-        self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")
-
-        del state0
-        self.assertEqual(len(server.to_remove_goal_states), 1)
-        server.gc()
-        self.assertEqual(len(server.to_remove_goal_states), 0)
-
-        state0b = server.goal_start("forall (p: Prop), p -> p")
-        del state0b
-        self.assertEqual(len(server.to_remove_goal_states), 1)
-        server.gc()
-        self.assertEqual(len(server.to_remove_goal_states), 0)
-
-    def test_goal_root(self):
-        server = Server()
-        state0 = server.goal_start("forall (p: Prop), p -> p")
-        e = server.goal_root(state0)
-        self.assertEqual(e, None)
-        state1 = server.goal_tactic(state0, tactic="exact fun z p => p")
-        e = server.goal_root(state1)
-        self.assertEqual(e, "fun z p => p")
-
-    def test_automatic_mode(self):
-        server = Server()
-        state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
-        self.assertEqual(len(server.to_remove_goal_states), 0)
-        self.assertEqual(state0.state_id, 0)
-        state1 = server.goal_tactic(state0, tactic="intro a b h")
-        self.assertEqual(state1.state_id, 1)
-        self.assertEqual(state1.goals, [Goal(
-            "_uniq.17",
-            variables=[
-                Variable(name="a", t="Prop"),
-                Variable(name="b", t="Prop"),
-                Variable(name="h", t="a ∨ b"),
-            ],
-            target="b ∨ a",
-            name=None,
-        )])
-        state2 = server.goal_tactic(state1, tactic="cases h")
-        self.assertEqual(state2.goals, [
-            Goal(
-                "_uniq.57",
-                variables=[
-                    Variable(name="a", t="Prop"),
-                    Variable(name="b", t="Prop"),
-                    Variable(name="h✝", t="a"),
-                ],
-                target="b ∨ a",
-                name="inl",
-            ),
-            Goal(
-                "_uniq.70",
-                variables=[
-                    Variable(name="a", t="Prop"),
-                    Variable(name="b", t="Prop"),
-                    Variable(name="h✝", t="b"),
-                ],
-                target="b ∨ a",
-                name="inr",
-            ),
-        ])
-        state3 = server.goal_tactic(state2, tactic="apply Or.inl", site=Site(goal_id=1))
-        state4 = server.goal_tactic(state3, tactic="assumption")
-        self.assertEqual(state4.goals, [
-            Goal(
-                "_uniq.57",
-                variables=[
-                    Variable(name="a", t="Prop"),
-                    Variable(name="b", t="Prop"),
-                    Variable(name="h✝", t="a"),
-                ],
-                target="b ∨ a",
-                name="inl",
-            )
-        ])
-
-    def test_have(self):
-        server = Server()
-        state0 = server.goal_start("1 + 1 = 2")
-        state1 = server.goal_tactic(state0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
-        self.assertEqual(state1.goals, [
-            Goal(
-                "_uniq.251",
-                variables=[],
-                target="2 = 1 + 1",
-            ),
-            Goal(
-                "_uniq.253",
-                variables=[Variable(name="h", t="2 = 1 + 1")],
-                target="1 + 1 = 2",
-            ),
-        ])
-    def test_let(self):
-        server = Server()
-        state0 = server.goal_start("1 + 1 = 2")
-        state1 = server.goal_tactic(
-            state0, tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
-        self.assertEqual(state1.goals, [
-            Goal(
-                "_uniq.251",
-                variables=[],
-                name="h",
-                target="2 = 1 + 1",
-            ),
-            Goal(
-                "_uniq.253",
-                variables=[Variable(name="h", t="2 = 1 + 1", v="?h")],
-                target="1 + 1 = 2",
-            ),
-        ])
-
-    def test_conv_calc(self):
-        server = Server(options={"automaticMode": False})
-        state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
-
-        variables = [
-            Variable(name="a", t="Nat"),
-            Variable(name="b", t="Nat"),
-            Variable(name="h", t="b = 2"),
-        ]
-        state1 = server.goal_tactic(state0, "intro a b h")
-        state1b = server.goal_tactic(state1, TacticMode.CALC)
-        state2 = server.goal_tactic(state1b, "1 + a + 1 = a + 1 + 1")
-        self.assertEqual(state2.goals, [
-            Goal(
-                "_uniq.342",
-                variables,
-                target="1 + a + 1 = a + 1 + 1",
-                name='calc',
-            ),
-            Goal(
-                "_uniq.356",
-                variables,
-                target="a + 1 + 1 = a + b",
-                mode=TacticMode.CALC,
-            ),
-        ])
-        state_c1 = server.goal_tactic(state2, TacticMode.CONV)
-        state_c2 = server.goal_tactic(state_c1, "rhs")
-        state_c3 = server.goal_tactic(state_c2, "rw [Nat.add_comm]")
-        state_c4 = server.goal_tactic(state_c3, TacticMode.TACTIC)
-        #state_c4b = server.goal_resume(state_c4, [state2.goals[0]])
-        state_c5 = server.goal_tactic(state_c4, "rfl")
-        self.assertTrue(state_c5.is_solved)
-
-        state3 = server.goal_tactic(state2, "_ = a + 2", site=Site(1))
-        state4 = server.goal_tactic(state3, "rw [Nat.add_assoc]")
-        self.assertTrue(state4.is_solved)
-
-    def test_dependent_mvars(self):
-        server = Server(options={"printDependentMVars": True})
-        state = server.goal_start("∃ (x : Nat), x + 1 = 0")
-        state = server.goal_tactic(state, "apply Exists.intro")
-        self.assertEqual(state.goals[0].sibling_dep, {1})
-        self.assertEqual(state.goals[1].sibling_dep, set())
-
-    def test_subsume(self):
-        server = Server()
-        state0 = server.goal_start("forall (p : Prop), p -> p")
-        state1 = server.goal_tactic(state0, "intro p")
-        state2 = server.goal_tactic(state1, "intro h")
-        state3 = server.goal_tactic(state2, "revert h")
-        src = state1.goals[0]
-        (sub, state, subsumptor) = server.goal_subsume(
-            state3,
-            state3.goals[0],
-            [state1.goals[0], state2.goals[0]],
-        )
-        self.assertEqual(sub, Subsumption.CYCLE)
-        self.assertEqual(state, None)
-        self.assertEqual(subsumptor, src)
-
-    def test_env_add_inspect(self):
-        server = Server()
-        server.env_add(
-            name="mystery",
-            levels=[],
-            t="forall (n: Nat), Nat",
-            v="fun (n: Nat) => n + 1",
-            is_theorem=False,
-        )
-        inspect_result = server.env_inspect(name="mystery")
-        self.assertEqual(inspect_result['type'], {'pp': 'Nat → Nat'})
-
-    def test_env_catalog(self):
-        server = Server()
-        server.load_definitions("def foo: Nat -> Nat | 0 => 1 | n + 1 => foo n")
-        definitions = server.env_catalog(module_prefix="Init", invert_filter=True)
-        self.assertEqual(
-            set(definitions),
-            {'dfoo._sunfold', 'dfoo._unsafe_rec', 'dfoo', 'dfoo.match_1'}
-        )
-
-    def test_env_parse(self):
-        server = Server()
-        head, tail = server.env_parse("intro x; apply a", category="tactic")
-        self.assertEqual(head, "intro x")
-        self.assertEqual(tail, "; apply a")
-
-    def test_goal_state_pickling(self):
-        import tempfile
-        server = Server()
-        state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
-        with tempfile.TemporaryDirectory() as td:
-            path = td + "/goal-state.pickle"
-            server.goal_save(state0, path)
-            state0b = server.goal_load(path)
-            self.assertEqual(state0b.goals, [
-                Goal(
-                    "_uniq.9",
-                    variables=[
-                    ],
-                    target="∀ (p q : Prop), p ∨ q → q ∨ p",
-                )
-            ])
-
-    def test_load_header(self):
-        server = Server(imports=[])
-        server.load_header("import Init\nopen Nat")
-        state0 = server.goal_start("forall (n : Nat), n + 1 = n.succ")
-        state1 = server.goal_tactic(state0, "intro")
-        state2 = server.goal_tactic(state1, "apply add_one")
-        self.assertTrue(state2.is_solved)
-
-    def test_check_compile(self):
-        server = Server()
-        unit, = server.check_compile("example (p: Prop) : p -> p := id")
-        self.assertEqual(unit.messages, [])
-        unit, = server.check_compile("example (p: Prop) : p -> p := 1")
-        self.assertEqual(unit.messages, [Message(
-            pos=Position(1, 30),
-            pos_end=Position(1, 31),
-            data=
-            "numerals are data in Lean, but the expected type is "
-            "a proposition\n"
-            "  p → p : Prop"
-        )
-        ])
-        unit, = server.check_compile("import Lean\nexample (p: Prop) : p -> p := id", read_header=True)
-        self.assertEqual(unit.messages, [])
-
-    def test_load_definitions(self):
-        server = Server()
-        server.load_definitions(
-            "def mystery (x : Nat) := x + 123"
-        )
-        inspect_result = server.env_inspect(name="mystery")
-        self.assertEqual(inspect_result['type'], {'pp': 'Nat → Nat'})
-
-    def test_load_sorry(self):
-        server = Server()
-        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry")
-        #self.assertIsNotNone(unit.goal_state, f"{unit.messages}")
-        state0 = unit.goal_state
-        self.assertEqual(state0.goals, [
-            Goal(
-                "_uniq.5",
-                [Variable(name="p", t="Prop")],
-                target="p → p",
-            ),
-        ])
-        state1 = server.goal_tactic(state0, tactic="intro h")
-        state2 = server.goal_tactic(state1, tactic="exact h")
-        self.assertTrue(state2.is_solved)
-
-        state1b = server.goal_tactic(state0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry"))
-        self.assertEqual(state1b.goals, [
-            Goal(
-                "_uniq.19",
-                [Variable(name="p", t="Prop")],
-                target="p ∨ p",
-            ),
-            Goal(
-                "_uniq.21",
-                [
-                    Variable(name="p", t="Prop"),
-                    Variable(name="h1", t="p ∨ p", v="?m.7"),
-                ],
-                target="p → p",
-            ),
-        ])
-
-    def test_distil_search_target(self):
-        server = Server()
-        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry", ignore_values = True)
-        state0 = unit.goal_state
-        self.assertEqual(state0.goals, [
-            Goal(
-                "_uniq.3",
-                [],
-                target="∀ (p : Prop), p → p",
-            ),
-        ])
-        state1 = server.goal_tactic(state0, tactic="intro p h")
-        state2 = server.goal_tactic(state1, tactic="exact h")
-        self.assertTrue(state2.is_solved)
-
-    def test_distil_coupled(self):
-        server = Server()
-        code = """
-        def f : Nat -> Nat := sorry
-        theorem property (n : Nat) : f n = n := sorry"""
-        unit, = server.load_sorry(code, ignore_values=False)
-        state0 = unit.goal_state
-        self.assertEqual(state0.goals, [
-            Goal(
-                "_uniq.7",
-                [],
-                name='f',
-                target="Nat → Nat",
-            ),
-            Goal(
-                "_uniq.10",
-                [Variable(name='n', t='Nat')],
-                target="?f n = n",
-            ),
-        ])
-
-    def test_check_track(self):
-        server = Server()
-        src = "def f : Nat -> Nat := sorry"
-        dst = "def f : Nat -> Nat := fun y => y + y"
-        self.assertTrue(server.check_track(src, dst).succeeded)
-
-    def test_refactor_search_target(self):
-        code = """
-        def f : Nat -> Nat := sorry
-        theorem property (n : Nat) : f n = n := sorry"""
-        target = """
-def f_composite : { f : Nat → Nat // ∀ (n : Nat), f n = n } :=
-  sorry"""
-        server = Server()
-        result = server.refactor_search_target(code)
-        self.assertEqual(result, target)
-
-if __name__ == '__main__':
-    unittest.main()

PyPantograph/pantograph/utils.py

@@ -1,48 +0,0 @@
-import asyncio
-from pathlib import Path
-import functools as F
-
-DEFAULT_EVENT_LOOP = asyncio.new_event_loop()
-
-def get_event_loop():
-    try:
-        return asyncio.get_event_loop()
-    except RuntimeError:
-        asyncio.set_event_loop(DEFAULT_EVENT_LOOP)
-        return loop
-
-def to_sync(func):
-    loop = get_event_loop()
-    @F.wraps(func)
-    def wrapper(*args, **kwargs):
-        return loop.run_until_complete(func(*args, **kwargs))
-    return wrapper
-
-async def check_output(*args, **kwargs):
-    p = await asyncio.create_subprocess_exec(
-        *args,
-        stdout=asyncio.subprocess.PIPE,
-        stderr=asyncio.subprocess.PIPE,
-        **kwargs,
-    )
-    stdout_data, stderr_data = await p.communicate()
-    if p.returncode == 0:
-        return stdout_data
-
-def _get_proc_cwd():
-    return Path(__file__).parent
-
-def _get_proc_path():
-    return _get_proc_cwd() / "pantograph-repl"
-
-async def get_lean_path_async(project_path):
-    """
-    Extracts the `LEAN_PATH` variable from a project path.
-    """
-    p = await check_output(
-        'lake', 'env', 'printenv', 'LEAN_PATH',
-        cwd=project_path,
-    )
-    return p
-
-get_lean_path = to_sync(get_lean_path_async)

PyPantograph/pyproject.toml

@@ -1,39 +0,0 @@
-[project]
-name = "pantograph"
-version = "0.3.9"
-description = "A machine-to-machine interaction system for Lean"
-license = "Apache-2.0"
-readme = "README.md"
-authors = [
-    {name = "Leni Aniva", email = "aniva@stanford.edu"},
-    {name = "contributors"}
-]
-requires-python = ">=3.11.0"
-dependencies = []
-[dependency-groups]
-dev = [
-    "jupyter-book>=1.0.4.post1",
-    "notebook",
-    "pytest>=8.4.1",
-]
-
-[build-system]
-requires = ["poetry-core>=2,<3"]
-build-backend = "poetry.core.masonry.api"
-
-[tool.poetry]
-include = [
-    { path = "pantograph/pantograph-repl", format = ["sdist", "wheel"] },
-    { path = "pantograph/lean-toolchain", format = ["sdist", "wheel"] },
-    { path = "src", format = ["sdist", "wheel"] },
-]
-
-[tool.poetry.build]
-generate-setup-file = false
-script = "build-pantograph.py"
-
-[tool.poetry.group.doc]
-optional = true
-[tool.poetry.group.doc.dependencies]
-notebook = "^7.2.1"
-jupyter-book = "^1.0.3"

PyPantograph/src/.gitignore

@@ -1,6 +0,0 @@
-.*
-!.gitignore
-!.pre-commit-config.yaml
-
-*.[io]lean
-/result

PyPantograph/src/.pre-commit-config.yaml

@@ -1,30 +0,0 @@
-default_install_hook_types:
-- pre-commit
-- commit-msg
-repos:
-- repo: https://github.com/pre-commit/pre-commit-hooks
-  rev: v6.0.0
-  hooks:
-  - id: check-yaml
-  - id: end-of-file-fixer
-  - id: trailing-whitespace
-  - id: check-symlinks
-  - id: check-added-large-files
-  - id: check-merge-conflict
-  - id: detect-private-key
-  - id: forbid-submodules
-  - id: no-commit-to-branch
-    args: [ --branch, main, --branch, dev ]
-- repo: https://github.com/compilerla/conventional-pre-commit
-  rev: v4.3.0
-  hooks:
-  - id: conventional-pre-commit
-    stages: [commit-msg]
-    args: [feat, fix, doc, chore, test, build, merge, refactor]
-- repo: local
-  hooks:
-  - id: format nix
-    name: Format Nix Code
-    language: system
-    entry: nix fmt
-    files: .*\.nix$

PyPantograph/src/LICENSE

@@ -1,190 +0,0 @@
-                                 Apache License
-                           Version 2.0, January 2004
-                        http://www.apache.org/licenses/
-
-   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
-
-   1. Definitions.
-
-      "License" shall mean the terms and conditions for use, reproduction,
-      and distribution as defined by Sections 1 through 9 of this document.
-
-      "Licensor" shall mean the copyright owner or entity authorized by
-      the copyright owner that is granting the License.
-
-      "Legal Entity" shall mean the union of the acting entity and all
-      other entities that control, are controlled by, or are under common
-      control with that entity. For the purposes of this definition,
-      "control" means (i) the power, direct or indirect, to cause the
-      direction or management of such entity, whether by contract or
-      otherwise, or (ii) ownership of fifty percent (50%) or more of the
-      outstanding shares, or (iii) beneficial ownership of such entity.
-
-      "You" (or "Your") shall mean an individual or Legal Entity
-      exercising permissions granted by this License.
-
-      "Source" form shall mean the preferred form for making modifications,
-      including but not limited to software source code, documentation
-      source, and configuration files.
-
-      "Object" form shall mean any form resulting from mechanical
-      transformation or translation of a Source form, including but
-      not limited to compiled object code, generated documentation,
-      and conversions to other media types.
-
-      "Work" shall mean the work of authorship, whether in Source or
-      Object form, made available under the License, as indicated by a
-      copyright notice that is included in or attached to the work
-      (an example is provided in the Appendix below).
-
-      "Derivative Works" shall mean any work, whether in Source or Object
-      form, that is based on (or derived from) the Work and for which the
-      editorial revisions, annotations, elaborations, or other modifications
-      represent, as a whole, an original work of authorship. For the purposes
-      of this License, Derivative Works shall not include works that remain
-      separable from, or merely link (or bind by name) to the interfaces of,
-      the Work and Derivative Works thereof.
-
-      "Contribution" shall mean any work of authorship, including
-      the original version of the Work and any modifications or additions
-      to that Work or Derivative Works thereof, that is intentionally
-      submitted to Licensor for inclusion in the Work by the copyright owner
-      or by an individual or Legal Entity authorized to submit on behalf of
-      the copyright owner. For the purposes of this definition, "submitted"
-      means any form of electronic, verbal, or written communication sent
-      to the Licensor or its representatives, including but not limited to
-      communication on electronic mailing lists, source code control systems,
-      and issue tracking systems that are managed by, or on behalf of, the
-      Licensor for the purpose of discussing and improving the Work, but
-      excluding communication that is conspicuously marked or otherwise
-      designated in writing by the copyright owner as "Not a Contribution."
-
-      "Contributor" shall mean Licensor and any individual or Legal Entity
-      on behalf of whom a Contribution has been received by Licensor and
-      subsequently incorporated within the Work.
-
-   2. Grant of Copyright License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      copyright license to reproduce, prepare Derivative Works of,
-      publicly display, publicly perform, sublicense, and distribute the
-      Work and such Derivative Works in Source or Object form.
-
-   3. Grant of Patent License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      (except as stated in this section) patent license to make, have made,
-      use, offer to sell, sell, import, and otherwise transfer the Work,
-      where such license applies only to those patent claims licensable
-      by such Contributor that are necessarily infringed by their
-      Contribution(s) alone or by combination of their Contribution(s)
-      with the Work to which such Contribution(s) was submitted. If You
-      institute patent litigation against any entity (including a
-      cross-claim or counterclaim in a lawsuit) alleging that the Work
-      or a Contribution incorporated within the Work constitutes direct
-      or contributory patent infringement, then any patent licenses
-      granted to You under this License for that Work shall terminate
-      as of the date such litigation is filed.
-
-   4. Redistribution. You may reproduce and distribute copies of the
-      Work or Derivative Works thereof in any medium, with or without
-      modifications, and in Source or Object form, provided that You
-      meet the following conditions:
-
-      (a) You must give any other recipients of the Work or
-          Derivative Works a copy of this License; and
-
-      (b) You must cause any modified files to carry prominent notices
-          stating that You changed the files; and
-
-      (c) You must retain, in the Source form of any Derivative Works
-          that You distribute, all copyright, patent, trademark, and
-          attribution notices from the Source form of the Work,
-          excluding those notices that do not pertain to any part of
-          the Derivative Works; and
-
-      (d) If the Work includes a "NOTICE" text file as part of its
-          distribution, then any Derivative Works that You distribute must
-          include a readable copy of the attribution notices contained
-          within such NOTICE file, excluding those notices that do not
-          pertain to any part of the Derivative Works, in at least one
-          of the following places: within a NOTICE text file distributed
-          as part of the Derivative Works; within the Source form or
-          documentation, if provided along with the Derivative Works; or,
-          within a display generated by the Derivative Works, if and
-          wherever such third-party notices normally appear. The contents
-          of the NOTICE file are for informational purposes only and
-          do not modify the License. You may add Your own attribution
-          notices within Derivative Works that You distribute, alongside
-          or as an addendum to the NOTICE text from the Work, provided
-          that such additional attribution notices cannot be construed
-          as modifying the License.
-
-      You may add Your own copyright statement to Your modifications and
-      may provide additional or different license terms and conditions
-      for use, reproduction, or distribution of Your modifications, or
-      for any such Derivative Works as a whole, provided Your use,
-      reproduction, and distribution of the Work otherwise complies with
-      the conditions stated in this License.
-
-   5. Submission of Contributions. Unless You explicitly state otherwise,
-      any Contribution intentionally submitted for inclusion in the Work
-      by You to the Licensor shall be under the terms and conditions of
-      this License, without any additional terms or conditions.
-      Notwithstanding the above, nothing herein shall supersede or modify
-      the terms of any separate license agreement you may have executed
-      with Licensor regarding such Contributions.
-
-   6. Trademarks. This License does not grant permission to use the trade
-      names, trademarks, service marks, or product names of the Licensor,
-      except as required for reasonable and customary use in describing the
-      origin of the Work and reproducing the content of the NOTICE file.
-
-   7. Disclaimer of Warranty. Unless required by applicable law or
-      agreed to in writing, Licensor provides the Work (and each
-      Contributor provides its Contributions) on an "AS IS" BASIS,
-      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-      implied, including, without limitation, any warranties or conditions
-      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
-      PARTICULAR PURPOSE. You are solely responsible for determining the
-      appropriateness of using or redistributing the Work and assume any
-      risks associated with Your exercise of permissions under this License.
-
-   8. Limitation of Liability. In no event and under no legal theory,
-      whether in tort (including negligence), contract, or otherwise,
-      unless required by applicable law (such as deliberate and grossly
-      negligent acts) or agreed to in writing, shall any Contributor be
-      liable to You for damages, including any direct, indirect, special,
-      incidental, or consequential damages of any character arising as a
-      result of this License or out of the use or inability to use the
-      Work (including but not limited to damages for loss of goodwill,
-      work stoppage, computer failure or malfunction, or any and all
-      other commercial damages or losses), even if such Contributor
-      has been advised of the possibility of such damages.
-
-   9. Accepting Warranty or Additional Liability. While redistributing
-      the Work or Derivative Works thereof, You may choose to offer,
-      and charge a fee for, acceptance of support, warranty, indemnity,
-      or other liability obligations and/or rights consistent with this
-      License. However, in accepting such obligations, You may act only
-      on Your own behalf and on Your sole responsibility, not on behalf
-      of any other Contributor, and only if You agree to indemnify,
-      defend, and hold each Contributor harmless for any liability
-      incurred by, or claims asserted against, such Contributor by reason
-      of your accepting any such warranty or additional liability.
-
-   END OF TERMS AND CONDITIONS
-
-   Copyright 2024 Leni Aniva
-
-   Licensed under the Apache License, Version 2.0 (the "License");
-   you may not use this file except in compliance with the License.
-   You may obtain a copy of the License at
-
-       http://www.apache.org/licenses/LICENSE-2.0
-
-   Unless required by applicable law or agreed to in writing, software
-   distributed under the License is distributed on an "AS IS" BASIS,
-   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-   See the License for the specific language governing permissions and
-   limitations under the License.

PyPantograph/src/Main.lean

@@ -1,80 +0,0 @@
-import Lean.Data.Json
-import Lean.Environment
-
-import Pantograph
-import Repl
-
--- Main IO functions
-open Pantograph.Repl
-open Pantograph.Protocol
-
-/-- Print a string to stdout without buffering -/
-def printImmediate (s : String) : IO Unit := do
-  let stdout ← IO.getStdout
-  stdout.putStr (s ++ "\n")
-  stdout.flush
-
-/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parseCommand (s: String): Except String Command := do
-  match s.trim.get? 0 with
-  | .some '{' =>
-    -- Parse in Json mode
-    Lean.fromJson? (← Lean.Json.parse s)
-  | .some _ =>
-    -- Parse in line mode
-    let offset := s.posOf ' ' |> s.offsetOfPos
-    if offset = s.length then
-      return { cmd := s.take offset, payload := Lean.Json.null }
-    else
-      let payload ← s.drop offset |> Lean.Json.parse
-      return { cmd := s.take offset, payload := payload }
-  | .none =>
-    throw "Command is empty"
-
-partial def loop : MainM Unit := do repeat do
-  let state ← get
-  let command ← (← IO.getStdin).getLine
-  -- Halt the program if empty line is given
-  if command.trim.length = 0 then break
-  match parseCommand command with
-  | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
-    -- Using `Lean.Json.compress` here to prevent newline
-    printImmediate error.compress
-  | .ok command =>
-    try
-      let ret ← execute command
-      let str := match state.options.printJsonPretty with
-        | true => ret.pretty
-        | false => ret.compress
-      printImmediate str
-    catch e =>
-      let message := e.toString
-      let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      printImmediate error.compress
-
-def main (args: List String): IO Unit := do
-  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
-  if args == ["--version"] then do
-    IO.println s!"{Pantograph.version}"
-    return
-
-  unsafe do
-    Pantograph.initSearch
-
-  -- Separate imports and options
-  let (options, imports) := args.partition (·.startsWith "--")
-  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
-  let env ← Lean.importModules
-    (imports := imports.toArray.map ({ module := ·.toName }))
-    (opts := {})
-    (trustLevel := 1)
-    (loadExts := true)
-  try
-    let mainM := loop.run { coreContext } |>.run' { env }
-    printImmediate "ready."
-    mainM
-  catch ex =>
-    let message := ex.toString
-    let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)
-    IO.println error.compress

PyPantograph/src/Pantograph.lean

@@ -1,9 +0,0 @@
-import Pantograph.Delate
-import Pantograph.Elab
-import Pantograph.Environment
-import Pantograph.Frontend
-import Pantograph.Goal
-import Pantograph.Library
-import Pantograph.Protocol
-import Pantograph.Serial
-import Pantograph.Version