Skip to content

Commit 872041c

Browse files
chore: purge nix per estate-wide deprecation directive 2026-06-01 (#189)
## Summary Owner directive 2026-06-01: "nix is now entirely deprecated and we use guix for everything." This PR completes that estate-wide hardening for echidna opportunistically. No `flake.nix`/`flake.lock` files were present in this repo (the earlier 2026-05-18 ruling already removed them), but stale doc, dependabot, workflow, and manifest references remained. ### Dependabot - `.github/dependabot.yml` + `echidna-playground/.github/dependabot.yml`: removed `package-ecosystem: nix` entries ### Workflows - `.github/workflows/live-provers.yml`: removed `Nix flake (fallback)` header line; documented deprecation in its place ### Manifest - `manifests/live-provers.scm`: hardened policy preamble + reworded the Lean 4 install hint to point at the Wave-3 sealed container instead of `flake.nix or upstream installer` ### Docs (root + echidna-playground subtree) Reworded every "Guix primary, Nix fallback" / "flake.nix mirror" / "Tier-2 ... Nix" mention to record the 2026-06-01 hardening (nix entirely removed; do NOT add flake.nix/flake.lock back). Files touched: - `.claude/CLAUDE.md`, `RSR_COMPLIANCE.adoc` - `docs/handover/STATE.md`, `docs/handover/PRODUCTION-WIRING-PLAN.md`, `docs/handover/L3-LIVE-PROVER-CI-PROMPT.md`, `docs/handover/TODO.md`, `docs/handover/llm-warmup-dev.md` - `docs/wiki/Home.md`, `docs/wiki/Getting-Started.md` - `echidna-playground/RSR_OUTLINE.adoc`, `echidna-playground/.claude/CLAUDE.md` ### Out of scope (intentionally not touched) - Historical session-log entries (`PRODUCTION-WIRING-PLAN.md:171` "2026-04-19 — Kickoff ... Nix fallback ...") - `NIX_ONLY` availability labels in `manifests/live-provers.scm` — they mean "absent from Guix upstream", not "provisioned via Nix"; the policy preamble now spells that out - `.github/workflows/governance.yml:6` historical wrapper-replaced-workflows comment listing `guix-nix-policy.yml` - False positives (`Unix-domain socket`, `UNIX_EPOCH`, `apt mirror flake red-checks`) `.guix-channel` + `guix.scm` already present at the repo root, so no follow-up issue needed. ### Overlap with open PRs The only file overlap with currently-open PRs is `docs/wiki/Home.md` — PR #182 touches the file but leaves the specific line I edit unchanged, so the diffs auto-merge regardless of landing order. ## Test plan - [x] `grep -rln -i 'nix\|flake'` returns only deprecation-policy language, historical session-log entries, the unrelated false positives listed above, and the wrapper-replaced workflow-name comments - [x] GPG-signed with `4A03639C1EB1F86C7F0C97A91835A14A2867091E` - [ ] Auto-merge `--auto --squash --delete-branch` (set on this PR) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 68ef34a commit 872041c

15 files changed

Lines changed: 43 additions & 44 deletions

File tree

.claude/CLAUDE.md

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -134,13 +134,13 @@ package definitions (not metadata files) and must NOT be deleted.
134134

135135
### Package Management
136136

137-
- **Primary**: Guix (`guix.scm`, `manifests/*.scm`)
137+
- **Sole primary**: Guix (`guix.scm`, `manifests/*.scm`)
138138
- **Escape hatch**: a sealed container (`.containerization/Containerfile.wave3`)
139-
for the not-in-Guix / non-free tail. **NO Nix mirror** — estate ruling
140-
2026-05-18 (Guix primary + sealed-container escape). `flake.nix` is
141-
deprecated and removed; a `flake.nix` that only mirrors the Guix manifest is
142-
drift, not a fallback. A second packager is permitted only where it is the
143-
sole source of a specific named dependency, documented as such.
139+
for the not-in-Guix / non-free tail. **NO Nix anywhere** — estate ruling
140+
2026-05-18 (Guix primary + sealed-container escape), hardened 2026-06-01
141+
(nix deprecated estate-wide; do NOT add `flake.nix`/`flake.lock` back).
142+
A second packager is permitted only where it is the sole source of a
143+
specific named dependency, documented as such.
144144
- **JS deps**: Deno (deno.json imports)
145145

146146
### Security Requirements

.github/dependabot.yml

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,6 @@ updates:
1616
actions:
1717
patterns:
1818
- "*"
19-
- package-ecosystem: "nix"
20-
directory: "/"
21-
schedule:
22-
interval: "weekly"
2319
- package-ecosystem: "npm"
2420
directory: "/"
2521
schedule:

.github/workflows/live-provers.yml

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,10 @@
1212
#
1313
# Reproducibility paths (both tried; at least one must succeed):
1414
# 1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
15-
# 2. Nix flake (fallback): nix develop .#live-provers
16-
# 3. apt-get (expedient bootstrap for T1 only): jobs below
15+
# 2. apt-get (expedient bootstrap for T1 only): jobs below
16+
#
17+
# (Nix flake removed 2026-06-01 per estate-wide nix-deprecation directive;
18+
# Guix is the sole reproducible-build primary.)
1719

1820
name: Live Provers
1921

RSR_COMPLIANCE.adoc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,14 +32,14 @@ the contractiles and the machine-readable policies above.
3232
| RSR-H10 | Prohibited: Python outside `salt/`; TypeScript/JS (use AffineScript); `Dockerfile` (use `Containerfile`); CUE (use Nickel) | `RSR_OUTLINE.adoc`
3333
| RSR-H11 | Canonical dirs: `config/`, `docs/`, `docs/generated/`, `docs/man/`, `src/`, `tests/` | `RSR_OUTLINE.adoc`
3434
| RSR-H12 | `just validate-rsr` passes on every PR | `MAINTENANCE-CHECKLIST.adoc:69`
35-
| RSR-H13 | Guix is primary package manager; sealed-container escape only; no Nix fallback (estate ruling 2026-05-18) | `.claude/CLAUDE.md`
35+
| RSR-H13 | Guix is the sole package manager; sealed-container escape only; nix deprecated estate-wide 2026-06-01 | `.claude/CLAUDE.md`
3636
| RSR-H14 | Justfile is the primary build system (no Make, etc.) | `MUST.contractile:42`
3737
| RSR-H15 | Podman, not Docker, for containers | `MUST.contractile:44`
3838
|===
3939

4040
== Soft conventions (SOFT; aspirational)
4141

42-
* Language tiers: Tier-1 = Rust, Elixir, Zig, Ada, Haskell, ReScript/AffineScript; Tier-2 = Nickel, Racket, Guile, Nix.
42+
* Language tiers: Tier-1 = Rust, Elixir, Zig, Ada, Haskell, ReScript/AffineScript; Tier-2 = Nickel, Racket, Guile. (Nix removed from Tier-2 on 2026-06-01 per estate-wide deprecation.)
4343
* Coverage above 80 %.
4444
* Performance benchmarks show no regression PR-over-PR.
4545
* Generated docs in `docs/generated/`; man pages in `docs/man/`.

docs/handover/L3-LIVE-PROVER-CI-PROMPT.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
**Context**: Echidna (`/var/mnt/eclipse/repos/verification-ecosystem/echidna/`) has 48 trait-wired
44
prover backends, but CI only tests them with `MockProver`. Mission: make every provisionable
5-
backend run against a canonical micro-goal on a predictable cadence. Guix primary, Nix fallback.
5+
backend run against a canonical micro-goal on a predictable cadence. Guix sole primary (nix deprecated estate-wide 2026-06-01).
66

77
**Master plan**: `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md`
88
**Order**: L3 (this) → L1 (Cap'n Proto) → L2 (Chapel max).
@@ -13,7 +13,7 @@ backend run against a canonical micro-goal on a predictable cadence. Guix primar
1313

1414
Wave-1 (Tier-1, every PR — 9 backends) DONE in kickoff session, commit `b022bf4`:
1515
- `manifests/live-provers.scm` — Guix manifest with Tier-1 + Tier-2 provers
16-
- `flake.nix` — expanded with matching `liveProverDeps`
16+
- ~`flake.nix` — expanded with matching `liveProverDeps`~ (removed 2026-06-01 per estate-wide nix-deprecation)
1717
- `.github/workflows/live-provers.yml` — tiered workflow (Tier-1 PR, Tier-2 nightly, etc.)
1818
- `tests/live_prover_suite.rs` — Rust test harness with Tier-1 version-check tests
1919

docs/handover/PRODUCTION-WIRING-PLAN.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ subprocess CI across ~38/48 backends, Cap'n Proto IPC, Chapel as first-class exe
1515
|---|---|---|
1616
| D1 | **Serialization = Cap'n Proto** | Chosen over Bebop3 for dependability+maturity (Cloudflare Workers use at scale), zero-copy reads, strongest schema-evolution story. Tradeoff: heavier codegen. Shim Julia/Chapel via C-ABI (fits existing Idris2-ABI + Zig-FFI policy). |
1717
| D2 | **Chapel = first-class, maximal** | Existing POC (`chapel_poc/parallel_proof_search.chpl`, 420 LoC) promoted to `src/chapel/`. Expand into portfolio dispatch, speculative tactic search, corpus-parallel ops, mutation-testing parallelism, multi-locale distributed, numeric hot paths. |
18-
| D3 | **Guix primary, Nix fallback** | Per project `CLAUDE.md` package-management policy. `guix.scm` / `manifests/live-provers.scm` authoritative; `flake.nix` mirrors. |
18+
| D3 | **Guix sole primary** | Per project `CLAUDE.md` package-management policy. `guix.scm` / `manifests/live-provers.scm` authoritative. (Nix fallback removed 2026-06-01 per estate-wide nix-deprecation directive — originally D3 said "Nix fallback"; that path is now closed.) |
1919
| D4 | **Execution order = L3 → L1 → L2** | Live-prover CI first: highest-leverage gap, surfaces real bugs mocks hide, no protocol break. Cap'n Proto next, since Chapel wiring (L2) will consume those schemas. |
2020
| D5 | **Live-prover CI cadence = tiered** | Tier-1 every PR, Tier-2 nightly, Tier-3 weekly, Tier-4 "best-effort / allow-fail" quarterly. |
2121
| D6 | **No JSON emit** | Per memory rule `feedback_no_json_emit_a2ml`. Cap'n Proto replaces the current HTTP-JSON Rust↔Julia channel. Tool config stays Nickel/A2ML. |
@@ -30,11 +30,12 @@ subprocess CI across ~38/48 backends, Cap'n Proto IPC, Chapel as first-class exe
3030

3131
**Artefacts**:
3232
- `manifests/live-provers.scm` — Guix manifest listing all provisionable prover binaries
33-
- `flake.nix` — Nix fallback, mirror of Guix set
3433
- `.github/workflows/live-provers.yml` — tiered CI workflow (PR/nightly/weekly/quarterly)
3534
- `tests/live_prover_suite.rs` — Rust test harness with canonical goals per backend
3635
- `tests/live_goals/` — micro-goal fixtures (one per backend, per category)
3736

37+
(Originally also planned `flake.nix` as a Nix-fallback mirror of the Guix set; removed 2026-06-01 per estate-wide nix-deprecation directive.)
38+
3839
**Tier assignment** (per `/var/mnt/eclipse/repos/verification-ecosystem/echidna/src/rust/provers/` audit):
3940

4041
| Tier | Cadence | Backends |

docs/handover/STATE.md

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,17 +16,18 @@ IPC end-to-end, Chapel as first-class parallel execution layer." Three
1616
phases, deliberately sequenced **L3 → L1 → L2**: live-prover CI first
1717
because it surfaces real bugs mocks hide, Cap'n Proto next so Chapel
1818
can consume its schemas, Chapel last because its sub-waves are the
19-
largest piece. Guix is the authoritative package manager throughout
20-
with Nix as fallback. GitHub is the single source of truth; no other
21-
forges pushed directly.
19+
largest piece. Guix is the sole authoritative package manager
20+
throughout (nix fallback removed 2026-06-01 per estate-wide
21+
nix-deprecation directive). GitHub is the single source of truth; no
22+
other forges pushed directly.
2223

2324
## Decisions locked
2425

2526
| # | Decision | Rationale |
2627
|---|----------|-----------|
2728
| D1 | **Serialization = Cap'n Proto** | Chosen over Bebop3 for dependability + maturity (Cloudflare Workers use at scale), zero-copy reads, strong schema-evolution. Tradeoff: heavier codegen; shim Julia/Chapel via C-ABI (fits existing Idris2-ABI + Zig-FFI). |
2829
| D2 | **Chapel = first-class, maximal** | 420-LoC POC promoted to `src/chapel/` across 7 sub-waves — portfolio dispatch, speculative tactic search, corpus-parallel ops, mutation-testing parallelism, multi-locale distributed, numeric hot paths. |
29-
| D3 | **Guix primary, Nix fallback** | Per project CLAUDE.md. `guix.scm` / `manifests/live-provers.scm` authoritative; `flake.nix` mirrors. |
30+
| D3 | **Guix sole primary** | Per project CLAUDE.md. `guix.scm` / `manifests/live-provers.scm` authoritative. (Originally "Nix fallback"; that path closed 2026-06-01 per estate-wide nix-deprecation directive.) |
3031
| D4 | **Execution order = L3 → L1 → L2** | Live-prover CI first: highest-leverage gap, surfaces real bugs mocks hide. Cap'n Proto next, since Chapel consumes those schemas. |
3132
| D5 | **Live-prover CI cadence tiered** | T1 every PR, T2 nightly, T3 weekly, T4 quarterly allow-fail. |
3233
| D6 | **No JSON emit on hot path** | Per `feedback_no_json_emit_a2ml`. Cap'n Proto replaces HTTP-JSON Rust↔Julia. Tool config stays Nickel/A2ML. |

docs/handover/TODO.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ core. **Consolidated 2026-05-18** into a single multi-target
5252
primary path (only SCIP/OR-Tools/Metamath are in Guix; 5 need bespoke package
5353
defs; Imandra is non-free) — per the 2026-05-18 estate ruling, the sealed
5454
container *is* the escape hatch for the not-in-Guix / non-free tail (Guix
55-
primary, no Nix mirror; `flake.nix` deprecated). Imandra target remains
55+
primary, no Nix mirror; `flake.nix` deprecated and removed estate-wide 2026-06-01). Imandra target remains
5656
licence-gated. Table below kept for the per-backend install strategy of record.
5757

5858
Handover hints live in `.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints]`.

docs/handover/llm-warmup-dev.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -176,9 +176,11 @@ All in `.machine_readable/`:
176176
## Packaging
177177

178178
- `guix.scm` — Guix package definition (uses cargo-build-system)
179-
- `flake.nix` — Nix flake (with rust-overlay)
180179
- `Containerfile` — Podman container
181180

181+
(Nix flake removed 2026-06-01 per estate-wide nix-deprecation directive;
182+
Guix is the sole packaging primary.)
183+
182184
## Test Structure
183185

184186
- 232 unit tests (`cargo test --lib`)

docs/wiki/Getting-Started.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ This page is a short orientation; defer to those for current details.
1616
- **Guix** (primary package manager; sealed-container escape hatch at `.containerization/Containerfile.wave3`)
1717
- **Podman** (containers — RSR-H15; **do not** use Docker)
1818

19-
> Note: Nix as a fallback was deprecated in the 2026-05-18 estate ruling. Use Guix or the sealed container only.
19+
> Note: Nix as a fallback was deprecated in the 2026-05-18 estate ruling and fully removed estate-wide on 2026-06-01. Use Guix or the sealed container only.
2020
2121
## Quick setup
2222

0 commit comments

Comments
 (0)