chore: make main sorry-free — release policy - #113
Merged
Conversation
Remove the 3-sorry Hopf–Rinow statement stub (HopfRinow.lean) and its root import; keep the proven bridge lemma (EVariationLePathELength). Turn the CI sorry check into a hard gate (0, not 3): main is a release-quality branch and carries no sorry. The Hopf–Rinow theorem returns to main once its proof is complete on the development branch.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Principle:
mainis a release-quality branch and must carry nosorry. Work-in-progress withsorrylives on a development branch and merges tomainonly once the proof is complete.Problem:
maincurrently has 3sorrys — all in the Hopf–Rinow statement stubGeodesic/HopfRinow.lean— and CI baked this in (EXPECTED=3).This PR:
OpenGALib/Riemannian/Geodesic/HopfRinow.lean(the stub) and its root import;HopfRinow/EVariationLePathELength.lean(0 sorry);mainmust be sorry-free (0, not 3).Effect:
mainis now the sorry-free supporting cone; the Hopf–Rinow theorem returns tomainwhen its proof lands (adoption finale).lake buildgreen, sorry count 0.