From f9afef2ce7efa25c043407fb24e63604bde171d2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 23 May 2026 14:22:37 +0200 Subject: [PATCH] fix(rocq_library): add self -Q even when out_dir is parent of dep paths `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 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) --- examples/rust_to_rocq/BUILD.bazel | 15 +++++++++++++-- examples/rust_to_rocq/point_proofs.v | 4 +++- rocq/private/rocq.bzl | 21 ++++++++++++--------- 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/examples/rust_to_rocq/BUILD.bazel b/examples/rust_to_rocq/BUILD.bazel index 8ff7405..3ab810b 100644 --- a/examples/rust_to_rocq/BUILD.bazel +++ b/examples/rust_to_rocq/BUILD.bazel @@ -27,10 +27,17 @@ coq_of_rust_library( ) # Step 2: Compile the translated Rocq code -# This compiles point.v to point.vo +# This compiles point.v to point.vo. +# `include_path` gives point.v a position-stable Rocq logical name -- +# `Example.point` -- regardless of whether this example is built nested in the +# rules_rocq_rust workspace or standalone as its own BCR test module. Without +# it, rocq_library would derive the prefix from ctx.label.package, which +# differs between nested ("examples.rust_to_rocq") and standalone ("") and so +# breaks point_proofs.v's import one way or the other. rocq_library( name = "point_compiled", srcs = [":point_translated"], + include_path = "Example", deps = [":rocq_of_rust_lib"], extra_flags = ["-impredicative-set"], ) @@ -38,11 +45,15 @@ rocq_library( # Method 2: Convenience macro (recommended) # ----------------------------------------- -# Single target that does both translation and compilation +# Single target that does both translation and compilation. +# `include_path = "Example"` must match the one on `point_compiled` above: +# both targets compile point.v to the same output path, and Bazel only +# deduplicates the colliding actions if their args (including `-Q`) are equal. rocq_rust_verified_library( name = "point_verified", rust_sources = ["point.rs"], edition = "2021", + include_path = "Example", extra_flags = ["-impredicative-set"], ) diff --git a/examples/rust_to_rocq/point_proofs.v b/examples/rust_to_rocq/point_proofs.v index a47b16e..199637e 100644 --- a/examples/rust_to_rocq/point_proofs.v +++ b/examples/rust_to_rocq/point_proofs.v @@ -11,7 +11,9 @@ - The [monadic] tactic wraps Value.t expressions with [pure] *) Require Import RocqOfRust.RocqOfRust. -From examples.rust_to_rocq Require Import point. +(* `Example` is the stable logical prefix set by point_compiled's include_path + (see BUILD.bazel) -- resolves the same nested or standalone. *) +From Example Require Import point. (* ========================================================================= *) (** * Section 1: Point::origin() Proofs *) diff --git a/rocq/private/rocq.bzl b/rocq/private/rocq.bzl index 0185749..64a50c4 100644 --- a/rocq/private/rocq.bzl +++ b/rocq/private/rocq.bzl @@ -151,15 +151,18 @@ def _rocq_library_impl(ctx): # nested files like lib/lib.vo get the correct logical path RocqOfRust.lib.lib out_dir = output_dir if output_dir else vo_file.dirname - # Check if out_dir conflicts with deps - out_conflicts = out_dir in dep_paths - if not out_conflicts: - for dep_path in dep_paths.keys(): - if dep_path.startswith(out_dir + "/"): - # out_dir is a parent of dep_path - would override - out_conflicts = True - break - if not out_conflicts: + # coqc resolves overlapping `-Q dir prefix` mappings by deepest-ancestor + # match per source file, so adding a self `-Q` whose dir is a *parent* + # of a dep's `-Q` dir does not override the dep -- the dep's more + # specific mapping still wins for its own files. Only skip when a dep + # already maps this exact directory (where two `-Q`s with different + # prefixes for the same dir would be genuinely ambiguous). + # + # Without adding the self `-Q`, the compiled .vo gets no logical prefix + # (just the basename), which breaks `From Require Import x` + # imports of generated files in root packages -- see the residual + # tracked in the rules_rust migration (Stage 4-fix follow-up). + if out_dir not in dep_paths: args.add("-Q") args.add(out_dir) args.add(logical_path)