ci: Speed up Zisk and Nix builds, don't run on push: main

.github/actions/install-zisk/action.yml

@@ -1,18 +1,16 @@
 name: Install Zisk
 description: >-
   Install the system build deps, the ZisK zkVM toolchain (ziskup, CPU build),
-  and — unless `proving-key: false` — the fork-matching proving key needed to
-  RUN the Zisk host. Execute needs the key too (zisk-host's `client.setup()`
-  loads the circuit's const-tree files before either the execute or the prove
-  branch), but BUILDING the host does not, so build-only callers skip the
-  few-GB download + const-tree regeneration. Assumes a Rust toolchain is
-  already set up.
+  and — unless `proving-key: false` — the fork-matching proving key used for
+  proof generation. Build and execute-only callers can skip the few-GB
+  download and const-tree regeneration. Assumes a Rust toolchain is already
+  set up.
 
 inputs:
   proving-key:
     description: >-
-      Install the fork-matching proving key (required to execute or prove;
-      not needed to build). Set false for build-only jobs.
+      Install the fork-matching proving key. Required to prove, but not to
+      build or use the SDK's execute-only client.
     required: false
     default: "true"
 
@@ -107,9 +105,8 @@ runs:
       shell: bash
       run: cargo build --release -p proofman-starks-lib-c
       working-directory: zisk
-    # Execute still needs a proving key present: zisk-host calls `client.setup()`
-    # (which the SDK runs before the execute branch), and that loads the circuit's
-    # const-tree files. We host the fork-matching key in a public S3 bucket
+    # Proof generation needs the fork-matching proving key. It lives in a
+    # public S3 bucket
     # WITHOUT the const-trees — exactly like Zisk's released
     # `zisk-provingkey-*.tar.gz` on `storage.googleapis.com/zisk-setup` — and
     # regenerate them here with `cargo-zisk-dev check-setup -a`, which is how

.github/workflows/bench-main.yml

@@ -295,6 +295,8 @@ jobs:
       - name: Install Zisk
         if: matrix.params.backend == 'zisk'
         uses: ./.github/actions/install-zisk
+        with:
+          proving-key: false
       - run: echo "$HOME/.local/bin" >> $GITHUB_PATH
       # Provision the toolchain so the staged binaries find libleanshared
       # (no package build). use-github-cache off: nothing to cache here, and

.github/workflows/bench-pr.yml

@@ -557,6 +557,8 @@ jobs:
       - name: Install Zisk
         if: matrix.params.backend == 'zisk'
         uses: ./.github/actions/install-zisk
+        with:
+          proving-key: false
 
       # ---------- PR side ----------
       # The PR side runs first: `ix bench run` selects its constants from

.github/workflows/ci.yml

@@ -1,8 +1,6 @@
 name: CI Jobs
 
 on:
-  push:
-    branches: main
   pull_request:
   merge_group:
   workflow_dispatch:
@@ -127,15 +125,10 @@ jobs:
   # jobs and with each other after `build` succeeds. Both hosts exit
   # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk:
   # `reject_failures`), so a guest that compiles but panics / faults / rejects
-  # fails the job. SP1 execute is pure RISC-V emulation (no key). Zisk execute
-  # goes through `client.setup()`, which loads the circuit const-trees — so the
-  # Zisk job DOES install the fork-matching proving key (~3 GB + const-tree regen;
-  # verified against the Zisk source: `AsmCoreProver::new` requires the key at
-  # client-build time, before setup). SP1 and Zisk build as independent jobs so
-  # they parallelize; each installs only its own toolchain via sp1up / ziskup
-  # (prebuilt binaries). The apt list inside the install actions is the shared
-  # superset both backends need (proofman's C++ links OpenMPI/OpenMP/GMP/…;
-  # SP1's host crates need pkg-config + libssl-dev).
+  # fails the job. Both execute paths are keyless: Zisk uses its SDK's
+  # standalone execute-only client, which retains the ASM executor without
+  # initializing the prover. SP1 and Zisk build as independent jobs so they
+  # parallelize; each installs only its own toolchain via sp1up / ziskup.
   sp1-build:
     name: SP1 host build
     needs: build
