Module mine 

Mining replayable proof tasks out of a Lean project.

A task points at one precise span the agent is allowed to rewrite: a sorry or admit placeholder, or the declaration around a compiler error. Each MineTask carries enough context (imports, enclosing declaration, the goal state when available) plus an exact target_span and allowed_edit so a later step can splice a candidate proof back in safely.

Placeholder mining (sorry, admit) is a pure text scan that skips comments and string literals, so it needs no Lean toolchain. Error mining runs the file through the tracer and is therefore backed by real diagnostics.

Structs

AllowedEdit

The single contiguous line range a replay step is permitted to edit.

MineOptions

Runtime options for a mine run.

MineSummary

Outcome counts from a single mine run.

MineTask

One mined, replayable proof task.

TargetSpan

The exact span a candidate proof must replace.

Enums

MineKind

What a mine run looks for.

Functions

mine_errors

Mine error tasks from one file’s source plus its tracer diagnostics.

mine_placeholders

Mine sorry/admit placeholder tasks from one file’s source.

run_mine

Discover files under roots, mine tasks of the requested kind, and stream them to writer.