Module replay 

Replaying bounded proof attempts against isolated workspace copies.

Each Attempt names a task, a single bounded edit (the same allowed_edit the miner emits), and the replacement text. Replay copies the Lake project into a throwaway workspace, applies the one span, runs lake lean on the target file, and emits a ReplayResult that decomposes the outcome into whether it compiled, whether the original problem went away, and whether the patch introduced anything new.

Comparisons use an optional baseline: the same target file compiled in an unpatched copy. The baseline for a target file is computed once and reused across attempts, since the unpatched project is identical every time.

Structs

Attempt

One bounded proof attempt to replay.

ReplayOptions

Runtime options for a replay run.

ReplayResult

Result record for one replayed attempt.

ReplaySummary

Counts from a replay run.

Enums

ReplayStatus

Coarse status for one replayed attempt.

Functions

run_replay

Replay every attempt and stream one result record per attempt to writer.