Repository navigation
check-review: a review with no statement is not a review that will survive - #20
Merged
Merged
Conversation
…rvive `reviewed_statement_pp` is nullable in review/1.0, and correctly so -- null is the honest way to record "not captured", and forbidding it would leave a reviewer no way to say it. It is also the value that makes a review SILENTLY un-carryable: restate-check parses that string to elaborate and isDefEq, so with nothing to parse the outcome is not_checkable, and not_checkable carries nothing forward. Nothing looks wrong in the meantime. The entry has a reviewer, a date, a faithfulness verdict, three digests, and it passes mfc validate. It is indistinguishable from a review that will survive until the next dependency bump, when C-10 fails and #136's ~2h/entry comes due. RV-01 is the whole command: every review records the statement it was made against. One rule, because that is what the issue asks for and a second smuggled in beside it would be harder to argue with later. NOT a schema change. `minLength: 1` would forbid recording "not captured" honestly, and it would amend review/1.0, which stopped being free at v0.1.0. The schema describes shape; this describes whether a review is USABLE, and only the second question has a wrong answer. It gates rather than warns. The reason a null slips through is that nothing stops it, and a warning nobody reads stops nothing. #654's `--capture` makes the value cheap and self-verifying, so the rule now asks for something the tooling supplies rather than something a human must remember. Whitespace fails too: " " has the shape of a capture and the substance of a null. An empty reviews[] is NOT_RUN rather than a pass -- a repository with no reviews yet is ordinary, and calling that green is the vacuous pass. 623 passed, 1 skipped; lake build clean. Closes chris-dare-dev/derived-alg-geo-lean#647
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
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.
Closes chris-dare-dev/derived-alg-geo-lean#647.
reviewed_statement_ppis nullable inreview/1.0, and correctly so — null is the honest way to record "not captured", and forbidding it would leave a reviewer no way to say it.It is also the value that makes a review silently un-carryable.
restate-checkparses that string to elaborate andisDefEq; with nothing to parse the outcome isnot_checkable, andnot_checkablecarries nothing forward.Nothing looks wrong in the meantime. The entry has a reviewer, a date, a faithfulness verdict, three digests, and it passes
mfc validate. It is indistinguishable from a review that will survive — until the next dependency bump, when C-10 fails and #136's ~2h/entry comes due.One rule
RV-01: every review records the statement it was made against. That is what the issue asks for; a second rule smuggled in beside it would be harder to argue with later.Not a schema change
minLength: 1would forbid recording "not captured" honestly, and it would amendreview/1.0, which stopped being free atv0.1.0. The schema describes shape; this describes whether a review is usable, and only the second question has a wrong answer.It gates rather than warns
The reason a null slips through is that nothing stops it, and a warning nobody reads stops nothing. #654's
--capturenow makes the value cheap and self-verifying, so the rule asks for something the tooling supplies rather than something a human must remember.Two edges worth the tests
" "has the shape of a capture and the substance of a null.reviews[]isNOT_RUN, not a pass. A repository with no reviews yet is an ordinary state; calling that green is the vacuous pass this contract keeps finding in new places.623 passed, 1 skipped;
lake buildclean.Not in this PR: wiring
mfc check-reviewinto derived-alg-geo-lean's Contract gates. That is a change in the other repo and follows once this is pinned.