Repository navigation
Deploy workflow has never run: install the Rust toolchain before cargo - #8663
gunbai-bot[bot] wants to merge 1 commit into
Conversation
`deploy.yml` invoked `cargo build` on the srv1 self-hosted runner with no toolchain on PATH. Every deploy run since the workflow landed exited 127 with `cargo: command not found` — the actuator has never once succeeded, so no merge has ever reached srv1 through it. The green witnesses said nothing because none of them looked at the step list. `witnesses.yml` already installs the toolchain; the two workflows share one runner and one need, so this is one fact with two consumers, not two facts. `witness_floor_toolchain_step` is renamed `self_hosted_rust_toolchain_step` and imported by both — the step is not a witness-floor fact and its old name asserted otherwise (DESIGN §3). Two claims added, each observed RED against a model with the step removed before being accepted green: the_deploy_workflow_installs_a_toolchain_before_its_first_cargo_invocation the_deploy_toolchain_step_disables_the_shared_home_cache The second anchors on the text after the toolchain step; with no step `split(...).last()` returns the whole document, so it fails for the right reason rather than by accident. Rung: mechanically preventable. The invalid state (a self-hosted job invoking cargo with no toolchain) stays writable — nothing derives the toolchain requirement from the fact that a step runs cargo. Next-rung trigger: a step carrying its tool requirements structurally, so the job projection installs them rather than an author remembering to. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…re cargo fleet-desired.yml runs `cargo build --release -p v1-compiler` on the same srv1 self-hosted runner that deploy.yml has been dying on. It had no toolchain step, so it would have exited 127 exactly as deploy.yml has on all 14 of its runs: the admission job would die before deciding anything and the fleet ref would silently never advance. This PR is the ordering gate that makes the deploy path safe, and it was about to merge a workflow that could not run — reproducing, inside the fix, the defect the fix exists to stay ahead of. The step is imported from witness_floor_workflow rather than copied. It is one fact — what a self-hosted runner needs before cargo — with several consumers (DESIGN §3). It keeps its current name here; #8663 renames it to self_hosted_rust_toolchain_step and updates both consumers, and lands after this. Two claims, each observed RED against a model with the step removed: the_admission_workflow_installs_a_toolchain_before_its_first_cargo_invocation the_admission_toolchain_step_disables_the_shared_home_cache Found by asking what the agreed merge sequence assumed. Its step 5 was "observe its first real floor-completion admission", which is only reachable if the admission job can start — an assumption nothing checked and no review of this diff alone would have questioned. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Closing as obsolete — and it would now be actively harmful to merge
This PR repairs a workflow that no longer exists. Worse, merging it would arm a hazard:
So the correct disposition is to close it, not to refresh it. What was actually right here, kept for the recordThe diagnosis stands and was independently confirmed: the deploy actuator had never once succeeded, 28/28 failures on The real fix is now completing the root cut: removing the registry row and the workflow projection so regeneration stops emitting the file at all. Cutting the emitted leaf while leaving the authority that re-authors it is the leaf-cut failure the replacement-migration doctrine names. — sent from nimble-fox-671 |
…hecking (#8643) * Gate the fleet-desired advance on the floor conclusion it was never checking gunbc.fleet_main_revision requires the fleet's desired revision to derive from merged, FLOOR-GREEN main -- "never from a CLI argument, a session's checkout, or raw HEAD" -- and models the gate as admit_fleet_desired_advance, whose refusal names the prevented class: raw-HEAD simultaneous fleet-bricking. That gate's only caller was its own witness test. The emitted deploy.yml stamped $GITHUB_SHA onto refs/fleet/desired on every push to main, consulting nothing. Specification-without-execution (DESIGN section 5) with the unproven path live. The blast radius is not the ref's name. gunbc.roadmap_belt_actuate gates worker DISPATCH on revision standing, and its own note calls a dispatch from an unadmitted tree "a worker spawned from code the fleet never admitted, reported as an ordinary spawn". A desired ref equal to whatever last landed makes that comparison agree unconditionally, so an existing safety gate passed in silence. WHY THE ADMISSION MOVED OUT OF THE DEPLOY JOB. The required floor takes ~30 minutes, so at push time no conclusion exists for the candidate. A push-triggered advance can only fabricate floor-green or refuse forever. The conclusion becomes observable exactly once -- when the floor run completes -- so the admission is a workflow_run-keyed workflow reading the conclusion GitHub delivers. gunbc.fleet_desired_admission trust-walls the payload on identity the trigger filter also claims (activity, workflow, branch, fork), derives floor_green from the delivered conclusion (only Success), and calls the modeled gate. It renders the authorized push ITSELF, so the surrounding shell carries no ref name, no candidate and no expected prior: a shell that cannot name a revision cannot push an unadmitted one. An unobservable prior REFUSES rather than being read as an absent one. fleet_desired_observe collapses "ls-remote refused" and "ref not advertised" into one state with different causes, and those demand opposite actuations -- treating the first as the second would create the ref from scratch and overwrite an admitted revision nobody could read (the empty-observation narrow). The ungated script is deleted at the root rather than kept beside the replacement, and the two deploy claims that asserted the old behaviour are rewritten -- one was NAMED for a ref this job no longer advances. This is a scope narrowing, not a full climb: the actuation is still shell. git.PublicationTransport PushRefUpdate is shadow-only and models no --force-with-lease, so full construction is not reachable. The DECISION is modeled; the residual debt is declared where the remaining shell lives. EVIDENCE BY EXECUTION, not by green claims alone. Wet, against the real remote, reading the actual admitted prior via ls-remote: git push --force-with-lease=refs/fleet/desired:517fdac4dd... \ origin 5a10ca7e018f...:refs/fleet/desired Six discriminating wet probes, each a distinct located cause, none writing an authorization file: floor conclusion failure -> rc=1, "raw-HEAD simultaneous fleet-bricking" conclusion from "deploy" -> rc=1, wrong workflow branch session/x -> rc=1, not the default branch fork head repository -> rc=1, a fork's run never admits activity "requested" -> rc=1, not completed floor success on main -> rc=0, authorization written Witnesses: 12/12 new, 5/5 rewritten deploy claims, both with the [resolve-summary] footer (complete runs, not partial kills). A DEFECT THE WET PATH CAUGHT AND THE MODEL DID NOT. GitObjectId as String renders the debug form, so the first authorized push read --force-with-lease=refs/fleet/desired:GitSha1ObjectId { digest: ... }. It compiled, typechecked, and would have failed at the remote. Routed through git_object_id_wire_hex. STILL OPEN, and deliberately not decided here: whether DEPLOYMENT should also block on floor-green, or only admission. This gates admission only, so a red floor leaves srv1 deployed while the fleet holds last-known-good and the belt refuses to dispatch -- loud, and the declared anti-entropy behaviour. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a concurrency claim the emitted bytes do not support (review 53998) The admission workflow's annotation claimed "queued, never cancelled ... two floor runs completing close together must admit in order". The chosen variant does not provide that. Per extdeps.languages.yaml.gha_workflow concurrency_queue_max_emission_note, ConcurrencyMappingQueueNotMax is the default group -- at most one running and one PENDING entry, with a newly-arriving entry CANCELLING the pending one. Multi-entry in-order queueing is what ConcurrencyMappingQueueMax was minted for. The claim was a state-space conflation of "in-order queue" with the platform's pending-replacement default. The variant STAYS, with a narrower and true reason. What this workflow needs is that a RUNNING admission is never interrupted -- a cancellation between the compare-and-swap decision and the push would leave the advance half-observed -- and the default group gives exactly that, since cancel-in-progress defaults false and only the pending entry is replaceable. Losing a superseded pending admission is preferable, not a defect: the desired ref should track the newest floor-green revision. QueueMax would buy the in-order queue and then owe an explanation of why the fleet wants to walk through revisions it has already passed. ALSO DECLARED, found while checking the above rather than reported by it: neither variant prevents an OLDER floor run from admitting after a newer one. A manually re-run floor for an earlier commit completes later, observes the current prior, and its CAS succeeds -- moving the desired ref BACKWARD. The gate models floor-greenness, not ancestry. Class sits at mitigatable: it needs a deliberate re-run of an old floor run, and the result is a valid earlier revision rather than an unproven one. NEXT-RUNG TRIGGER: an ancestry operand on the admission, which needs a git ancestry read git.Core does not yet model. Annotation-only: the emitted .github/workflows/fleet-desired.yml is byte-identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retract a false ordering guarantee in the deploy workflow annotation The annotation claimed the fleet-desired admission "cannot run until the required floor has completed, which is strictly after this workflow has finished or failed". There is no such dependency. deploy.yml and witnesses.yml BOTH trigger on push to the default branch and run in parallel; nothing sequences them. The floor takes ~30 minutes against ~10 here, so the admission does land later in practice -- but deploy's concurrency group is a queue, so a deploy waiting behind another deploy can still be running when the floor completes. Typical is not guaranteed. An annotation saying "strictly" about a race is the prose half of the fail-open class this module's own history is made of, and it was load-bearing: it was the justification offered for moving the advance out. WHAT THE ANNOTATION NOW CLAIMS INSTEAD, which is the argument that actually needed making: the lost ordering is acceptable because refs/fleet/desired is a TARGET, not an observation of what is deployed. gunbc.fleet_main_revision defines it as the revision hosts converge TOWARD, and the anti-entropy property is precisely that a host which has not applied it yet keeps serving last-known-good while saying so. A host behind an advanced ref reads RevisionDrifted and refuses dispatch loudly, carrying both revisions. The original ordering argument was defending against a SILENT window; there is none, because the failure it feared is a typed refusal either way. Annotation-only: the emitted .github/workflows/deploy.yml is byte-identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct an understated reachability claim and declare the unmodelled admission judge Two findings from independent review, both verified against the emitted workflows rather than accepted, and both correcting claims this PR itself made. 1. THE BACKWARD ADVANCE IS ORDINARY, NOT AN OPERATOR EDGE CASE. The annotation said reaching it "requires deliberately re-running an old floor run". That was wrong and it made a live race read as a curiosity. The floor's concurrency group is witness-floor-${{ github.event.pull_request.number || github.run_id }}; on a default-branch push there is no PR number, so the group is unique per run and the floor imposes NO ordering between main pushes: floor(C1) starts; floor(C2) starts floor(C2) finishes first -> desired advances D -> C2 floor(C1) finishes later -> observes C2 -> CAS SUCCEEDS -> C2 -> C1, backward --force-with-lease does not prevent this. The lease refuses an UNOBSERVED concurrent write; the older admission observes the newer prior correctly and overwrites it on purpose. Rung is unchanged at mitigatable -- the ref lands on a revision that IS floor-green, and a host behind it refuses dispatch loudly. What changes is reachability: ordinary merge traffic, not operator action. NEXT-RUNG TRIGGER, now stated as blocked on modelling rather than effort: a forward-only operand needs an ancestry read git.Core does not model. RevList cannot express it -- its argv is hardcoded to `{since}..HEAD`, so it answers only HEAD-relative questions, while the discriminating test needs both endpoints named. 2. THE IDENTITY OF THE CODE MAKING THE ADMISSION DECISION IS NOT MODELLED. On a workflow_run event GitHub checks out the DEFAULT BRANCH HEAD, not the triggering run's head_sha, and the checkout step names no ref. So the binary adjudicating candidate C is built from whatever the default branch is when the admission runs. The decision is correct about WHICH revision it admits -- the candidate comes from the event payload, not the checkout -- but the judge's provenance is an accident of timing, and today that default branch can itself be red. The naive repair (check out the event's head_sha) is not automatically safe: workflow_run is privileged and carries write credentials, and the in-model trust wall runs after checkout and compilation, so it cannot protect a step that already executed candidate code. Two honest constructions are named in the annotation; both are larger than this change. Annotation-only: the emitted workflows are byte-identical. Neither gap is introduced here -- the advance this PR replaces was an ungated raw-HEAD stamp on every push, which is strictly worse on both axes -- but shipping them undeclared would be the rung inflation this PR exists to remove. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the two declared gaps as search keys, and record why they are not typed rows The two residual classes were declared in prose with no stable identifier, so a future migration would have to find them by memory. They now carry greppable keys: FleetDesiredAdvanceForwardOnly the backward-advance race FleetDesiredAdmissionJudgeIdentity the timing-dependent judge provenance WHY THEY ARE NOT TYPED CARRIERS, recorded beside them because section 4c says a machine-consumed fact belongs in one and these are not: The intended owner exists as a PLAN and not as a MODULE. gunbc.roadmap_authority specifies GuaranteeRequirement (class identity, domain, harm, ceiling with typed reason, next_rung_trigger) with GuaranteePath and GuaranteeMeasurement beside it and the disposition DERIVED rather than stored, as Stage 1b. Grepping the tree finds that vocabulary only in that roadmap prose; no module declares it. So the only way to give these typed owners today is a bespoke registry in this module, refused on three of this repository's own grounds: it would be a second authority for facts Stage 1b exists to own (section 3); its whole future is migration-then-deletion, failing section 6's survival test; and section 6 forbids a scaffold authorized by its own author. A private registry would make this module look more modeled while trading visible incompleteness for false completion. The annotation is untyped debt that is honest about being debt. When the real carrier lands these two classes move straight into GuaranteeRequirement rows with no interim registry to dissolve first. Annotation-only: the emitted .github/workflows/fleet-desired.yml is byte-identical, verified by re-running the emitter. The block attaches to expected_fleet_desired_yml rather than sitting at end-of-file -- a section 4c annotation needs a following declaration, and an earlier revision of this PR reddened the floor by forgetting that. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The admission workflow builds on srv1 too: install the toolchain before cargo fleet-desired.yml runs `cargo build --release -p v1-compiler` on the same srv1 self-hosted runner that deploy.yml has been dying on. It had no toolchain step, so it would have exited 127 exactly as deploy.yml has on all 14 of its runs: the admission job would die before deciding anything and the fleet ref would silently never advance. This PR is the ordering gate that makes the deploy path safe, and it was about to merge a workflow that could not run — reproducing, inside the fix, the defect the fix exists to stay ahead of. The step is imported from witness_floor_workflow rather than copied. It is one fact — what a self-hosted runner needs before cargo — with several consumers (DESIGN §3). It keeps its current name here; #8663 renames it to self_hosted_rust_toolchain_step and updates both consumers, and lands after this. Two claims, each observed RED against a model with the step removed: the_admission_workflow_installs_a_toolchain_before_its_first_cargo_invocation the_admission_toolchain_step_disables_the_shared_home_cache Found by asking what the agreed merge sequence assumed. Its step 5 was "observe its first real floor-completion admission", which is only reachable if the admission job can start — an assumption nothing checked and no review of this diff alone would have questioned. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rename the two toolchain claims to what they actually establish Their names asserted more than the predicate proves. They are textual projection sentinels over emitted yaml, not proofs that a Cargo consumer is dominated by a Cargo provider: the_admission_workflow_installs_a_toolchain_before_its_first_cargo_invocation -> the_emitted_admission_yaml_places_a_setup_action_before_its_literal_cargo_build the_admission_toolchain_step_disables_the_shared_home_cache -> the_emitted_admission_yaml_disables_the_shared_home_cache_on_its_setup_action The predicate splits on the literal "cargo build", which has two unequal failure modes. A changed spelling — for example `"$CARGO_BIN" build`, which is exactly how fleet-converge.yml already invokes cargo — makes the first conjunct false and the claim RED: a false alarm, but fail-closed. A second non-literal invocation placed BEFORE the provider, with a later literal one still present, makes `.first()` span both and the claim PASSES: a false green, fail-open. Adding "$CARGO_BIN" to the match would enlarge the recognised spellings and move the hole one substitution along. A text search over emitted bytes cannot see what a step executes; that is the ceiling, not a gap in effort. §4b rung declared in the annotation: mitigatable, with the next-rung trigger named — workflow capability closure, a typed step operation deriving CargoCapability (that derivation already exists for validations in gunbc.roadmap_execution_contract) plus a projection that refuses to emit a job whose derived capabilities are unclosed. The structural control is then invariant under every spelling because it inspects none of them, and these two claims are deleted or demoted to a byte fixture rather than kept beside it as though both were safety mechanisms. The claims still execute and still hold; only the names and the recorded rung change. 13/13 pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the scaffold obligation for the shell push actuation The replacement advance renders a script and executes it through `sh`, and the annotations said so — but neither module carried a `Disposition = Scaffold` or a `DissolutionCondition`, while the surviving ci_spec annotation claimed the debt was "re-declared where the remaining shell actually lives". It was explained there and not actually re-declared. One obligation covers the renderer and its executor: they are one independently removable unit, the renderer exists solely to feed the executor, both dissolve into the same typed git CAS realization, and neither has a useful life without the other. This authorizes nothing. `std.disposition.Scaffold` records the construction and its dissolution binding and says nothing about permission; the operator verdict is an external fact bound to the current head. Leaving the debt unmarked was not the conservative choice — under the doctrine it is marked debt's violation plus concealment, and declaring the population is what makes the verdict decidable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
What is broken
deploy.ymlrunscargo buildon the srv1 self-hosted runner. Nothing installs a toolchain first, so the step exits 127 withcargo: command not found.Tally over the workflow's entire history: 14 runs, 14 failures, zero successes ever. Independently verified by swift-badger-524; run
32333231306carries the log line.This is not a repaired regression — read it as one, and every other sentence here misleads
There is no working state to restore. The modeled deploy actuator has never once actuated. This PR makes the modeled path executable for the first time; it does not bring back a known-good prior behaviour, because there was none. The first successful run will be the first successful run.
The larger finding, which is the part worth carrying: if nothing has ever reached srv1 through the modeled path, then whatever is running on that box got there some other way — a hand-run command, a manual copy, an out-of-band script. That is DESIGN §6's out-of-band-actuation tell in its purest form: manual application, with a modeled path beside it that has never executed. The workflow was not a broken actuator, it was a decorative one, and the real actuation has been invisible and unmodeled the whole time.
Named as an open unknown rather than answered here: nobody currently knows what is running on srv1 or how it was placed there. I did not reverse-engineer the box, and the repo carries no hand-authored deploy script that would explain it. The modeled path is supposed to replace that mechanism, and we cannot yet say what it is replacing.
The change
witnesses.ymlalready installs the toolchain, on the same runner, for the same reason. That is one fact with two consumers.witness_floor_toolchain_stepis renamedself_hosted_rust_toolchain_stepand imported by both — the old name asserted the step was a witness-floor fact when it is a self-hosted-runner fact (DESIGN §3).Emitted
deploy.ymlnow carriesactions-rust-lang/setup-rust-toolchain@v1.16.0withcache: falseahead of the build step.Evidence
Two claims, each observed RED before being accepted green:
..._installs_a_toolchain_before_its_first_cargo_invocation..._disables_the_shared_home_cacheThe second anchors on the text after the toolchain step; with no step,
split(…, "setup-rust-toolchain").last()returns the whole document, so it fails for the right reason rather than by coincidence. A control never observed failing is indistinguishable from a comment.Why nothing caught this
The deploy witnesses assert the job's grants and provider wiring, and never its step list. The model was checked for the properties someone thought to model; the one property deciding whether the job runs at all was outside them. Honest about what it examined, silent on the axis that mattered.
Rung
Mechanically preventable, honestly. The invalid state — a self-hosted job invoking
cargowith no toolchain — stays writable; nothing derives the requirement from the fact that a step runs cargo, and the next workflow to do it reproduces this defect. Next-rung trigger: a step carrying its tool requirements structurally, so the job projection installs them instead of an author remembering to.What this does not establish
That a deploy now succeeds end-to-end. There is no successful run in history to compare against, so the first real run is the measurement — I will report its outcome, not forecast it. If it fails for a second reason, that is the next layer of a path nobody has ever exercised, not a setback.