Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ jobs:
id: build_witness_fold
run: |
cargo build --release -p v1-compiler --bins
cargo build --release -p v1-stage0-runtime -p v1-stage0-std-core -p v1-stage0-std-surface -p v1-stage0-extdeps-languages -p v1-stage0-v1-artifact -p v1-stage0-v1-infer -p v1-stage0-emit-core
- name: Record the toolchain environment
run: |
echo "host=$(hostname) runner=${RUNNER_NAME:-unset}"
Expand Down
44 changes: 44 additions & 0 deletions dag/gunbc/repo/repo_self_build.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module gunbc.repo_self_build

import std.types { String, List, NonEmptyStr }
import gunbc.stage0_crate_partition_generated { generated_partition_crate_rows }

// THE SINGLE POINT THROUGH WHICH THIS REPOSITORY BUILDS ITS OWN BINARIES.
// Before this module the same operation was spelled independently in three
Expand Down Expand Up @@ -80,6 +81,49 @@ fn repo_self_test_command() -> String {
)
}

// THE DERIVED STAGE0 PARTITION CRATES, WHICH THE PACKAGE-AS-DATA DECISION ABOVE DOES NOT REACH.
// repo_self_build_package is one package because that was the whole repository's compiler for as
// long as this module existed. The stage0 partition splits that compiler across seven SIBLING
// packages, and none of them is v1-compiler, so every command above builds none of them --
// which is exactly how #9689 put main's whole-workspace build in a state no required run could
// see. Three modules landed in stage0 lib.rs and in the partition authority's blind spot at once,
// and v1-stage0-v1-infer failed with E0432 on all three for a day while the required gate,
// building the two v1-compiler bins, stayed green.
//
// THE PACKAGE LIST IS READ FROM THE PARTITION ROSTER AND IS NOT RESTATED HERE, for the same
// reason repo_self_build_all_bins_command asks cargo for the bin roster rather than enumerating
// it: a caller free to enumerate the packages could omit the one that is drifting and still look
// like a conforming call. Adding a crate to the partition adds it to this command with no edit
// here, so the gate cannot fall behind the authority it is guarding.
//
// WHAT THIS BUYS, STATED AS THE REFUSAL IT PRODUCES RATHER THAN AS COVERAGE. rustc is the oracle
// for "every crate:: reference in a rostered module resolves inside its crate's reexport
// closure". A module dropped from a roster reds with E0432 naming the module and the referrer; a
// roster entry naming no file reds with E0583 naming the entry. That class has no hermetic
// witness available: gunbc.stage0_rust_product_reachability declares the Rust module dependency
// graph unmodeled in rust_module_dependency_graph_unresolved_edge, and a joining witness that
// read the tree instead would declare ReadsLiveTree and be declined by the required floor. So
// this build IS the wall, and the modeled dependency graph is the trigger for climbing off it.
//
// NOT A WHOLE-WORKSPACE WIDENING, and deliberately not: this names the partition packages, so a
// declared bin or crate outside both this list and the v1-compiler package remains unbuilt by any
// required phase. That gap is the 2026-08-25 declared row and this command does not close it.
fn repo_self_build_partition_crate_packages() -> List<String> {
generated_partition_crate_rows |> map(row => row.package_name)
}

fn repo_self_build_packages_command(packages: List<String>) -> String {
join(
["cargo build", repo_self_build_profile_flag]
|> concat(packages |> map(p => join(["-p", p], " "))),
" "
)
}

fn repo_self_build_partition_crates_command() -> String {
repo_self_build_packages_command(packages: repo_self_build_partition_crate_packages())
}

