From e132a37427ff597aefb7ddf9d6dad734dd6a97b2 Mon Sep 17 00:00:00 2001
From: David Abram <david@crocoder.dev>
Date: Sat, 10 Oct 2026 16:24:02 +0200
Subject: [PATCH] ci(quint): avoid rebuilding MBT in spec-only workflow

---
 .github/workflows/quint.yml                 | 17 ++---------------
 context/cli/mutation-trace-quint-connect.md | 10 +++++-----
 flake.nix                                   |  2 +-
 3 files changed, 8 insertions(+), 21 deletions(-)

diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml
index 323f68532..7f4916bc1 100644
--- a/.github/workflows/quint.yml
+++ b/.github/workflows/quint.yml
@@ -55,8 +55,8 @@ jobs:
     needs: detect
     if: needs.detect.outputs.quint == 'true'
     runs-on: ubuntu-latest
-    # The focused Quint Connect Nix package compiles the CLI crate, so this needs more
-    # headroom than the pure-Quint steps alone required.
+    # The Rust/Quint Connect MBT suite already runs in the Nix CI cli-tests
+    # check on both Linux and macOS. Keep this workflow spec-only.
     timeout-minutes: 30
     steps:
       - name: Harden the runner (Audit all outbound calls)
@@ -70,12 +70,6 @@ jobs:
       - name: Install Nix
         uses: DeterminateSystems/nix-installer-action@ef8a148080ab6020fd15196c2084a2eea5ff2d25 # v22
 
-      - name: Enable Magic Nix Cache
-        uses: DeterminateSystems/magic-nix-cache-action@908b263ff629f4cc17666315b7fd3ec127c6244d # v14
-        with:
-          use-flakehub: false
-          use-gha-cache: true
-
       - name: Typecheck Quint spec
         run: nix run .#quint -- typecheck spec/mutation_cursor.qnt
 
@@ -95,13 +89,6 @@ jobs:
           --max-samples=5000
           --max-steps=20
 
-      - name: Quint Connect model-based tests (Nix-pinned Rust + Quint)
-        # The entire MBT invocation goes through this opt-in Nix package rather than
-        # `cargo test` on the runner's own Cargo, so both the Rust toolchain
-        # and the Quint binary come from the repository's pinned flake
-        # inputs, never a second, unpinned Rust installation.
-        run: nix build .#mutation-trace-quint-connect --print-build-logs
-
   gate:
     name: Quint gate
     if: always()
diff --git a/context/cli/mutation-trace-quint-connect.md b/context/cli/mutation-trace-quint-connect.md
index c5c84285e..00e244921 100644
--- a/context/cli/mutation-trace-quint-connect.md
+++ b/context/cli/mutation-trace-quint-connect.md
@@ -212,17 +212,17 @@ nix build .#mutation-trace-quint-connect --print-build-logs
 ```
 
 The focused package is intentionally absent from `checks`, but remains in
-`packages` so `.github/workflows/quint.yml` can run it on Quint-relevant
-changes without waiting for the full Nix CI matrix.
+`packages` for explicit, targeted MBT validation. `.github/workflows/quint.yml`
+runs Quint spec checks only, while `cli-tests` performs Rust refinement testing
+on both Linux and macOS in the ordinary Nix CI matrix.
 
 Quint's presence alone is not sufficient: `quint run` and `quint test`
 resolve the model via `../spec/mutation_cursor.qnt` relative to the
 `cli/` crate root. Therefore `workspaceSrc` must explicitly include the
 top-level `spec/` tree (it is not part of Crane's common Cargo sources).
 
-Quint CI continues to pin both Rust and Quint via the flake and separately
-runs the named `test.*` scenarios, the typecheck, and the randomized safety
-check. The workflow uses `--match '^test.*'` because omitting `--match`
+Quint CI continues to pin Quint via the flake and separately runs the named
+`test.*` scenarios, the typecheck, and the randomized safety check. The workflow uses `--match '^test.*'` because omitting `--match`
 silently selects zero named scenarios on this spec.
 
 ## Non-goals
diff --git a/flake.nix b/flake.nix
index 5577cf5c7..f9a280842 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1551,7 +1551,7 @@
 
         # The dedicated MBT runner is opt-in as a package, not a flake check:
         # cli-tests already executes the same mutation_trace::mbt test module.
-        # Quint CI still invokes this focused runner independently.
+        # The Quint workflow tests the spec separately, without rebuilding Rust MBT.
         mutationTraceQuintConnectCheck = craneLib.cargoTest (
           testCargoArgs
           // {