lean

The Lean input contract: the project to complete, the task describing what to fill, and the staging helper. A project is a full lake project carrying its own lean-toolchain and lake-manifest.json.

Project

A full lake project on disk is just LeanProject(Path(path)). create_project() stages one or more bare .lean files into the pinned Mathlib skeleton.

class open_atp.lean.LeanProject(root: Path)

A complete lake project on disk.

Parameters:

rootPath

Directory containing lakefile.toml (or lakefile.lean), lean-toolchain, and lake-manifest.json. Resolved to an absolute path.

Examples

Point LeanProject at a lake project directory and inspect it (here a minimal project is written to a temp dir to keep the example self-contained):

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.lean import LeanProject
>>> root = Path(tempfile.mkdtemp())
>>> _ = (root / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (root / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> _ = (root / "Demo.lean").write_text("theorem t : True := by sorry\n")
>>> project = LeanProject(root)
>>> project.lean_toolchain
'leanprover/lean4:v4.31.0'
>>> [p.name for p in project.lean_files()]
['Demo.lean']
>>> [p.name for p in project.files_with_sorry()]
['Demo.lean']

property lean_toolchain: str

The pinned toolchain read from lean-toolchain.

A full toolchain identifier such as leanprover/lean4:v4.31.0, compared against the backend image’s pin before any compute is spent.

property mathlib_rev: str | None

The pinned Mathlib revision from lake-manifest.json, if present.

Prefers the human-declared inputRev (e.g. v4.28.0) so it is comparable to an Image’s declared mathlib_rev, falling back to the resolved git rev (a commit SHA) when no inputRev is recorded.

lean_files() → list[Path]

All .lean source files, excluding build artifacts under .lake.

files_with_sorry() → list[Path]

Lean files that contain a sorry token (cheap textual scan).

open_atp.lean.create_project(files: Sequence[Path | str], dest: Path | str, *, skeleton: Path = PosixPath('/home/docs/checkouts/readthedocs.org/user_builds/open-atp/envs/latest/lib/python3.12/images/lean')) → LeanProject

Stage bare .lean files into the default Mathlib skeleton -> a project.

Convenience for the “upload one or more ``.lean`` files” contract: copies the skeleton’s lakefile.toml + lean-toolchain into dest and drops the files at its root. Limitation: this only works for the pinned toolchain/deps the skeleton (and the baked image) provide – a file needing a different Mathlib revision or extra deps must arrive as a full lake project instead.

Parameters:

filesSequence[Path | str]

Bare .lean files to stage. Each is copied to the root of dest; a non-.lean path raises ValueError.

destPath | str

Destination directory for the new project. Created if missing.

skeletonPath, default SKELETON_DIR

Project skeleton to copy the lakefile.toml/lean-toolchain (and, when present, lakefile.lean/lake-manifest.json) from. The default is the baked image’s skeleton, only present in a source checkout.

Returns:

LeanProject

A complete project rooted at dest, ready to verify.

Examples

Stage a bare .lean file into a skeleton to get a complete LeanProject (here a minimal skeleton is written to a temp dir; in practice skeleton defaults to the baked image’s SKELETON_DIR):

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.lean import create_project
>>> skeleton = Path(tempfile.mkdtemp())
>>> _ = (skeleton / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (skeleton / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> bare = Path(tempfile.mkdtemp()) / "Bare.lean"
>>> _ = bare.write_text("theorem t : True := by sorry\n")
>>> dest = Path(tempfile.mkdtemp()) / "project"
>>> project = create_project([bare], dest, skeleton=skeleton)
>>> project.lean_toolchain
'leanprover/lean4:v4.31.0'
>>> [p.name for p in project.lean_files()]
['Bare.lean']

Task

class open_atp.lean.ProofTask(project: ~open_atp.lean.LeanProject, name: str | None = None, targets: tuple[~pathlib.Path, ...] = (), user_prompt: str | None = None, metadata: dict[str, str] = <factory>)

A unit of work: complete the sorrys in project.

Parameters:

projectLeanProject

The lake project to complete.

namestr, default None

Task identifier, used to attribute log records to this task. Populated when tasks are loaded from a dataset directory; None for a one-off task.

targetstuple[Path, …], default ()

Explicit list of files (relative to project.root) to focus on. When empty, every file containing sorry is fair game.

user_promptstr, default None

Per-task guidance appended below the prover’s own prompt under an # Additional instructions heading. None (the common case) leaves the prover prompt untouched.

metadatadict[str, str], optional

Free-form metadata carried alongside the task. Defaults to an empty mapping.

resolved_targets() → list[Path]

Absolute paths of the files to work on.

The explicit targets (resolved against project.root) when given, else every file containing sorry (files_with_sorry()).

Exceptions

exception open_atp.lean.ToolchainMismatch

Raised when an uploaded project’s toolchain does not match the image’s pin.

exception open_atp.lean.MathlibRevMismatch

Raised when an uploaded project’s Mathlib revision differs from the image’s.

Image defaults

The constants describing the baked sandbox image (the contract the verifier enforces).

open_atp.images.DEFAULT_IMAGE = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0')

The image built from images/Dockerfile – all default pins.

class open_atp.images.Image(name: str = 'open-atp:latest', lean_toolchain: str = 'leanprover/lean4:v4.28.0', mathlib_rev: str = 'v4.28.0')

A sandbox image: its container tag and the Lean pins baked into it.

Carried by a ComputeBackend and used by the Verifier as the compatibility contract: a project must match lean_toolchain (and, when it locks one, mathlib_rev) or it is rejected before any compute is spent.

Parameters:

namestr, default “open-atp:latest”

Container image tag carrying Lean + Mathlib that the sandbox runs. The default is the tag produced by docker build -t open-atp:latest images/.

lean_toolchainstr, default “leanprover/lean4:v4.28.0”

Lean toolchain baked into the image (see images/lean/lean-toolchain); projects must pin it or the verifier rejects them.

mathlib_revstr, default “v4.28.0”

Mathlib revision whose olean cache is pre-baked, matching the declared pin in images/lean/lakefile.toml.

open_atp.images.SKELETON_DIR = PosixPath('/home/docs/checkouts/readthedocs.org/user_builds/open-atp/envs/latest/lib/python3.12/images/lean')

The lake-project skeleton (lakefile.toml + lean-toolchain) matching DEFAULT_IMAGE. Used to stage bare .lean uploads into a full project for the pinned toolchain/deps only. Lives at the repo root in a source checkout.