Skip to content

Commit 50cb27b

Browse files
crumplecupCopilot
andcommitted
fix: remove vestigial build.rs from elicit_proofs
build.rs did nothing useful — proofs are pre-generated and committed. Moved the regeneration instructions into README.md instead. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent b64f184 commit 50cb27b

2 files changed

Lines changed: 11 additions & 19 deletions

File tree

crates/elicit_proofs/README.md

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,14 @@
22

33
Formal verification proof harnesses for the elicitation ecosystem.
44

5-
Harnesses are generated at build time by `build.rs` from `VerifiedStateMachine::vsm_kani_proof()` (and future Creusot/Verus equivalents).
5+
Proof files are pre-generated by the `elicitation generate` CLI and committed to the repository.
6+
To regenerate after changing VSM source files:
7+
8+
```text
9+
elicitation generate kani --crate-path crates/elicit_server/src/archive/vsm \
10+
--out crates/elicit_proofs/src/kani/generated
11+
elicitation generate creusot --crate-path crates/elicit_server/src/archive/vsm \
12+
--out crates/elicit_proofs/src/creusot/generated
13+
elicitation generate verus --crate-path crates/elicit_server/src/archive/vsm \
14+
--out crates/elicit_proofs/src/verus/generated
15+
```

crates/elicit_proofs/build.rs

Lines changed: 0 additions & 18 deletions
This file was deleted.

0 commit comments

Comments
 (0)