@@ -184,11 +177,9 @@ jobs:
       - uses: ./.github/actions/setup-rust-toolchain
         with:
           cache-workspaces: zisk
-      # Proving key ON (the default): the execute step's `client.setup()` loads
-      # the circuit const-trees, and `AsmCoreProver::new` requires the key path
-      # to exist at client-build time — so an execute run needs it even though a
-      # build does not.
       - uses: ./.github/actions/install-zisk
+        with:
+          proving-key: false
       # Unit tests: the clap surface `ix bench run` drives, plus the closure auditor
       # (closure_detects_missing_dep self-skips without an IX_TEST_IXE
       # fixture — this gate has no Lean build to produce one).
@@ -205,11 +196,10 @@ jobs:
         with:
           name: nataddcomm-ixe
           path: .
-      # Run the guest ELF in the Zisk VM over the nataddcomm env. `zisk-host`
-      # exits 3 (EXIT_REJECTED, via `reject_failures`) if the kernel rejects any
-      # constant and non-zero on any VM fault — so the tool errors on failures,
-      # no output parsing. The ASM executor (default) mmaps with MAP_LOCKED, so
-      # raise the memlock limit in this shell for the tool it spawns.
+      # Run the guest ELF through Zisk's keyless ASM executor. `zisk-host` exits
+      # 3 (EXIT_REJECTED, via `reject_failures`) if the kernel rejects any
+      # constant and non-zero on any VM fault. The ASM executor mmaps with
+      # MAP_LOCKED, so raise the memlock limit for the tool it spawns.
       - name: Execute zisk-guest over the nataddcomm env
         working-directory: zisk
         env:

.github/workflows/merge-tests.yml

@@ -19,9 +19,19 @@ jobs:
       fail-fast: true
       matrix:
         include:
-          - name: Lake ignored tests
+          - name: Lake ignored tests (compile pipeline)
             kind: lake
             runner: warp-ubuntu-latest-x64-32x
+            test_args: --ignored compile-pipeline
+          - name: Lake ignored tests (kernel)
+            kind: lake
+            runner: warp-ubuntu-latest-x64-32x
+            test_args: --ignored kernel
+          - name: Lake ignored tests (misc)
+            kind: lake
+            runner: warp-ubuntu-latest-x64-32x
+            test_args: --ignored --exclude=compile-pipeline,kernel,typecheckers
+            zk_voting: true
           - name: Valgrind FFI
             kind: valgrind
             runner: warp-ubuntu-latest-x64-8x
@@ -63,16 +73,14 @@ jobs:
           key: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
 
-      # The proof build uses its own incremental cache and falls back to the
-      # base Lake cache without weakening the trust or sorry-frontier checks.
+      # A generic cache on the merge-queue ref can shadow a complete `lake-tc`
+      # cache from main, so this deliberately has no base-cache fallback.
       - if: ${{ matrix.kind == 'tc' }}
         uses: actions/cache@v6
         with:
           path: ./.lake
           key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
-            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
+          restore-keys: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
 
       # The Rust FFI bindgen build also needs the Lean toolchain and headers.
       - if: ${{ matrix.kind != 'valgrind' }}
@@ -88,13 +96,11 @@ jobs:
           build-args: "IxTests"
           use-github-cache: false
 
-      - name: Run general ignored Lake tests
+      - name: Run ignored Lake test partition
         if: ${{ matrix.kind == 'lake' }}
-        run: >-
-          lake test --wfail -- --ignored
-          --exclude=tc-pins,tc-accel-diff,tc-anon-diff,tc-init,tc-tutorial,tc-roundtrip,lean4lean
+        run: lake test --wfail -- ${{ matrix.test_args }}
       - name: Run ZK voting prover
-        if: ${{ matrix.kind == 'lake' }}
+        if: ${{ matrix.kind == 'lake' && matrix.zk_voting }}
         run: lake exe Apps.ZKVoting.Prover
 
       - name: Install valgrind
