From 89648b204794c008176cbe98578fa64ec093c012 Mon Sep 17 00:00:00 2001 From: David Abram Date: Sat, 10 Oct 2026 16:23:44 +0200 Subject: [PATCH] perf(nix): use test-profile Crane cache and avoid duplicate Quint MBT check --- .github/workflows/quint.yml | 6 +- context/cli/mutation-trace-quint-connect.md | 73 ++++++++++----------- context/sce/flake-build-performance.md | 25 +++++++ flake.nix | 70 ++++++++++++-------- 4 files changed, 105 insertions(+), 69 deletions(-) diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index 18395f894..323f68532 100644 --- a/.github/workflows/quint.yml +++ b/.github/workflows/quint.yml @@ -55,7 +55,7 @@ jobs: needs: detect if: needs.detect.outputs.quint == 'true' runs-on: ubuntu-latest - # The Quint Connect Nix check compiles the CLI crate, so this needs more + # The focused Quint Connect Nix package compiles the CLI crate, so this needs more # headroom than the pure-Quint steps alone required. timeout-minutes: 30 steps: @@ -96,11 +96,11 @@ jobs: --max-steps=20 - name: Quint Connect model-based tests (Nix-pinned Rust + Quint) - # The entire MBT invocation goes through this Nix check rather than + # 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 .#checks.x86_64-linux.mutation-trace-quint-connect --print-build-logs + run: nix build .#mutation-trace-quint-connect --print-build-logs gate: name: Quint gate diff --git a/context/cli/mutation-trace-quint-connect.md b/context/cli/mutation-trace-quint-connect.md index 1cd5e78f1..c5c84285e 100644 --- a/context/cli/mutation-trace-quint-connect.md +++ b/context/cli/mutation-trace-quint-connect.md @@ -183,52 +183,47 @@ generate traces toward that boundary. The dedicated no-wrap regressions in `mutation-trace-revision-refinement.md` remain the sole targeted coverage for it; this harness's coverage is incidental, not a substitute. -## CI: two Nix checks, both need Quint +## CI: full flake check plus an opt-in focused runner -`mutation_trace::mbt` is registered as an ordinary `#[cfg(test)] mod mbt;` -(gated behind `#[cfg(test)]` in `mutation_trace/mod.rs`), so it is compiled -and run by *any* `cargo test` over the CLI crate — including the pre-existing -generic `checks.cli-tests` in `flake.nix`, not only a dedicated focused -check: +`mutation_trace::mbt` is an ordinary `#[cfg(test)] mod mbt;` module in +`mutation_trace/mod.rs`. The full Rust check already exercises it, so the +default flake check must not compile and run it again as a second derivation: ```text checks.cli-tests - -> full `cargo test`, including mutation_trace::mbt - -> needs the pinned Quint binary on PATH + -> full cargo test, including mutation_trace::mbt + -> pinned Quint on PATH -checks.mutation-trace-quint-connect - -> focused `cargo test ... mutation_trace::mbt` only - -> needs the pinned Quint binary on PATH +packages.mutation-trace-quint-connect (explicit invocation only) + -> focused cargo test ... mutation_trace::mbt + -> pinned Quint on PATH ``` -Both checks list the Nix `quint` package in `nativeCheckInputs`. Quint's -presence alone is not sufficient, though: `quint run`/`quint test` resolve -the spec by a path relative to the `cli/` crate root -(`../spec/mutation_cursor.qnt`), and `craneLib.fileset.commonCargoSources` -only covers each crate's own Cargo-referenced sources, not files outside any -crate. `workspaceSrc`'s Nix fileset therefore lists the top-level `spec/` -directory explicitly; without it, the spec never reaches either check's -sandbox and every MBT test fails with an opaque `"Quint returned non-zero -code."` (`quint-connect`'s error formatting is `Display`-only, so the -underlying Quint stderr explaining *why* — file not found — never surfaces -in the Rust test panic). - -`checks.mutation-trace-quint-connect` follows the same `craneLib.cargoTest` -pattern as `cli-tests`/`cli-clippy`/`cli-fmt`, reusing the pinned -`rustToolchain`/`cargoArtifacts`, scoped via `cargoTestExtraArgs`, printing -`rustc`/`cargo`/`quint --version` in `preCheck`. Both checks are part of -ordinary `nix flake check` (not Linux-only); `.github/workflows/quint.yml` -additionally invokes the dedicated check directly (`nix build -.#checks.x86_64-linux.mutation-trace-quint-connect`) for fast, targeted -feedback without waiting on the full Nix CI matrix — the entire invocation -comes from Nix, never a second, unpinned Rust toolchain stitched together -with the runner's own Cargo. That workflow's change detector also watches -`cli/src/services/mutation_trace/mbt/**`, `.../protocol.rs`, `.../types.rs`, -`cli/Cargo.toml`, `cli/Cargo.lock` (`flake.nix`/`flake.lock` were already -watched), so a Rust-only refinement/driver change triggers Quint CI without -touching the spec. Its "Run Quint tests" step passes `--match '^test.*'` — -omitting `--match` silently selects zero tests on this spec rather than -running the named scenarios. +Both runners use Crane's separate test-profile dependency artifacts, the same +pinned Rust toolchain, and `nativeCheckInputs = [ pkgs.git pkgs.quint ]`. +The test profile is unoptimized and uses line-table-only debug information; +production binaries continue using their existing release-profile artifacts. + +Run all checks (including MBT **once**) with `nix flake check`. To run only +the focused MBT suite, use: + +```sh +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. + +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` +silently selects zero named scenarios on this spec. ## Non-goals diff --git a/context/sce/flake-build-performance.md b/context/sce/flake-build-performance.md index 2e5b94ab9..7af52bf02 100644 --- a/context/sce/flake-build-performance.md +++ b/context/sce/flake-build-performance.md @@ -33,6 +33,31 @@ rebuilding dependency artifacts or formatting. The `cli-generated-input` flake check verifies the payload roots and both inventories independently of Cargo compilation. +## Rust test profile and focused Quint MBT + +Crane defaults to the release profile, including for `cargoTest` and +`cargoClippy`. To avoid repeatedly optimizing the test binary, the flake now +has two isolated sets of dependency artifacts: + +- `cargoArtifacts` remains release-profile, reused by native and release + package builds where applicable. Release optimization and embedding are + unchanged. +- `cargoArtifactsTest` uses `CARGO_PROFILE = "test"` and + `CARGO_PROFILE_TEST_DEBUG = "line-tables-only"`. The same artifacts are + passed to `cli-tests`, `cli-clippy`, and the optional focused Quint MBT + runner, preventing accidental test/release profile cache mixing. + +The existing `checks.cli-tests` already includes `mutation_trace::mbt`. +Therefore `nix flake check` runs this suite once rather than also building a +second focused MBT check. The focused runner is available independently at +`nix build .#mutation-trace-quint-connect -L`, and the Quint workflow calls +that package when targeted testing is useful. + +**Cold-cache trade-off:** test and release dependency profiles produce +different Cargo artifacts, so the first build may compile both sets. Subsequent +test and Clippy runs reuse the test-profile cache. Benchmark cold and warm runs +on both Linux and macOS before claiming a measured speedup. + ## Benchmark method Measurements were taken on x86_64-linux with 8 logical cores, Nix 2.34.8, and a diff --git a/flake.nix b/flake.nix index dde943a68..5577cf5c7 100644 --- a/flake.nix +++ b/flake.nix @@ -390,6 +390,26 @@ cargoArtifacts = craneLib.buildDepsOnly cargoDepsArgs; + # Keep production artifacts on Crane's release profile. The test and + # Clippy derivations use the unoptimized Cargo test profile with a + # separate dependency cache, so changing CLI sources does not require + # repeatedly optimizing the entire Rust test binary. + testProfileArgs = { + CARGO_PROFILE = "test"; + # Preserve useful file/line backtraces without full DWARF debug info. + CARGO_PROFILE_TEST_DEBUG = "line-tables-only"; + }; + + cargoArtifactsTest = craneLib.buildDepsOnly ( + cargoDepsArgs + // testProfileArgs + // { pname = "sce-test-deps"; } + ); + + testCargoArgs = commonCargoArgs // testProfileArgs // { + cargoArtifacts = cargoArtifactsTest; + }; + scePackage = craneLib.buildPackage ( commonCargoArgs // { @@ -1529,6 +1549,24 @@ ''} ''; + # 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. + mutationTraceQuintConnectCheck = craneLib.cargoTest ( + testCargoArgs + // { + pname = "sce-mutation-trace-quint-connect"; + doCheck = true; + cargoTestExtraArgs = "mutation_trace::mbt"; + nativeCheckInputs = [ pkgs.git pkgs.quint ]; + preCheck = '' + rustc --version + cargo --version + quint --version + ''; + } + ); + sceApp = { type = "app"; program = "${scePackage}/bin/sce"; @@ -1552,6 +1590,7 @@ ci-checks = ciChecks; bun = bunPackage; quint = pkgs.quint; + mutation-trace-quint-connect = mutationTraceQuintConnectCheck; quint-language-server = quintLanguageServerPackage; turso = tursoPackage; default = scePackage; @@ -1562,23 +1601,21 @@ # `mutation_trace::mbt` (the Quint Connect model-based-testing # harness) is an ordinary `#[cfg(test)]` module reached by the # full `cargo test` this check runs, so the pinned Quint binary - # must be on PATH here too, not only in the dedicated - # `mutation-trace-quint-connect` check below. + # must be on PATH for this check. The focused MBT runner is + # available separately as .#mutation-trace-quint-connect. cli-tests = craneLib.cargoTest ( - commonCargoArgs + testCargoArgs // { pname = "sce-cli-tests"; - inherit cargoArtifacts; doCheck = true; nativeCheckInputs = [ pkgs.git pkgs.quint ]; } ); cli-clippy = craneLib.cargoClippy ( - commonCargoArgs + testCargoArgs // { pname = "sce-cli-clippy"; - inherit cargoArtifacts; cargoClippyExtraArgs = "--all-targets --all-features"; } ); @@ -1590,27 +1627,6 @@ } ); - # Focused Quint Connect model-based-testing check: runs only - # `mutation_trace::mbt` under the repository's pinned Rust - # toolchain and pinned Quint binary, reusing the same - # `cargoArtifacts`/`commonCargoArgs` pipeline as `cli-tests` - # rather than a bespoke Rust+Quint environment. - mutation-trace-quint-connect = craneLib.cargoTest ( - commonCargoArgs - // { - pname = "sce-mutation-trace-quint-connect"; - inherit cargoArtifacts; - doCheck = true; - cargoTestExtraArgs = "mutation_trace::mbt"; - nativeCheckInputs = [ pkgs.git pkgs.quint ]; - preCheck = '' - rustc --version - cargo --version - quint --version - ''; - } - ); - cli-generated-input = cliGeneratedInputCheck; pkl-generated = pklGeneratedCheck; codex-hook-command = codexHookCommandCheck;