Repository navigation
ci: admit the typed Eigen3_DIR flag in the release step contract - #795
Conversation
The release prebuilt configure passes -DEigen3_DIR=/usr/share/eigen3/cmake and then requires the cache line Eigen3_DIR:PATH=/usr/share/eigen3/cmake. Without a type CMake caches the entry as Eigen3_DIR:UNINITIALIZED, so the check fails after every successful configure. The fix is the typed flag, but the PR admission rules judge a pull request's workflows with main's contract, which names the untyped flag exactly. Read -DEigen3_DIR:PATH=/usr/share/eigen3/cmake as the reviewed untyped flag wherever the release prebuilt steps are compared, so both forms are admitted. release.yml is unchanged here; the switch to the typed flag, and the contract's return to a single form, follow in their own change. Any other Eigen3_DIR value is still refused. Co-Authored-By: Claude Opus 5.5 <[email protected]>
![graphify-labs[bot]](https://avatars.githubusercontent.com/in/4356270?s=60&v=4){kind=small}
There was a problem hiding this comment.
Graphify reviewed this change.
No issues found by static checks — no coupling regressions or blocking issues in the code graph. That is not the same as safe to merge: see what was not checked.
Not checked: tests were not run; formal verification proved 0 of 2 changed function(s) (1 sampled, not proven, 1 not verified).
Formal verification. PR-changed functions: 1/2 verified (0 proven, 1 may-equivalent, 0 distinguished) · 1 not verified (1 vacuous).
Not verified on this run: \_release\_split\_job\_findings (vacuous: never exercised).
Graphify review — findings
Adds support in the release workflow preflight for the typed -DEigen3_DIR:PATH=/usr/share/eigen3/cmake flag alongside the current untyped one. Without the type, CMake caches Eigen3_DIR as UNINITIALIZED, so the reviewed grep -Fx 'Eigen3_DIR:PATH=...' never matches. The new _eigen_dir_accept_typed helper normalizes the typed flag back to the untyped form before the split-layout job checks and release_prebuilt_workflow_findings run, so both layouts accept either spelling. Any other value, such as a different path, still produces findings. The docstring says both forms are admitted only until the workflow switches, after which the contract keeps just the typed form. A new test swaps in the typed flag for both the split and legacy layouts. It checks that the prebuilt, runner and main-admission checks stay clean, and that an out-of-tree path is still refused.
No blocking issues surfaced.
Analysis details — impact, health, verification
Impact & health
Graphify review
Impact — 1049 functions depend on the 952 functions this change touches.
Health — this change adds coupling hotspots:
- worse:
release_prebuilt_workflow_findings()— 8 callers, 11 callees - worse:
main_admission_data_findings()— 7 callers, 3 callees - worse:
_release_split_job_findings()— 2 callers, 7 callees
Verification — 1049 functions in the blast radius were not formally verified this run (proofs are advisory here).
Gate & verification
graphify gate
PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.
Advisory (not blocking):
- verification_scope: 1016 function(s) in the blast radius were not formally verified this run
Test selection
Test selection
5 of 1400 test file(s) selected (0%) via static blast radius.
scripts/test_check_doc_reverts.py— impactscripts/test_ci_corpus_variant.py— impactscripts/test_ci_preflight.py— impact, changed-testscripts/test_ci_release_gate.py— impactscripts/test_cr150_source_gate.py— impact
Selection is safe under the controlled-regression assumption; always-run tests + a periodic full run are the backstops. Advisory — it never changes the check verdict.
Formal verification
Could not verify: Could not verify \_release\_split\_job\_findings.
The verifier did not have enough to check \_release\_split\_job\_findings, so it is saying so rather than guessing. No false assurance is the whole point.
Guarantee: No guarantee either way, this is an honest abstention, not a pass.
Note: Reason: not verifiable: all 63 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly KeyError — names the real obstacle, not a sampling gap)
No difference found (not proven): No behavior difference found in release\_prebuilt\_workflow\_findings (not a proof).
The verifier ran both versions of release\_prebuilt\_workflow\_findings on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.
Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.
Note: An input the sampler did not try could still differ.
· 2 grounded finding(s) anchored inline below; 1 more finding(s) on lines outside this diff (see the check run).
| return text.replace(EIGEN_DIR_TYPED, EIGEN_DIR_UNTYPED) | ||
|
|
||
|
|
||
| def _release_split_job_findings(job: str, body: str) -> list[str]: |
There was a problem hiding this comment.
_release_split_job_findings()
fans out to 7 callees (efferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
| @@ -4857,6 +4873,7 @@ def _release_split_workflow_findings(workflow: str) -> list[str]: | |||
|
|
|||
| def release_prebuilt_workflow_findings(workflow: str) -> list[str]: | |||
There was a problem hiding this comment.
release_prebuilt_workflow_findings()
fans out to 11 callees (efferent coupling); 8 callers depend on it (afferent coupling).
Grounded coupling-delta finding (deterministic), not an LLM guess.
Summary
The release prebuilt configure passes
-DEigen3_DIR=/usr/share/eigen3/cmakeand then requires the cache lineEigen3_DIR:PATH=/usr/share/eigen3/cmake. Without a type, CMake caches the entry asEigen3_DIR:UNINITIALIZED=..., so the check fails after every successful configure (the 1.11.0 release dry run stopped there in both prebuilt jobs).The fix is the typed flag. The PR admission rules judge a pull request's workflows with main's contract, which names the untyped flag exactly, so the contract has to admit the typed form first.
Changes
scripts/ci_preflight.py:-DEigen3_DIR:PATH=/usr/share/eigen3/cmakeis read as the reviewed untyped flag wherever the release prebuilt steps are compared, so both forms are admitted. Any otherEigen3_DIRvalue is still refused.scripts/test_ci_preflight.py: the typed flag is admitted in the split and legacy layouts by the prebuilt, runner and admission checks; a moved directory is still refused.release.ymlis unchanged here. The switch to the typed flag, and the contract's return to a single form, follow in their own change.🤖 Generated with Claude Code