@@ -129,13 +135,9 @@ jobs:
       - name: Test Ix.Tc unit and adversarial fixtures
         if: ${{ matrix.kind == 'tc' }}
         run: lake test --wfail -- tc-unit
-      # These suites are partitioned from the general Lake sweep so the long
-      # parity and proof-related tests run concurrently with it.
       - name: Run Ix.Tc ignored tests
         if: ${{ matrix.kind == 'tc' }}
-        run: >-
-          lake test --wfail -- --ignored
-          tc-pins tc-accel-diff tc-anon-diff tc-init tc-tutorial tc-roundtrip lean4lean
+        run: lake test --wfail -- --ignored typecheckers
 
   merge-tests-result:
     name: Merge tests

.github/workflows/nix.yml

@@ -1,8 +1,6 @@
 name: Nix CI
 
 on:
-  push:
-    branches: main
   pull_request:
   merge_group:
   workflow_dispatch:
@@ -18,7 +16,7 @@ jobs:
   # Runs Lean tests via Nix
   nix-test:
     name: Nix Tests
-    runs-on: warp-ubuntu-latest-x64-8x
+    runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
       - uses: cachix/install-nix-action@v31
@@ -32,15 +30,8 @@ jobs:
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
       - run: nix run .#ix -- --help
-      # One step per check for separate logs; the store is shared across
-      # steps, so nothing rebuilds.
-      - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.clippy
-      - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.nextest
-      - run: nix build --print-build-logs --accept-flake-config .#checks.x86_64-linux.ix-tests
-      # Catch-all: builds every flake check for this system (near-free — the
-      # heavy ones above are already in the store), so a check added without
-      # its own step is still verified here.
-      - run: nix flake check --accept-flake-config
+      # A single invocation lets Nix schedule independent checks concurrently.
+      - run: nix flake check --print-build-logs --accept-flake-config
 
   # Tests Nix devShell support on Ubuntu
   nix-devshell:

README.md

@@ -195,13 +195,15 @@ cells locally, and `!benchmark` runs them on a PR — see
 **Lean tests:** `lake test`
 
 - `lake test -- <suite>` runs one or multiple primary test suites. Primary suites: `ffi`, `byte-array`, `ixon`, `claim`, `commit`, `canon`, `keccak`, `sharing`, `graph-unit`, `condense-unit`
-- `lake test -- --ignored` runs only the expensive test suites: `shard-map`, `rust-canon-roundtrip`, `serial-canon-roundtrip`, `parallel-canon-roundtrip`, `graph-cross`, `condense-cross`, `compile`, `decompile`, `rust-serialize`, `rust-decompile`, `commit-io`, `aiur`, `aiur-hashes`, `ixvm`
+- `lake test -- --ignored` runs all expensive test suites and runners
     - Most tests require at least 32 GB RAM
     - The `compile` and `decompile` tests require 128 GB RAM
-    - `aiur` and `aiur-hashes` generate ZK proofs and use significant CPU
-- `lake test -- --ignored <ignored-suite>` runs one or multiple expensive suites by name
+    - `ixvm` generates ZK proofs and uses significant CPU
+- `lake test -- --ignored <name>` runs one or more expensive suites, runners, or groups by name
+- Ignored groups: `compile-pipeline`, `kernel`, and `typecheckers`
+- `--exclude=<name,...>` excludes ignored suites, runners, or groups from a full ignored-test run
 - `lake test -- --include-ignored` runs both primary and expensive test suites
-- `lake test -- --include-ignored <ignored-suite>` runs all primary suites plus one or multiple expensive suites
+- `lake test -- --include-ignored <name>` runs all primary suites plus selected expensive suites, runners, or groups
 - `lake test -- cli` runs CLI integration tests
 - `lake test -- rust-compile` runs the Rust cross-compilation diagnostic
 

Tests/Main.lean

@@ -129,6 +129,50 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
   ("tc-ingress-meta", Tests.Tc.IngressMeta.suite),
 ]
 
