verify: Replay a Lean project into one kernel environment, importing the toolchain once by SwayamInSync · Pull Request #63 · SwayamInSync/cpp-verify

verify: Replay a Lean project into one kernel environment, importing the toolchain once.

SwayamInSync

committed

128a6cb

test: Add a program whose first goal sorts before the other function's goals.

SwayamInSync

committed

62cac8d

test: Add a proof of the first goal that defines a goal of its own under its name.

SwayamInSync

committed

9d85f6e

test: Expect a proof file that redeclares its goal to be the module left out, also when it comes first.

SwayamInSync

committed

fe6fc92

test: Add a wrapper that bounds the peak memory of the processes a command runs.

SwayamInSync

committed

f716cd7

test: Bound the Lean checker's memory where a proof imports Lean through a rejected module.

SwayamInSync

committed

a9098e0

docs: Say that certification imports the toolchain once and rejects a module that redeclares a name.

SwayamInSync

committed

f814f9f

docs: Say in the release notes that the checker replays into one environment.

SwayamInSync

committed

ed50d74

docs: Describe the checker's single kernel environment in the design.

SwayamInSync

committed

e918963

docs: Describe the checker's single kernel environment and its memory in the architecture.

SwayamInSync

committed

c55de5b

Navigation Menu

Repository navigation

verify: Replay a Lean project into one kernel environment, importing the toolchain once - #63

verify: Replay a Lean project into one kernel environment, importing the toolchain once#63
SwayamInSync merged 10 commits into
mainfrom
fix/lean-certifier-memory

Commits on Oct 24, 2026

verify: Replay a Lean project into one kernel environment, importing the toolchain once.

test: Add a program whose first goal sorts before the other function's goals.

test: Add a proof of the first goal that defines a goal of its own under its name.

test: Expect a proof file that redeclares its goal to be the module left out, also when it comes first.

test: Add a wrapper that bounds the peak memory of the processes a command runs.

test: Bound the Lean checker's memory where a proof imports Lean through a rejected module.

docs: Say that certification imports the toolchain once and rejects a module that redeclares a name.

docs: Say in the release notes that the checker replays into one environment.

docs: Describe the checker's single kernel environment in the design.

docs: Describe the checker's single kernel environment and its memory in the architecture.