What I was trying to do: Evaluating whether rules_rocq_rust — a Bazel rule set wrapping a Rocq/Coq theorem-prover toolchain (Rocq core, coqutil, Hammer, smpl, Flocq, Gappa/gappalib-coq, Coq-Interval, Coquelicot, mathcomp-boot/fingroup, bignums, hierarchy-builder, coq-elpi) — should distribute that built toolchain through varve, so downstream consumers stop needing a local Nix install just to consume an already-built toolchain. Confirmed real: consumers currently hit recurring friction from requiring Nix locally (tracked as rules_rocq_rust#47 and rules_rocq_rust#48), and varve is this team's intended target if/when we move off that requirement — not a tool we're shopping around, the one we'd pick.
Tool + version: varve, source read at HEAD in this session (workspace version 0.32.0 per Cargo.toml, matching the latest release v0.32.0, 2026-09-05). CLI installed locally is 0.29.0 (behind), but this finding is against the current source, not the older binary's runtime behavior.
What happened — the capability gap: varve's only tree-shaped payload kind is Sdk (crates/varve-core/src/kind.rs), explicitly scoped in its own doc comment to "a C/C++ SDK tree (headers + libs + a cmake package)." Its relocation logic (export_sdk in crates/varve/src/main.rs, and REQ-SDK-001 in artifacts/requirements.yaml) supports exactly two shapes:
- A Yocto/VxWorks-style tree with one absolute install prefix baked into its binaries, byte-patched in place to a same-or-shorter path (the
relocate_sdk.py technique — if len(new_dl_path) >= p_filesz: ERROR).
- A tree that's already relative-to-itself by construction, like the Zephyr SDK (
arm-zephyr-eabi-gcc resolves via bin/../lib/gcc/... relative to its own location).
The very recent requirement fields (relocation-gap-2026-09-07, env-encoding-gap) confirm this is still actively being hardened against those two families specifically.
A Nix-built closure — which is what rules_rocq_rust's toolchain actually is — fits neither shape. It has dozens to hundreds of distinct absolute /nix/store/<hash>-<pkg>/... references scattered across RPATHs, OCaml findlib META/dune-package files, and dynlink search paths, for the entire transitive closure (not one prefix to patch). And it isn't relative-to-itself by construction — Nix deliberately uses absolute store-path RPATHs rather than $ORIGIN-relative ones, as part of its own hermeticity model. So even after we've done our own portability work on the rules_rocq_rust side (nix bundle / static linking / patchelf-rewriting the whole closure to shrink it to something varve could plausibly ingest), neither of Sdk's two relocation strategies applies to what we'd hand it.
Repro: Read crates/varve-core/src/kind.rs (the Sdk doc comment), crates/varve/src/main.rs (export_sdk, ExportSdk), and the REQ-SDK-001 / relocation-gap-2026-09-07 entries in artifacts/requirements.yaml, against the shape of a real Nix closure (e.g. nix build coqPackages.mathcomp-boot and inspect the RPATHs/META files it produces).
Workaround used (if any): None yet — we haven't attempted to force a Nix closure through the Sdk kind. We've stopped short of that, which is why this is filed now rather than after a failed attempt: the mismatch is structural (many-absolute-paths vs. one-prefix-or-self-relative), not a bug we could patch around on our side, so we wanted to raise it before spending the portability-engineering effort on our end.
Impact: Not currently blocking (rules_rocq_rust still builds and works fine on Nix directly) — but it's the load-bearing blocker for the larger move both linked issues describe. We don't yet know whether a Nix-closure-shaped tree payload kind (many absolute paths, whole-closure relocation) is something varve wants to take on at all, or whether the intended answer is "make your output relocatable yourself, we only ever support one-prefix/self-relative." Flagging so that's a deliberate scoping decision on varve's side rather than something we discover by attempting it. Happy to bring more detail on the actual shape of a Rocq/OCaml Nix closure if useful.
What I was trying to do: Evaluating whether
rules_rocq_rust— a Bazel rule set wrapping a Rocq/Coq theorem-prover toolchain (Rocq core, coqutil, Hammer, smpl, Flocq, Gappa/gappalib-coq, Coq-Interval, Coquelicot, mathcomp-boot/fingroup, bignums, hierarchy-builder, coq-elpi) — should distribute that built toolchain through varve, so downstream consumers stop needing a local Nix install just to consume an already-built toolchain. Confirmed real: consumers currently hit recurring friction from requiring Nix locally (tracked as rules_rocq_rust#47 and rules_rocq_rust#48), and varve is this team's intended target if/when we move off that requirement — not a tool we're shopping around, the one we'd pick.Tool + version: varve, source read at HEAD in this session (workspace version
0.32.0perCargo.toml, matching the latest releasev0.32.0, 2026-09-05). CLI installed locally is0.29.0(behind), but this finding is against the current source, not the older binary's runtime behavior.What happened — the capability gap: varve's only tree-shaped payload kind is
Sdk(crates/varve-core/src/kind.rs), explicitly scoped in its own doc comment to "a C/C++ SDK tree (headers + libs + a cmake package)." Its relocation logic (export_sdkincrates/varve/src/main.rs, andREQ-SDK-001inartifacts/requirements.yaml) supports exactly two shapes:relocate_sdk.pytechnique —if len(new_dl_path) >= p_filesz: ERROR).arm-zephyr-eabi-gccresolves viabin/../lib/gcc/...relative to its own location).The very recent requirement fields (
relocation-gap-2026-09-07,env-encoding-gap) confirm this is still actively being hardened against those two families specifically.A Nix-built closure — which is what rules_rocq_rust's toolchain actually is — fits neither shape. It has dozens to hundreds of distinct absolute
/nix/store/<hash>-<pkg>/...references scattered across RPATHs, OCaml findlibMETA/dune-packagefiles, and dynlink search paths, for the entire transitive closure (not one prefix to patch). And it isn't relative-to-itself by construction — Nix deliberately uses absolute store-path RPATHs rather than$ORIGIN-relative ones, as part of its own hermeticity model. So even after we've done our own portability work on the rules_rocq_rust side (nix bundle / static linking / patchelf-rewriting the whole closure to shrink it to something varve could plausibly ingest), neither ofSdk's two relocation strategies applies to what we'd hand it.Repro: Read
crates/varve-core/src/kind.rs(theSdkdoc comment),crates/varve/src/main.rs(export_sdk,ExportSdk), and theREQ-SDK-001/relocation-gap-2026-09-07entries inartifacts/requirements.yaml, against the shape of a real Nix closure (e.g.nix build coqPackages.mathcomp-bootand inspect the RPATHs/META files it produces).Workaround used (if any): None yet — we haven't attempted to force a Nix closure through the
Sdkkind. We've stopped short of that, which is why this is filed now rather than after a failed attempt: the mismatch is structural (many-absolute-paths vs. one-prefix-or-self-relative), not a bug we could patch around on our side, so we wanted to raise it before spending the portability-engineering effort on our end.Impact: Not currently blocking (rules_rocq_rust still builds and works fine on Nix directly) — but it's the load-bearing blocker for the larger move both linked issues describe. We don't yet know whether a Nix-closure-shaped tree payload kind (many absolute paths, whole-closure relocation) is something varve wants to take on at all, or whether the intended answer is "make your output relocatable yourself, we only ever support one-prefix/self-relative." Flagging so that's a deliberate scoping decision on varve's side rather than something we discover by attempting it. Happy to bring more detail on the actual shape of a Rocq/OCaml Nix closure if useful.