+/-- Related ignored suites and runners that can be selected or excluded together. -/
+def ignoredGroups : Std.HashMap String (List String) := .ofList [
+  ("compile-pipeline", [
+    "rust-canon-roundtrip",
+    "serial-canon-roundtrip",
+    "parallel-canon-roundtrip",
+    "graph-cross",
+    "condense-cross",
+    "compile",
+    "decompile",
+    "rust-serialize",
+    "ixon-corpus",
+    "rust-decompile",
+    "validate-aux",
+    "aux-gen-diff",
+    "decompile-diff",
+  ]),
+  ("kernel", [
+    "kernel-ixon-roundtrip",
+    "kernel-tutorial",
+    "kernel-check-env",
+    "kernel-check-const",
+    "rust-kernel-build-primitives",
+    "rust-kernel-build-prim-origs",
+    "ixvm",
+  ]),
+  ("typecheckers", [
+    "tc-anon-diff",
+    "tc-init",
+    "tc-tutorial",
+    "tc-roundtrip",
+    "tc-ingress-meta",
+    "tc-pins",
+    "tc-accel-diff",
+    "lean4lean",
+  ]),
+]
+
+private def expandIgnoredNames (names : List String) : List String :=
+  (names.flatMap fun name =>
+    match ignoredGroups[name]? with
+    | some members => members
+    | none => [name]).eraseDups
+
 /-- Primary test runners — quick suites run by default alongside
 `primarySuites`, but kept as deferred `IO` actions (not `TestSeq`
 values) so their setup — Aiur system builds, STARK proofs — does not
@@ -297,14 +341,15 @@ def main (args : List String) : IO UInt32 := do
 
   let runIgnored := args.contains "--ignored"
   let includeIgnored := args.contains "--include-ignored"
-  -- `--exclude=a,b,c` drops the named ignored suites/runners from the sweep, so
-  -- one job can run every ignored test except the suites another job owns.
-  let excludeSet : List String :=
+  -- `--exclude=a,b,c` drops named ignored suites, runners, or groups.
+  let rawExcludeSet : List String :=
     match args.find? (·.startsWith "--exclude=") with
     | some a => (a.drop ("--exclude=".length)).toString.splitOn "," |>.filter fun s => !s.isEmpty
     | none => []
+  let excludeSet := expandIgnoredNames rawExcludeSet
   let filterArgs := args.filter fun a =>
     a != "--ignored" && a != "--include-ignored" && !a.startsWith "--exclude="
+  let ignoredFilterArgs := expandIgnoredNames filterArgs
 
   -- Run primary tests unless --ignored (without --include-ignored) is specified
   if !runIgnored || includeIgnored then
@@ -338,16 +383,16 @@ def main (args : List String) : IO UInt32 := do
     -- that matches nothing is an ERROR, not a silent no-op: otherwise a typo
     -- runs (or excludes) nothing and still reports success having executed
     -- nothing.
-    for arg in filterArgs ++ excludeSet do
+    for arg in ignoredFilterArgs ++ excludeSet do
       if !(allRunners.any fun (key, _) => key == arg)
           && !ignoredSuites.contains arg then
         IO.eprintln s!"error: no ignored suite or runner named '{arg}'"
         return 1
     let suites := excludeSet.foldl (fun m k => m.erase k) ignoredSuites
     let runners := allRunners.filter fun (key, _) => !excludeSet.contains key
-    let mut result ← LSpec.lspecIO suites filterArgs
-    let filtered := if filterArgs.isEmpty then runners
-      else filterArgs.filterMap fun arg => runners.find? fun (key, _) => key == arg
+    let mut result ← LSpec.lspecIO suites ignoredFilterArgs
+    let filtered := if ignoredFilterArgs.isEmpty then runners
+      else ignoredFilterArgs.filterMap fun arg => runners.find? fun (key, _) => key == arg
     for (_, action) in filtered do
       let r ← action
       if r != 0 then result := r

flake.nix

@@ -255,6 +255,7 @@
             lake2nix.mkPackage (
               lakeTestBuildArgs
               // {
+                lakeArtifacts = ixLib;
                 name = "IxTests";
                 installArtifacts = true;
               }