Repository navigation

Open statements and a revision contract for shared Lean declarations - #115

Closed

Deicyde wants to merge 39 commits into

mainfrom

open-statements-revision

Commits on Oct 5, 2026

Make the open-statement policy configurable (spec A1-A5)
Deicyde
committed
62ed473
Pin readiness wording, Assumes row order and the empty open frontier
Deicyde
committed
ce0c123
Cover the unreadable-path and output-error branches of work assumptions
Deicyde
committed
9e29e78
Add all-or-nothing multi-key claims
Deicyde
committed
ac7be46
Name malformed leases as blocking keys in claim batches
Deicyde
committed
de4dc3e
Report articles whose Lean target is deprecated
Deicyde
committed
acf9f19
Add work impact to show what revising shared declarations affects
Deicyde
committed
c644d70
Test impact edge cases and deprecated attributes of earlier declarations
Deicyde
committed
18c31a3
Audit open statements in project CI
Deicyde
committed
36ab265
Document open statements and the revision contract
Deicyde
committed
a2ae587
Keep a retracted theorem open while its lean: names the old declaration
Deicyde
committed
00af085
Claim helper owners in work impact
Deicyde
committed
fef8a4e
Describe assumed open statements without claiming they are sorry
Deicyde
committed
23c7f2c
Hold a definition until its proof prerequisites are stated
Deicyde
committed
2bd6335
Print open statements once in work assumptions
Deicyde
committed
03bf0a4
Test the contract entry for a proof recorded without its statement
Deicyde
committed
66d7cb9
Keep a retracted definition passing on what its body reaches
Deicyde
committed
59414fe
Keep the open probe's helpers out of a namespace
Deicyde
committed
1276277
Log no clean result for a declaration that failed the open audit
Deicyde
committed
a7b8672
Explain recursive auxiliaries in the open audit's sorry error
Deicyde
committed
5abb133
Name the probe in Lean build freshness messages
Deicyde
committed
e9edaf1
Resolve private names, follow aliases, and tighten deprecation in work impact
Deicyde
committed
c582ec0
Refuse imported helper names and quiet lines resting on a failure
Deicyde
committed
c75b7bb
Count a theorem as an alias only when it copies its target's type
Deicyde
committed
59d189e
Document open statements under revision and the impact report's limits
Deicyde
committed
3420208
Run the impact probe's real-Lean test in CI
Deicyde
committed
bae97ab
Read a partial def's body through its _unsafe_rec companion in work impact
Deicyde
committed
5408982
Report a deprecated Lean target under doctor's lean targets check
Deicyde
committed
b2d40ed
Run the open-statement audit and impact probe in their own real-Lean step
Deicyde
committed
5648a8d
Say that a retracted theorem stays open until its proof is recorded
Deicyde
committed
f062776
Keep the conditional-proof render test off the Actions environment
Deicyde
committed
20eb5a4
Merge main into open-statements-revision
Deicyde
committed
94e7772
Mark a retracted statement explicitly instead of inferring it from lean:
Deicyde
committed
466e87e
Give every impacted helper a claim target, keyed by its own name when no article owns it
Deicyde
committed
019ed2e
Document the retraction marker and close the revision contract's gaps
Deicyde
committed
0da3cac
Claim a revised declaration no article names like an unowned helper
Deicyde
committed
cc36d27
Close three gaps in the revision and open-statement docs
Deicyde
committed
433de30
Pin the sorry-free open-statement hint and a mathlib contract entry
Deicyde
committed
88e2da4
Pin the wiki/Lean open-statement contract with a property test
Deicyde
committed
0237cd6