### Install LeanDojo
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Install the LeanDojo library using pip. You can install from PyPI or from a local source.
```bash
pip install lean-dojo
# or from source
pip install .
```
--------------------------------
### Install LeanDojo from Git Repo
Source: https://github.com/lean-dojo/leandojo/blob/main/README.md
Install LeanDojo locally from its Git repository. This method is useful for development or when using the latest unreleased changes.
```bash
pip install .
```
--------------------------------
### Install LeanDojo via Pip
Source: https://github.com/lean-dojo/leandojo/blob/main/README.md
Install the LeanDojo library from PyPI using pip. Ensure you have Python 3.9-3.12 and other requirements met.
```bash
pip install lean-dojo
```
--------------------------------
### Initialize Lean Dojo and Inspect Initial State
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Initializes a Lean dojo environment for a given theorem and displays the initial tactic state. This is the starting point for most theorem proving interactions.
```python
dojo, state_0 = Dojo(theorem).__enter__()
```
```python
state_0
```
--------------------------------
### Run Tactic: simp
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Executes the 'simp' tactic, which simplifies expressions. This example shows it completing the proof, resulting in a ProofFinished state.
```python
state_4 = dojo.run_tac(state_3, "simp")
print(state_4)
```
--------------------------------
### Lean 4 Theorem Definitions
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
Example Lean 4 code defining two theorems: `hello_world` and `foo`. The `hello_world` theorem demonstrates theorem proving steps using `rw` and `add_comm`, while `foo` uses `rfl` for reflexivity.
```lean
open Nat (add_assoc add_comm)
theorem hello_world (a b c : Nat)
: a + b + c = a + c + b := by
rw [add_assoc, add_comm b, ←add_assoc]
theorem foo (a : Nat) : a + 1 = Nat.succ a := by rfl
```
--------------------------------
### Get Theorem Start and End Positions
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieve the start and end positions of a theorem within its Lean file using `thm.start` and `thm.end`.
```python
thm.start, thm.end
```
--------------------------------
### get_lean_version
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/trace.md
Retrieves the version of the Lean installation.
```APIDOC
## get_lean_version
### Description
Get the version of Lean.
### Signature
`get_lean_version() -> str`
```
--------------------------------
### check_git_version()
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/api-reference.md
Checks if the installed Git version is compatible with Lean Dojo.
```APIDOC
## check_git_version()
### Description
Verifies that the installed Git version meets the requirements for Lean Dojo.
### Method
`check_git_version()`
### Parameters
None
### Response
None
### Example
```python
from lean_dojo import check_git_version
check_git_version()
```
```
--------------------------------
### Access Theorem Statement, Proof, and Premises
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Use TracedTheorem to get the theorem statement, check for a tactic proof, retrieve the proof itself, and list all premises used in the proof.
```python
from lean_dojo import LeanGitRepo, trace, Theorem
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
traced_repo = trace(repo)
thm_obj = Theorem(repo, "Lean4Example.lean", "hello_world")
traced_thm = traced_repo.get_traced_theorem(thm_obj)
print(traced_thm.get_theorem_statement())
# theorem hello_world (a b c : Nat) : a + b + c = a + c + b
print(traced_thm.has_tactic_proof()) # True
print(traced_thm.get_tactic_proof())
# by\n rw [add_assoc, add_comm b, ←add_assoc]
print(traced_thm.get_num_tactics()) # 1
print(traced_thm.is_private) # False
# Premises referenced in the proof
for name in traced_thm.get_premise_full_names():
print(name)
# Nat.add_assoc, Nat.add_comm, ...
# Traced tactics with before/after states
for tac in traced_thm.get_traced_tactics():
print("Tactic:", tac.tactic)
print("Before:", tac.state_before)
print("After: ", tac.state_after)
annotated, provenance = tac.get_annotated_tactic()
print("Annotated:", annotated)
# rw [add_assoc, add_comm b, ←add_assoc]
```
--------------------------------
### Apply Rewrite Rules in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
Use the `rw` tactic to apply rewrite rules for simplifying expressions. This example demonstrates applying `add_assoc` and `add_comm` to simplify an arithmetic expression.
```Lean
example (a b c : Nat) : a + b + c = a + c + b :=
by
rw [add_assoc, add_comm b, ←add_assoc]
```
--------------------------------
### Get Premise Definitions in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Extracts premise definitions from a traced Lean file. This is useful for understanding the context and dependencies of a theorem or definition.
```python
traced_file.get_premise_definitions()
```
--------------------------------
### Get Lean Toolchain Configuration
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieves the 'lean-toolchain' configuration from the LeanGitRepo. This configuration specifies the Lean version used by the project.
```python
repo.get_config("lean-toolchain")
```
--------------------------------
### Get Traced Theorems in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieves all traced theorems from a Lean file. Useful for analyzing the theorems available in a project.
```python
traced_theorems = traced_file.get_traced_theorems()
len(traced_theorems)
```
--------------------------------
### Lean 4 Example Trace XML Structure
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
An excerpt from a `*.trace.xml` file, showing the hierarchical structure of a Lean 4 file's parsed data. It includes nodes for modules, declarations, theorems, and their associated metadata like start/end positions and identifiers.
```xml
```
--------------------------------
### Build Documentation with Sphinx
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/developer-guide.md
Build the project's documentation using Sphinx. Navigate to the docs directory, clean previous builds, and then generate the HTML documentation.
```bash
cd docs && make clean && make html && cd ..
```
--------------------------------
### Load and Initialize Lean Git Repository
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/extract-complete-proofs.ipynb
Load a specific version of the mathlib repository from GitHub using LeanGitRepo. This is the first step in preparing the repository for tracing.
```python
repo = LeanGitRepo(
"https://github.com/leanprover-community/mathlib",
"19c869efa56bbb8b500f2724c0b77261edbfa28c",
)
repo
```
--------------------------------
### Comment Class
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/traced_data.md
Represents a comment within a Lean file, including its start and end positions and the comment text.
```APIDOC
## class lean_dojo.data_extraction.traced_data.Comment
### Description
A comment in a Lean file.
### Attributes
- **start** ([Pos](lean.md#lean_dojo.data_extraction.lean.Pos)) - The starting position of the comment.
- **end** ([Pos](lean.md#lean_dojo.data_extraction.lean.Pos)) - The ending position of the comment.
- **text** (str) - The content of the comment.
### Class Methods
#### from_xml(tree: Element) -> Comment
Creates a Comment object from an XML tree.
### Methods
#### to_xml(parent: Element) -> None
Serializes the Comment object to XML.
```
--------------------------------
### Run Arbitrary Lean Commands with Dojo.run_cmd
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Interact with Lean as a general REPL using Dojo.run_cmd when Dojo is initialized with a file path and line number. Supports commands like #check, #eval, and definitions.
```python
from pathlib import Path
from lean_dojo import LeanGitRepo, Dojo, CommandState, LeanError
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
entry = (repo, Path("Lean4Example.lean"), 1) # (repo, file, line_nb)
with Dojo(entry, timeout=60) as (dojo, init_state):
assert isinstance(init_state, CommandState)
result = dojo.run_cmd(init_state, "#check Nat.add_assoc")
if isinstance(result, CommandState):
print(result.message)
# Nat.add_assoc : ∀ (n m k : ℕ), n + m + k = n + (m + k)
result2 = dojo.run_cmd(result, "#eval 2 + 2")
if isinstance(result2, CommandState):
print(result2.message) # 4
result3 = dojo.run_cmd(result2, "def bad : Nat := \"oops\"")
if isinstance(result3, LeanError):
print(result3.error)
```
--------------------------------
### Get Number of Tactics in Proof
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieve the total number of tactics used in a theorem's proof with `thm.get_num_tactics()`.
```python
thm.get_num_tactics()
```
--------------------------------
### Get Specific Traced File in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieves a specific traced Lean file by its path within the repository.
```python
traced_file = traced_repo.get_traced_file("Mathlib/Algebra/BigOperators/Pi.lean")
traced_file
```
--------------------------------
### launch_progressbar
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/trace.md
Launches an asynchronous progress bar to monitor the tracing progress of a repository.
```APIDOC
## launch_progressbar
### Description
Launch an async progressbar to monitor the progress of tracing the repo.
### Parameters
* **paths** (*List*[*Path*]) – A list of paths to monitor.
### Returns
A generator that yields None, used for monitoring progress.
### Return type
Generator[None, None, None]
### Signature
`launch_progressbar(paths: List[Path]) -> Generator[None, None, None]`
```
--------------------------------
### Initialize Lean Dojo for Command Execution
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Initializes a Lean dojo environment for executing Lean commands, referencing a specific file and line number. The initial state for commands is CommandState.
```python
entry = (repo, "Mathlib/Algebra/Module/Equiv.lean", 953) # (repo, file_path, line_nb)
dojo, state_0 = Dojo(entry).__enter__()
```
```python
state_0
```
--------------------------------
### Retrieve Traced Tactics
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Get a list of all traced tactics applied during the proof using `thm.get_traced_tactics()`. Each element in the list is a `TracedTactic` object.
```python
traced_tactics = thm.get_traced_tactics()
traced_tactics
```
--------------------------------
### Build and Publish Package with Hatch
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/developer-guide.md
Build the LeanDojo package for distribution and publish it to PyPI using Hatch. These commands are typically for release management.
```bash
hatch build
```
```bash
hatch publish
```
--------------------------------
### Import LeanDojo Libraries
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/extract-complete-proofs.ipynb
Import necessary components from the lean_dojo library to begin data extraction.
```python
import json
from lean_dojo import *
```
--------------------------------
### Instantiate a Theorem Object
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Create a `Theorem` object by providing the `LeanGitRepo`, file path, and full theorem name. This object represents a specific theorem within a repository.
```python
theorem = Theorem(repo, "Mathlib/Algebra/BigOperators/Pi.lean", "pi_eq_sum_univ")
```
--------------------------------
### TacticTacticseqbracketedNode
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Represents a bracketed tactic sequence node. It extends the base Node with properties for state before/after and the tactic itself, and offers a method to get tactic nodes.
```APIDOC
## class lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode
Bases: [`Node`](#lean_dojo.data_extraction.ast.Node)
#### *classmethod* from_data(node_data: Dict[str, Any], lean_file: [LeanFile](lean.md#lean_dojo.data_extraction.lean.LeanFile)) → [TacticTacticseqbracketedNode](#lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode)
#### get_tactic_nodes(atomic_only: bool = False) → Generator[[Node](#lean_dojo.data_extraction.ast.Node), None, None]
#### state_after *: str | None* *= None*
#### state_before *: str | None* *= None*
#### tactic *: str | None* *= None*
#### *property* tactic_nodes *: List[[Node](#lean_dojo.data_extraction.ast.Node)]*
```
--------------------------------
### Interactive Theorem Proving with Dojo
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Use the Dojo class as a context manager for programmatic interaction with Lean. It spawns a Lean REPL subprocess and handles tactic execution, returning states or errors.
```python
from lean_dojo import (
LeanGitRepo, Theorem, Dojo,
TacticState, ProofFinished, LeanError, ProofGivenUp,
DojoCrashError, DojoTacticTimeoutError, DojoInitError,
)
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
try:
with Dojo(theorem, timeout=60) as (dojo, init_state):
assert isinstance(init_state, TacticState)
print(init_state.pp)
# a b c : Nat
# ⊢ a + b + c = a + c + b
print(init_state.num_goals) # 1
# Apply a correct tactic
result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
assert isinstance(result, ProofFinished)
print(result)
# ProofFinished(tactic_state_id=1, message='')
# Apply a wrong tactic — returns LeanError, does not crash
result2 = dojo.run_tac(init_state, "ring")
if isinstance(result2, LeanError):
print("Error:", result2.error)
elif isinstance(result2, TacticState):
print("New goals:", result2.pp)
except DojoInitError as e:
print("Initialization failed:", e)
except DojoCrashError as e:
print("Lean crashed:", e, "OOM:", e.is_out_of_memory)
except DojoTacticTimeoutError:
print("Tactic timed out")
```
--------------------------------
### Get Specific Traced Theorem in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Retrieves a specific traced theorem by its full name. Use this when you need to inspect or work with a particular theorem.
```python
thm = traced_file.get_traced_theorem("pi_eq_sum_univ")
thm
```
--------------------------------
### Prove Theorem with Tactic `rw` in Lean
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/user-guide.md
Demonstrates proving a theorem using the `rw` tactic with `add_assoc` and `add_comm` premises. Ensure necessary imports like `open nat` are included.
```lean
open nat (add_assoc add_comm)
theorem hello_world (a b c : ℕ) : a + b + c = a + c + b :=
begin
rw [add_assoc, add_comm b, ←add_assoc]
end
```
--------------------------------
### Execute Lean Command: #eval 1
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Executes the Lean command '#eval 1' and returns the result. This demonstrates basic evaluation of expressions.
```python
dojo.run_cmd(state_0, "#eval 1")
```
--------------------------------
### Lean 4 Tactic State and Proof Finished Output
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
This output shows the initial tactic state before applying tactics and the final `ProofFinished` status after successfully completing the proof.
```default
TacticState(pp='a b c : Nat
⊢ a + b + c = a + c + b', id=0, message=None)
ProofFinished(tactic_state_id=1, message='')
```
--------------------------------
### LeanGitRepo Initialization
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Initialize a LeanGitRepo object to represent a Lean 4 project from a URL or local path.
```APIDOC
## LeanGitRepo
`LeanGitRepo(url, commit)` is the entry point for identifying any Lean 4 project. The `url` may be a GitHub HTTPS URL, an SSH URL (auto-converted), or a local path. The `commit` may be a full 40-character hash or a tag/branch name (resolved to a hash automatically). The object exposes the required Lean version, dependency graph, and repo type.
### Usage
```python
from lean_dojo import LeanGitRepo, get_latest_commit
# Point to a specific commit
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
print(repo.name) # "lean4-example"
print(repo.lean_version) # e.g. "v4.3.0"
print(repo.commit_url) # full GitHub tree URL
# Resolve HEAD automatically
latest = get_latest_commit("https://github.com/yangky11/lean4-example")
repo_head = LeanGitRepo("https://github.com/yangky11/lean4-example", latest)
# From a local git repo
repo_local = LeanGitRepo.from_path("/path/to/my-lean-project")
# Inspect dependencies
deps = repo.get_dependencies()
# {"lean4": LeanGitRepo(...), "Mathlib": LeanGitRepo(...), ...}
for name, dep in deps.items():
print(name, dep.commit)
```
```
--------------------------------
### Lean 3 Project Configuration (leanpkg.toml)
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/user-guide.md
Configuration file for Lean 3 projects, specifying package details, Lean version, source directory, and dependencies.
```toml
[package]
name = "lean-liquid"
version = "0.1"
lean_version = "leanprover-community/lean:3.48.0"
path = "src"
[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5947fb69cc1fdfebaba1e1b1f0a04f26f0f612bf"}
```
--------------------------------
### Define a Theorem in Lean 4
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
Demonstrates how to define a simple theorem in Lean 4, specifying its type signature and proof.
```lean
theorem foo (a : Nat) : a + 1 = Nat.succ a :=
by
sorry
```
--------------------------------
### Trace a Lean Repository and Access Theorems
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Use TracedRepo to wrap a Lean repository, access all theorems, and look up specific theorems. It can also save and load repository traces.
```python
from lean_dojo import LeanGitRepo, trace, TracedRepo, Theorem
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
traced_repo = trace(repo)
# Iterate all traced theorems in the repo (including dependencies)
all_theorems = traced_repo.get_traced_theorems()
print(f"Total theorems: {len(all_theorems)}")
# Look up a specific theorem
thm = Theorem(repo, "Lean4Example.lean", "hello_world")
traced_thm = traced_repo.get_traced_theorem(thm)
print(traced_thm.get_theorem_statement())
# "theorem hello_world (a b c : Nat) : a + b + c = a + c + b"
# Save XML representations of all traced files to disk
traced_repo.save_to_disk()
# Load a previously saved traced repo
traced_repo2 = TracedRepo.load_from_disk("traced_lean4-example/lean4-example")
traced_repo2.check_sanity()
```
--------------------------------
### Dojo Class
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/dojo.md
The Dojo class provides a gym-like environment for programmatic interaction with Lean. It allows users to execute commands and tactics, manage proof states, and handle timeouts and crashes.
```APIDOC
## Class: Dojo
### Description
Gym-like environment for programmatic interaction with Lean through tactics or commands.
### Methods
#### run_cmd(state: CommandState, command: str) -> CommandState | LeanError
Executes a Lean command and returns the resulting command state or a Lean error.
#### run_tac(state: TacticState, tactic: str) -> TacticState | ProofFinished | LeanError | ProofGivenUp
Executes a Lean tactic and returns the resulting tactic state, proof finished, proof given up, or a Lean error.
### Properties
#### additional_imports: List[str]
#### entry: Theorem | Tuple[LeanGitRepo, Path, int]
#### file_path: Path
#### has_timedout: bool
#### is_crashed: bool
#### is_successful: bool | None
#### modified_file: TextIO
#### repo: LeanGitRepo
#### uses_commands: bool
#### uses_tactics: bool
```
--------------------------------
### Exporting metadata
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Exports project metadata, including creation time and LeanDojo version, to a 'metadata.json' file.
```python
def export_metadata(traced_repo: TracedRepo, dst_path: Path, **kwargs) -> None:
"""Export the metadata of a traced repo to ``dst_path''."""
metadata = dict(kwargs)
metadata["creation_time"] = str(datetime.now())
metadata["from_repo"] = {
"url": traced_repo.repo.url,
"commit": traced_repo.repo.commit,
}
metadata["leandojo_version"] = lean_dojo.__version__
json.dump(metadata, (dst_path / "metadata.json").open("wt"))
```
--------------------------------
### Import LeanDojo Library
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Imports the necessary LeanDojo library for use in the notebook.
```python
from lean_dojo import *
```
--------------------------------
### Trace Lean Repository
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/extract-complete-proofs.ipynb
Trace the loaded Lean repository to prepare it for theorem extraction. This step may involve significant processing and logging.
```python
traced_repo = trace(repo)
```
--------------------------------
### Verify a complete proof string with check_proof
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Checks if a complete proof string is accepted by Lean for a given theorem without requiring a Dojo context. Use this to validate proof strings.
```python
from lean_dojo import LeanGitRepo, Theorem
from lean_dojo.interaction.dojo import check_proof
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
thm = Theorem(repo, "Lean4Example.lean", "hello_world")
# Correct proof
ok = check_proof(thm, "by rw [add_assoc, add_comm b, ←add_assoc]")
print(ok) # True
# Wrong proof
ok2 = check_proof(thm, "by ring")
print(ok2) # False
```
--------------------------------
### Extract Proof Node and Code
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Obtain the proof node using `thm.get_proof_node()` and then extract the proof code from the Lean file using slicing with `proof_node.start` and `proof_node.end`.
```python
proof_node = thm.get_proof_node()
proof = proof_node.lean_file[proof_node.start : proof_node.end]
print(proof)
```
--------------------------------
### lean_dojo.interaction.dojo
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/api-reference.md
Core interaction with the Lean environment.
```APIDOC
## `CommandState`
### Description
Represents the state of a Lean command.
## `Dojo`
### Description
Main class for interacting with the Lean environment.
## `DojoCrashError`
### Description
Exception raised when the Lean process crashes.
## `DojoInitError`
### Description
Exception raised during Lean environment initialization.
## `DojoTacticTimeoutError`
### Description
Exception raised when a tactic times out.
## `LeanError`
### Description
Base exception for Lean-related errors.
## `ProofFinished`
### Description
Indicates that a proof has been finished.
## `ProofGivenUp`
### Description
Indicates that the proof process was given up.
## `TacticState`
### Description
Represents the state of a tactic.
## `check_proof(dojo: Dojo, theorem_name: str)`
### Description
Checks if a proof for a given theorem is correct.
### Parameters
#### Path Parameters
- **dojo** (Dojo) - Required - The Dojo instance.
- **theorem_name** (str) - Required - The name of the theorem to check.
## `kill_descendants(pid: int)`
### Description
Kills all descendant processes of a given process ID.
### Parameters
#### Path Parameters
- **pid** (int) - Required - The process ID.
```
--------------------------------
### Configure LeanDojo behavior with environment variables
Source: https://context7.com/lean-dojo/leandojo/llms.txt
LeanDojo's behavior is configured through environment variables. These control cache locations, resource limits, and logging.
```bash
# Cache location (default: ~/.cache/lean_dojo)
export CACHE_DIR=/data/lean_cache
# Force local tracing, disable remote cache download
export DISABLE_REMOTE_CACHE=1
# Temporary working directory
export TMP_DIR=/tmp/lean_dojo_tmp
# Parallel extraction processes (default: min(cpu_count, 32))
export NUM_PROCS=16
# Tactic interaction resource limits
export TACTIC_CPU_LIMIT=2
export TACTIC_MEMORY_LIMIT=16g # must match \d+g
# GitHub API token (increases rate limits)
export GITHUB_ACCESS_TOKEN=ghp_...
# Load only files used by the target repo (faster, uses less memory)
export LOAD_USED_PACKAGES_ONLY=1
# Enable debug/verbose logging
export VERBOSE=1
```
--------------------------------
### Import Libraries and Define Constants for LeanDojo Benchmark
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Imports essential Python libraries and defines constants for constructing the LeanDojo Benchmark 4. This includes setting the source repository, commit hash, destination directory, and the number of theorems for validation and testing.
```python
import json
import shutil
import random
import networkx as nx
from copy import copy
from pathlib import Path
from loguru import logger
from datetime import datetime
from collections import defaultdict
from typing import Dict, List, Union
import lean_dojo
from lean_dojo import *
from lean_dojo.constants import LEAN4_PACKAGES_DIR
random.seed(3407) # https://arxiv.org/abs/2109.08203
URL = "https://github.com/leanprover-community/mathlib4"
COMMIT = "29dcec074de168ac2bf835a77ef68bbe069194c5"
DST_DIR = Path("../leandojo_benchmark_4")
NUM_VAL = NUM_TEST = 2000
```
--------------------------------
### Interact with Lean 4 Theorem
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/getting-started.md
Use this snippet to interact with Lean 4 theorems. Ensure the Lean 4 repository is traced before execution. The `Dojo` context manages the interaction, allowing you to run tactics and inspect proof states.
```python
from lean_dojo import *
repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f")
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
with Dojo(theorem) as (dojo, init_state):
print(init_state)
result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
assert isinstance(result, ProofFinished)
print(result)
```
--------------------------------
### ModulePreludeNode
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Represents the prelude import in a Lean module.
```APIDOC
## Class: ModulePreludeNode
### Description
Represents the prelude import in a Lean module.
### Class Methods
#### classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) -> ModulePreludeNode
```
--------------------------------
### CommandDeclvaleqnsNode.from_data
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Class method to create a CommandDeclvaleqnsNode instance from provided node data and Lean file information.
```APIDOC
## classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) -> CommandDeclvaleqnsNode
### Description
Creates a `CommandDeclvaleqnsNode` from a dictionary of data and a `LeanFile` object.
### Parameters
- **node_data** (Dict[str, Any]): A dictionary containing the data for the node.
- **lean_file** (LeanFile): The Lean file object associated with this node.
```
--------------------------------
### Run Tactic: Unknown Tactic
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Attempts to run an unknown tactic ('hello world!') and shows the resulting LeanError. This demonstrates how invalid tactic names are handled.
```python
state_2 = dojo.run_tac(state_0, "hello world!")
state_2
```
--------------------------------
### Run Tactic: ext
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Executes the 'ext' tactic, which is used for extensionality. It transforms the goal to allow for element-wise comparison.
```python
state_3 = dojo.run_tac(state_0, "ext")
print(state_3.pp)
```
--------------------------------
### Exporting licenses
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Exports the licenses of the traced repository and its dependencies into a 'licenses' subdirectory. Includes a README explaining the dataset's license.
```python
def export_licenses(traced_repo: TracedRepo, dst_path: Path) -> None:
"""Export the licenses of a traced repo and all its dependencies to ``dst_path``."""
license_dir = dst_path / "licenses"
license_dir.mkdir()
all_repos = [traced_repo.repo] + list(traced_repo.dependencies.values())
for repo in all_repos:
lic = repo.get_license()
if lic is None:
continue
with (license_dir / repo.name).open("wt") as oup:
oup.write(lic)
with (license_dir / "README.md").open("wt") as oup:
oup.write(
"This directory contains licenses of Lean repos used to generate this dataset. The dataset itself is released under [CC BY 2.0](https://creativecommons.org/licenses/by/2.0/)."
)
```
--------------------------------
### Main data export function
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Orchestrates the export of proofs, premises, licenses, and metadata. Removes the destination directory if it already exists.
```python
def export_data(
traced_repo: TracedRepo,
splits: Dict[SPLIT_STRATEGY, SPLIT],
dst_path: Union[str, Path],
**kwargs,
) -> None:
"""Export a traced repo whose theorems have been splitted to ``dst_path``."""
if isinstance(dst_path, str):
dst_path = Path(dst_path)
if dst_path.exists():
logger.warning(f"{dst_path} already exists. Removing it now.")
shutil.rmtree(dst_path)
# Export the proofs.
export_proofs(splits, dst_path, traced_repo)
```
--------------------------------
### Run Tactic: sorry
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Executes the 'sorry' tactic, which is a placeholder for an unfinished proof. It results in a ProofGivenUp state.
```python
dojo.run_tac(state_0, "sorry")
```
--------------------------------
### Run Tactic: revert
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Executes the 'revert' tactic on the current state and prints the resulting pretty-printed state. 'revert' moves a variable from the local context to the goal.
```python
state_1 = dojo.run_tac(state_0, "revert x")
print(state_1.pp)
```
--------------------------------
### check_proof
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Verifies if a given proof string is accepted by Lean for a specific theorem without needing a full Dojo context.
```APIDOC
## `check_proof` — Verify a complete proof string
`check_proof(thm, proof)` checks whether a complete proof (as a string) is accepted by Lean for a given theorem, without requiring a `Dojo` context.
### Parameters
- **thm** (`Theorem`): The theorem object to check the proof against.
- **proof** (`str`): The proof string to verify.
### Returns
- (`bool`): True if the proof is valid, False otherwise.
### Example
```python
from lean_dojo import LeanGitRepo, Theorem
from lean_dojo.interaction.dojo import check_proof
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
thm = Theorem(repo, "Lean4Example.lean", "hello_world")
# Correct proof
ok = check_proof(thm, "by rw [add_assoc, add_comm b, ←add_assoc]")
print(ok) # True
# Wrong proof
ok2 = check_proof(thm, "by ring")
print(ok2) # False
```
```
--------------------------------
### Goal.from_pp
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/parse_goals.md
Parses a single pretty-printed Lean goal into a Goal object.
```APIDOC
## Goal.from_pp(pp: str) -> Goal
### Description
Parses a pretty-printed goal string into a `Goal` object.
### Method
`classmethod`
### Parameters
#### Arguments
- **pp** (str) - The pretty-printed goal string to parse.
### Returns
- **Goal** - A `Goal` object representing the parsed goal.
```
--------------------------------
### Display Theorem Information
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Use `thm.show()` to open a new tab displaying the theorem's website. Access the theorem's name using `thm.theorem`.
```python
thm.show()
```
```python
thm.theorem
```
--------------------------------
### Exporting LeanDojo Benchmark Data
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
This script initializes a LeanGitRepo, traces it, splits the data, and then exports it to a specified directory with a given dataset name. It handles different splitting strategies and saves data to train, validation, and test JSON files.
```python
repo = LeanGitRepo(URL, COMMIT)
traced_repo = trace(repo)
splits = split_data(traced_repo)
export_data(traced_repo, splits, DST_DIR, dataset_name="LeanDojo Benchmark 4")
```
--------------------------------
### Split Data Using Strategies
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Splits a traced repository's theorems using predefined strategies, including random splitting and splitting by novel premises. Excludes theorems from the Lean 4 repository itself.
```python
def split_data(traced_repo: TracedRepo) -> Dict[SPLIT_STRATEGY, SPLIT]:
# Skip theorems in the Lean 4 repo itself.
traced_theorems = [
thm for thm in traced_repo.get_traced_theorems() if not thm.repo.is_lean4
]
logger.info(f"{len(traced_theorems)} theorems in total")
return {
"random": split_randomly(traced_theorems),
"novel_premises": split_by_premise(traced_theorems),
}
```
--------------------------------
### CommandDefNode.from_data
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Class method to create a CommandDefNode instance from provided node data and Lean file information.
```APIDOC
## classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) -> CommandDefNode
### Description
Creates a `CommandDefNode` from a dictionary of data and a `LeanFile` object.
### Parameters
- **node_data** (Dict[str, Any]): A dictionary containing the data for the node.
- **lean_file** (LeanFile): The Lean file object associated with this node.
### Properties
- **name** (str): The name of the definition.
```
--------------------------------
### CommandDeclidNode.from_data
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Class method to create a CommandDeclidNode instance from provided node data and Lean file information.
```APIDOC
## classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) -> CommandDeclidNode
### Description
Creates a `CommandDeclidNode` from a dictionary of data and a `LeanFile` object.
### Parameters
- **node_data** (Dict[str, Any]): A dictionary containing the data for the node.
- **lean_file** (LeanFile): The Lean file object associated with this node.
```
--------------------------------
### Low-level access to Lean source files with LeanFile
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Provides byte-accurate, line/column-indexed access to Lean source files. Supports slicing by Pos objects and converting between byte offsets and Pos positions.
```python
from pathlib import Path
from lean_dojo.data_extraction.lean import LeanFile, Pos
root = Path("traced_lean4-example/lean4-example").resolve()
lean_file = LeanFile(root, Path("Lean4Example.lean"))
print(lean_file.num_lines) # total number of lines
print(lean_file.start_pos) # Pos(1, 1)
print(lean_file.end_pos) # Pos(N, M)
# Slice source code between two positions
start = Pos(3, 1)
end = Pos(5, 41)
print(lean_file[start:end])
# theorem hello_world (a b c : Nat)
# : a + b + c = a + c + b := by
# rw [add_assoc, add_comm b, ←add_assoc]
# Convert a byte index to a Pos
pos = lean_file.convert_pos(42)
print(pos) # e.g. Pos(3, 9)
# Read a single line
print(lean_file.get_line(3))
# "theorem hello_world (a b c : Nat)"
```
--------------------------------
### Define a Variable and Evaluate
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Defines a variable 'x' using 'def x := 1' and then successfully evaluates it using '#eval x'. This demonstrates defining and using variables within the dojo.
```python
state_1 = dojo.run_cmd(state_0, "def x := 1")
state_1
```
```python
dojo.run_cmd(state_1, "#eval x")
```
--------------------------------
### TokenAntiquotNode.from_data
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/ast.md
Class method to create a TokenAntiquotNode from node data and Lean file information.
```APIDOC
## classmethod TokenAntiquotNode.from_data(node_data: Dict[str, Any], lean_file: LeanFile) -> TokenAntiquotNode
### Description
Creates a `TokenAntiquotNode` instance from provided node data and a `LeanFile` object.
### Parameters
- **node_data** (Dict[str, Any]) - The dictionary containing data for the node.
- **lean_file** (LeanFile) - The `LeanFile` object associated with this node.
```
--------------------------------
### Trace Tactic Execution with TracedTactic
Source: https://context7.com/lean-dojo/leandojo/llms.txt
Use TracedTactic to inspect tactic steps, including state transitions and premise provenance. Access annotated tactics and detailed information about used premises.
```python
from lean_dojo import LeanGitRepo, trace, Theorem
repo = LeanGitRepo(
"https://github.com/yangky11/lean4-example",
"7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f",
)
traced_repo = trace(repo)
thm_obj = Theorem(repo, "Lean4Example.lean", "hello_world")
traced_thm = traced_repo.get_traced_theorem(thm_obj)
for tac in traced_thm.get_traced_tactics(atomic_only=False):
print(repr(tac))
# TracedTactic(tactic=rw [...], state_before=..., state_after=...)
annotated_tac, provenances = tac.get_annotated_tactic()
# annotated_tac: "rw [add_assoc, add_comm b, ←add_assoc]"
for prov in provenances:
print(prov["full_name"]) # e.g. "Nat.add_assoc"
print(prov["def_path"]) # ".lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean"
print(prov["def_pos"]) # [138, 19]
print(prov["def_end_pos"]) # [138, 28]
```
--------------------------------
### Exporting premise definitions to JSONL
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/generate-benchmark-lean4.ipynb
Exports premise definitions from traced files, including their import paths, into a JSON Lines file. Processes files in topological order.
```python
def export_premises(traced_repo: TracedRepo, dst_path: Path) -> None:
"""Export all premise definitions in a traced repo to ``dst_path``."""
oup_path = dst_path / "corpus.jsonl"
num_premises = 0
with oup_path.open("wt") as oup:
G = traced_repo.traced_files_graph
for tf_node in reversed(list(nx.topological_sort(G))):
tf = G.nodes[tf_node]["traced_file"]
imports = [str(_) for _ in G.successors(tf_node)]
premises = tf.get_premise_definitions()
num_premises += len(premises)
oup.write(
json.dumps(
{"path": str(tf.path), "imports": imports, "premises": premises}
)
+ "\n"
)
logger.info(
f"{num_premises} theorems/definitions from {len(traced_repo.traced_files)} files saved to {oup_path}"
)
```
--------------------------------
### Initialize LeanGitRepo
Source: https://github.com/lean-dojo/leandojo/blob/main/scripts/demo-lean4.ipynb
Initializes a LeanGitRepo object to represent a specific Lean project from a GitHub repository and commit hash. This is useful for analyzing specific versions of Lean projects.
```python
repo = LeanGitRepo(
"https://github.com/leanprover-community/mathlib4",
"29dcec074de168ac2bf835a77ef68bbe069194c5",
)
repo
```
--------------------------------
### trace
Source: https://github.com/lean-dojo/leandojo/blob/main/docs/source/trace.md
Traces a Lean repository and its dependencies, saving the results to a specified directory. Uses caching if the repository is already traced.
```APIDOC
## trace
### Description
Trace a repo (and its dependencies), saving the results to `dst_dir`. The function only traces the repo when it’s not available in the cache. Otherwise, it directly copies the traced repo from the cache to `dst_dir`.
### Parameters
* **repo** ([*LeanGitRepo*](lean.md#lean_dojo.data_extraction.lean.LeanGitRepo)) – The Lean repo to trace.
* **dst_dir** (*Union* *[**str* *,* *Path* *]*) – The directory for saving the traced repo. If None, the traced repo is only saved in the cache.
* **build_deps** (*bool*) – Whether to build the dependencies of `repo`. Defaults to True.
### Returns
A `TracedRepo` object corresponding to the files at `dst_dir`.
### Return type
[TracedRepo](traced_data.md#lean_dojo.data_extraction.traced_data.TracedRepo)
### Signature
`trace(repo: LeanGitRepo, dst_dir: str | Path | None = None, build_deps: bool = True) -> TracedRepo`
```