fn repo_self_build_command(bins: List<String>) -> String {
if bins |> count == 0 {
repo_self_build_package_command()
Expand Down
4 changes: 3 additions & 1 deletion dag/gunbc/stage0/stage0_crate_partition_generated.dag
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
"std_measure",
"std_types",
"std_unicode_types",
"std_lens_verdict",
"std_algebra",
"std_nat",
"std_node",
Expand All @@ -71,6 +70,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
"extdeps_units_iso_80000_3",
"std_occurrence_identity",
"std_source_annotation",
"std_target_representation",
"v1_std_core"
],
reexport_packages: [
Expand Down Expand Up @@ -114,6 +114,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
"extdeps_languages_python_types",
"extdeps_languages_rust_capabilities",
"extdeps_languages_rust_emit",
"extdeps_languages_rust_representation",
"extdeps_languages_rust_syntax",
"extdeps_languages_rust_types"
],
Expand Down Expand Up @@ -145,6 +146,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
crate_dir: "src/v1/stage0_v1_infer",
kind: GeneratedLayeredCoreCrate,
modules: [
"gunbc_rust_source_type_bindings",
"v1_compiler_coercion",
"v1_compiler_infer_emit_info",
"v1_compiler_infer_env",
Expand Down
21 changes: 19 additions & 2 deletions dag/gunbc/witness/witness_floor_workflow.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import extdeps.languages.yaml.types { yaml_string, yaml_int, yaml_bool, kv, Yaml
import gunbc.roadmap_execution_contract {
CargoCapability, RustcCapability, RustfmtCapability, RustupCapability,
}
import gunbc.repo_self_build { repo_self_build_command, repo_self_build_all_bins_command, repo_self_test_command }
import gunbc.repo_self_build { repo_self_build_command, repo_self_build_all_bins_command, repo_self_build_partition_crates_command, repo_self_test_command }
import gunbc.workflow_capability_closure {
CapabilityAnnotatedStep,
StepCapabilityRole,
Expand Down Expand Up @@ -373,8 +373,25 @@ fn witness_floor_build_script() -> String {
repo_self_build_command(bins: witness_floor_required_bins)
}

// TWO INVOCATIONS, BECAUSE THEY BUILD DISJOINT PACKAGE SETS AND NEITHER SUBSUMES THE OTHER.
// The first is every declared bin target of the v1-compiler package. The second is the seven
// sibling packages of the derived stage0 partition, whose roster gunbc.repo_self_build reads
// from the partition authority itself. Before this pair the build lane covered only the first,
// which is how #9689 left main's whole-workspace build red on E0432 in v1-stage0-v1-infer while
// every required context stayed green -- the partition crates are the ONLY consumers that
// compile a stage0 module through a per-crate reexport closure, so a roster short of a module is
// invisible to the monolith and fatal to them.
//
// THE SECOND COMMAND IS THE EXECUTING FORM OF A WALL THAT HAS NO HERMETIC WITNESS. Its refusal
// is rustc's: a module missing from a roster reds E0432 naming the module and the referring
// module, a roster entry naming no file reds E0583 naming the entry. gunbc.repo_self_build
// carries why a joining witness is not available instead, and names the modeled Rust module
// dependency graph as the trigger for climbing off the compiler as oracle.
fn build_lane_build_script() -> String {
repo_self_build_all_bins_command()
join(
[repo_self_build_all_bins_command(), repo_self_build_partition_crates_command()],
"\n"
)
}

fn witness_floor_build_step(build_script: String) -> Step {
Expand Down
6 changes: 3 additions & 3 deletions src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ pub fn generated_partition_crate_rows() -> Rc<Vec<Rc<GeneratedPartitionCrateRow>
package_name: "v1-stage0-std-core".to_string(),
crate_dir: "src/v1/stage0_std_core".to_string(),
kind: GeneratedPartitionCrateKind::GeneratedLayeredCoreCrate,
modules: Rc::new(vec!["std_content_hash".to_string(), "std_coercion".to_string(), "extdeps_currency_currency".to_string(), "std_decl_ref".to_string(), "std_keyed_row".to_string(), "std_keyed_roster".to_string(), "std_roster_frontier".to_string(), "std_dissolution".to_string(), "std_disposition".to_string(), "std_error_primitives".to_string(), "std_emit_model".to_string(), "std_magnitude".to_string(), "std_measure".to_string(), "std_types".to_string(), "std_unicode_types".to_string(), "std_lens_verdict".to_string(), "std_algebra".to_string(), "std_nat".to_string(), "std_node".to_string(), "std_syntax".to_string(), "std_computation".to_string(), "std_termination".to_string(), "std_checked_arithmetic".to_string(), "std_induction".to_string(), "std_graph".to_string(), "extdeps_uri".to_string(), "extdeps_external_authority".to_string(), "std_process_termination".to_string(), "extdeps_container_oci_digest".to_string(), "extdeps_units_dimensionless".to_string(), "extdeps_units_iec_80000_13".to_string(), "extdeps_units_iso8601".to_string(), "extdeps_units_iso_80000_3".to_string(), "std_occurrence_identity".to_string(), "std_source_annotation".to_string(), "v1_std_core".to_string()]),
modules: Rc::new(vec!["std_content_hash".to_string(), "std_coercion".to_string(), "extdeps_currency_currency".to_string(), "std_decl_ref".to_string(), "std_keyed_row".to_string(), "std_keyed_roster".to_string(), "std_roster_frontier".to_string(), "std_dissolution".to_string(), "std_disposition".to_string(), "std_error_primitives".to_string(), "std_emit_model".to_string(), "std_magnitude".to_string(), "std_measure".to_string(), "std_types".to_string(), "std_unicode_types".to_string(), "std_algebra".to_string(), "std_nat".to_string(), "std_node".to_string(), "std_syntax".to_string(), "std_computation".to_string(), "std_termination".to_string(), "std_checked_arithmetic".to_string(), "std_induction".to_string(), "std_graph".to_string(), "extdeps_uri".to_string(), "extdeps_external_authority".to_string(), "std_process_termination".to_string(), "extdeps_container_oci_digest".to_string(), "extdeps_units_dimensionless".to_string(), "extdeps_units_iec_80000_13".to_string(), "extdeps_units_iso8601".to_string(), "extdeps_units_iso_80000_3".to_string(), "std_occurrence_identity".to_string(), "std_source_annotation".to_string(), "std_target_representation".to_string(), "v1_std_core".to_string()]),
reexport_packages: Rc::new(vec!["v1-stage0-runtime".to_string()]),
carries_non_empty_wrappers: false,
}), Rc::new(GeneratedPartitionCrateRow {
Expand All @@ -68,7 +68,7 @@ pub fn generated_partition_crate_rows() -> Rc<Vec<Rc<GeneratedPartitionCrateRow>
package_name: "v1-stage0-extdeps-languages".to_string(),
crate_dir: "src/v1/stage0_extdeps_languages".to_string(),
kind: GeneratedPartitionCrateKind::GeneratedLayeredCoreCrate,
modules: Rc::new(vec!["extdeps_languages_dag_emit".to_string(), "extdeps_languages_dag_syntax".to_string(), "extdeps_languages_dag_types".to_string(), "extdeps_languages_go_emit".to_string(), "extdeps_languages_go_syntax".to_string(), "extdeps_languages_go_types".to_string(), "extdeps_languages_python_emit".to_string(), "extdeps_languages_python_syntax".to_string(), "extdeps_languages_python_types".to_string(), "extdeps_languages_rust_capabilities".to_string(), "extdeps_languages_rust_emit".to_string(), "extdeps_languages_rust_syntax".to_string(), "extdeps_languages_rust_types".to_string()]),
modules: Rc::new(vec!["extdeps_languages_dag_emit".to_string(), "extdeps_languages_dag_syntax".to_string(), "extdeps_languages_dag_types".to_string(), "extdeps_languages_go_emit".to_string(), "extdeps_languages_go_syntax".to_string(), "extdeps_languages_go_types".to_string(), "extdeps_languages_python_emit".to_string(), "extdeps_languages_python_syntax".to_string(), "extdeps_languages_python_types".to_string(), "extdeps_languages_rust_capabilities".to_string(), "extdeps_languages_rust_emit".to_string(), "extdeps_languages_rust_representation".to_string(), "extdeps_languages_rust_syntax".to_string(), "extdeps_languages_rust_types".to_string()]),
reexport_packages: Rc::new(vec!["v1-stage0-runtime".to_string(), "v1-stage0-std-core".to_string(), "v1-stage0-std-surface".to_string()]),
carries_non_empty_wrappers: false,
}), Rc::new(GeneratedPartitionCrateRow {
Expand All @@ -82,7 +82,7 @@ pub fn generated_partition_crate_rows() -> Rc<Vec<Rc<GeneratedPartitionCrateRow>
package_name: "v1-stage0-v1-infer".to_string(),
crate_dir: "src/v1/stage0_v1_infer".to_string(),
kind: GeneratedPartitionCrateKind::GeneratedLayeredCoreCrate,
modules: Rc::new(vec!["v1_compiler_coercion".to_string(), "v1_compiler_infer_emit_info".to_string(), "v1_compiler_infer_env".to_string(), "v1_compiler_infer_items".to_string(), "v1_compiler_infer_occurrence_binding".to_string(), "v1_compiler_infer_service".to_string(), "v1_compiler_infer_sigs".to_string(), "v1_compiler_infer_types".to_string(), "v1_compiler_type_head_exposure".to_string()]),
modules: Rc::new(vec!["gunbc_rust_source_type_bindings".to_string(), "v1_compiler_coercion".to_string(), "v1_compiler_infer_emit_info".to_string(), "v1_compiler_infer_env".to_string(), "v1_compiler_infer_items".to_string(), "v1_compiler_infer_occurrence_binding".to_string(), "v1_compiler_infer_service".to_string(), "v1_compiler_infer_sigs".to_string(), "v1_compiler_infer_types".to_string(), "v1_compiler_type_head_exposure".to_string()]),
reexport_packages: Rc::new(vec!["v1-stage0-runtime".to_string(), "v1-stage0-std-core".to_string(), "v1-stage0-std-surface".to_string(), "v1-stage0-extdeps-languages".to_string(), "v1-stage0-v1-artifact".to_string()]),
carries_non_empty_wrappers: false,
}), Rc::new(GeneratedPartitionCrateRow {
Expand Down
3 changes: 3 additions & 0 deletions src/v1/stage0_extdeps_languages/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,9 @@ pub mod extdeps_languages_rust_capabilities;
#[path = "../../stage0/src/extdeps_languages_rust_emit.rs"]
pub mod extdeps_languages_rust_emit;
#[rustfmt::skip]
#[path = "../../stage0/src/extdeps_languages_rust_representation.rs"]
pub mod extdeps_languages_rust_representation;
#[rustfmt::skip]
#[path = "../../stage0/src/extdeps_languages_rust_syntax.rs"]
pub mod extdeps_languages_rust_syntax;
#[rustfmt::skip]
Expand Down
6 changes: 3 additions & 3 deletions src/v1/stage0_std_core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,9 +66,6 @@ pub mod std_types;
#[path = "../../stage0/src/std_unicode_types.rs"]
pub mod std_unicode_types;
#[rustfmt::skip]
#[path = "../../stage0/src/std_lens_verdict.rs"]
pub mod std_lens_verdict;
#[rustfmt::skip]
#[path = "../../stage0/src/std_algebra.rs"]
pub mod std_algebra;
#[rustfmt::skip]
Expand Down Expand Up @@ -126,5 +123,8 @@ pub mod std_occurrence_identity;
#[path = "../../stage0/src/std_source_annotation.rs"]
pub mod std_source_annotation;
#[rustfmt::skip]
#[path = "../../stage0/src/std_target_representation.rs"]
pub mod std_target_representation;
#[rustfmt::skip]
#[path = "../../stage0/src/v1_std_core.rs"]
pub mod v1_std_core;
3 changes: 3 additions & 0 deletions src/v1/stage0_v1_infer/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,9 @@ pub use v1_stage0_std_core::*;
pub use v1_stage0_std_surface::*;
pub use v1_stage0_v1_artifact::*;

#[rustfmt::skip]
#[path = "../../stage0/src/gunbc_rust_source_type_bindings.rs"]
pub mod gunbc_rust_source_type_bindings;
#[rustfmt::skip]
#[path = "../../stage0/src/v1_compiler_coercion.rs"]
pub mod v1_compiler_coercion;
Expand Down
32 changes: 30 additions & 2 deletions src/v2/test/claim/rust_crate_partition_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ import v2.workflow.rust_crate_partition {
stage0_module_dag,
stage0_module_dag_interface_grounding_is_debt,
stage0_module_bearing_unit_count,
stage0_module_id,
stage0_v1_infer_modules,
stage0_partition_fold_ok,
stage0_partition_member_coverage_consistent,
Stage0PartitionReceiptFoldRefused,
Expand Down Expand Up @@ -216,12 +218,38 @@ test fn witness_runtime_unit_members_holds() -> Bool {
}
}

// THIS WAS `== 9` AND THE 9 WAS THE WHOLE ASSERTION, which is why it is not `== 10` now.
// #9689 added three modules to stage0 and the v1-infer roster gained one of them
// (gunbc_rust_source_type_bindings), so the literal went stale the moment the roster it
// measures changed -- and the only available repair for a literal is to retype it, which
// DESIGN section 5 names exactly: if automating the update collapses the assertion to
// measure() == measure(), the manual update was the test's entire content.
//
// The join below is not that collapse, and the reason is which side each half comes from.
// stage0_v1_infer_modules() is the DECLARED roster, a list in the partition authority.
// unit.members is what came back through stage0_assign_modules_to_unit and then through
// partition_fold_outcome -- the assignment map keyed by ModuleId, folded and grouped. So
// this asserts the fold routed exactly the declared modules to this unit and invented,
// dropped and misfiled none, which is a property of the plumbing rather than of the list.
// It is honest about its blind spot: an error in the ROSTER ITSELF is invisible here, as it
// was to the count, because both sides then move together. That class is the required build
// lane's (gunbc.repo_self_build repo_self_build_partition_crates_command), where rustc is
// the oracle.
//
// The sibling unit witnesses still carry count literals with the same defect. They are left
// alone deliberately: this one is converted because this change broke it, and converting the
// rest is a separate diff rather than a rider on an unbreak.
test fn witness_v1_infer_unit_members_holds() -> Bool {
match stage0_partition_receipt_outcome() {
Stage0PartitionReceiptOk { units: units } =>
match partition_unit_by_id(units: units, unit_id: stage0_unit_v1_infer) {
Present { value: unit } =>
(unit.members |> count) == 9
Present { value: unit } => {
let declared = stage0_v1_infer_modules()
|> map(basename => stage0_module_id(basename: basename))
(unit.members |> count) == (declared |> count)
&& declared |> all(d => unit.members |> any(m => m == d))
&& unit.members |> all(m => declared |> any(d => d == m))
}
Absent => false
}
Stage0PartitionReceiptResolveRefused { cause: _ } => false
Expand Down
Loading
Loading