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.

Attributes:

rootPath

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

lean_toolchainstr

The pinned toolchain, e.g.

mathlib_revstr | None

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

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']

files_with_sorry() → list[Path]

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

lean_files() → list[Path]

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

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/stable/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

Project skeleton to copy the lakefile.toml/lean-toolchain (and, when present, lakefile.lean/lake-manifest.json) from. Default SKELETON_DIR – 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: LeanProject, targets: tuple[~pathlib.Path, ...]=(), user_prompt: str | None = None, metadata: dict[str, str]=<factory>)

A unit of work: complete the sorrys in project.

Attributes:

projectLeanProject

The lake project to complete.

targetstuple[Path, …]

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

user_promptstr | None

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

metadatadict[str, str]

Optional free-form metadata carried alongside the task.

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.

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.

Attributes:

namestr

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

lean_toolchainstr

Lean toolchain baked into the image (see images/lean/lean-toolchain); projects must pin it or the verifier rejects them. Default leanprover/lean4:v4.28.0.

mathlib_revstr

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