fix(rocq_library): add self -Q even when out_dir is parent of dep paths - #35
Merged
Conversation
`rocq_library` was deliberately skipping the self `-Q out_dir prefix` whenever a dependency's `-Q` dir lived underneath `out_dir`, on the theory that the self mapping would "override" the dep. That is incorrect: coqc resolves overlapping `-Q dir prefix` mappings by deepest-ancestor match per source file, so a parent self `-Q` does NOT override a more specific dep -- the dep's mapping still wins for its own files. The actual consequence: when out_dir was a parent (e.g. `bazel-out/.../bin` in a standalone module), no self `-Q` reached the coqc command line, and the compiled `.vo` had no logical prefix -- just the source basename. That broke `From <prefix> Require Import x` imports of any generated `.v` whose target compiled at the bin root, including the entire standalone build of examples/rust_to_rocq. Only skip when a dep already maps the exact same directory (where two `-Q`s for one dir with different prefixes would be genuinely ambiguous). Also pin examples/rust_to_rocq's point.v to a position-stable Rocq logical prefix `Example` via `include_path` on both targets that compile it, so the example's hand-written point_proofs.v import (`From Example Require Import point`) resolves the same nested or standalone -- closes the residual flagged in the rules_rust migration (#34). Verified locally (nix + bazel): - `bazel test //tests:all //examples/rust_to_rocq:all` (nested) -> 5/5 pass - `cd examples/rust_to_rocq && bazel test //...` (standalone) -> 2/2 pass Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 task
avrabe
added a commit
that referenced
this pull request
Jul 21, 2026
…for #37 (#40) rules_rocq_rust had no rivet project. Initializes one (stpa + dev schemas) and seeds the top of the V so #37 (add Flocq/Gappa/Coq-Interval for machine-checked FP error-bound proofs) can be driven through the feature loop with traceability from commit one: - STPA: the loss is a false "verified" signal from this toolchain propagating into a downstream safety case (e.g. relay's flight-math kernels). H-001 generalizes an already-fixed failure class (the smpl .vo version mismatch in PR #30, the rocq_library -Q path issue in #35). H-002 is the new risk #37 introduces: trusting a Gappa-emitted proof certificate without replaying it through the Rocq kernel. - REQ-001/DD-002 document the existing mechanism (Bazel action-failure semantics + explicit Rocq-version pinning) that already satisfies the general constraint. - REQ-002/DD-001/FEAT-001 capture #37's own technical assessment (Gappa for rounding, Coq-Interval for approximation, Flocq underneath, every Gappa certificate kernel-replayed) as the accepted design. rivet validate passes; remaining warnings are expected (no test artifacts yet — this is the scaffold, not the implementation). Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Two-part fix that closes the standalone-build residual flagged in PR #34
(the
rules_rustmigration):rocq_libraryrule (rocq/private/rocq.bzl) — stop dropping theself
-Q out_dir prefixwhenever a dep's-Qdir lives underneathout_dir. coqc resolves overlapping-Qmappings by deepest-ancestormatch per source, so a parent self-
-Qdoes not override a morespecific dep -- the dep wins for its own files. Only skip when a dep
already maps the exact same directory.
examples/rust_to_rocq— give the translatedpoint.vaposition-stable Rocq logical prefix
Exampleviainclude_pathonboth
point_compiledandpoint_verified(they compete for thesame output path, so Bazel only deduplicates the conflict if the args
match).
point_proofs.vimports asFrom Example Require Import point, which now resolves the same nested or standalone.Why
The actual consequence of the over-cautious
rocq_librarycheck: whenout_dirwas a parent directory (typical when a target lives in the rootpackage, e.g. building
examples/rust_to_rocqas its own root module),no self
-Qreached the coqc command line — the compiled.vogotno logical prefix, only the source basename. That broke any
From <prefix> Require Import ximport of a generated.vwhose targetcompiled at the bin root — and so the entire standalone build of the
example module.
Verified
Nix + Bazel, locally:
bazel test //tests:all //examples/rust_to_rocq:all(nested, root module isrules_rocq_rust) — 5/5 passcd examples/rust_to_rocq && bazel test //...(standalone, root module is the example) — 2/2 passCloses the known residual from #34.
🤖 Generated with Claude Code