Repository navigation

Census path is not laxer than compile: the probe keyed the wrong class; fix the qualified-Nat spellings that made the census stricter - #12395

Merged

gunbai-bot[bot] merged 11 commits into

mainfrom

session/still-hawk-901

Sep 28, 2026

Commits on Sep 26, 2026
- WIP probe matrix (not for merge)
  gunbc-ci-auto-heal
  committed
  5542414
Commits on Sep 27, 2026
- WIP probe runner returns ProcessExit
  gunbc-ci-auto-heal
  committed
  5eed55a
- v2.std.cardinality spells its imported Nat by the bound name; RFM row + product-inhabitance class witness
  gunbc-ci-auto-heal
  committed
  afcf820
- v2.std.integer spells its imported Nat by the bound name
  gunbc-ci-auto-heal
  committed
  5c4b317
- RFM row: name both repaired modules
  gunbc-ci-auto-heal
  committed
  e832377
- drop scratch probe matrix
  gunbc-ci-auto-heal
  committed
  6e60524
- v2.lens.synthesis imports the AdvisoryLens it names (surfaced when v2.std.integer entered the floor subject)
  gunbc-ci-auto-heal
  committed
  edcd49c
- floor roster: retire the three synthesis.dag unimported-bare-provider rows as ImportsFixed
  gunbc-ci-auto-heal
  committed
  cad2737
- Merge remote-tracking branch 'origin/main' into session/still-hawk-901
  gunbc-ci-auto-heal
  committed
  096695d
- v2.lens.synthesis imports Report and its SynthesisGap reasons from v2.std.report directly (drops the now-unused AdvisoryLens import)
  gunbc-ci-auto-heal
  committed
  82c3975
- v2.lens.synthesis: keep the AdvisoryLens import it uses beside the direct v2.std.report import
  gunbc-ci-auto-heal
  committed
  cfdc7f2