Skip to content

fix: sysroot assembly verification + absolute path resolution#20

Open
avrabe wants to merge 5 commits intomainfrom
fix/sysroot-diagnostics-and-verification
Open

fix: sysroot assembly verification + absolute path resolution#20
avrabe wants to merge 5 commits intomainfrom
fix/sysroot-diagnostics-and-verification

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Apr 6, 2026

Summary

Fixes the can't find crate for 'core' error when using the bundled sysroot (#18).

Root cause: Bazel's download_and_extract with stripPrefix + cp -R merge silently failed on CI — the rust-std rlib files (libcore, libstd, etc.) never made it into the assembled sysroot. The sysroot had librustc_driver.so from the rustc component but no standard library rlibs.

Fix: Replace the fragile two-step pipeline with download + tar --strip-components=2, which extracts rust-std directly into the sysroot directory. This also:

  • Adds verification that libcore exists after sysroot assembly (fails early with clear error)
  • Resolves sysroot to absolute path to avoid symlink-based runfiles issues
  • Adds diagnostic output in verus_test to log sysroot contents

Diagnostic evidence

From CI run on Gale (commit 2a6907b):

Error in fail: Sysroot missing libcore for x86_64-unknown-linux-gnu. Contents:
rust_sysroot/lib/rustlib/etc/gdb_lookup.py

The sysroot had etc/ and bin/ from rustc but NO lib/ with rlibs — confirming the cp -R merge was a no-op.

Fixes #18

Test plan

  • Local: bazel clean --expunge && bazel fetch produces 27 rlibs + 78 total sysroot files
  • CI: Point Gale at this branch and verify Formal Verification passes

🤖 Generated with Claude Code

avrabe and others added 5 commits April 6, 2026 07:45
The repo rule now verifies that libcore exists in the assembled sysroot
after merging rust-std, failing early with a clear error if the merge
was incomplete. The test script logs the target lib directory contents
to diagnose the "can't find crate for core" failure on CI.

Ref #18

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Resolve the sysroot to an absolute path using `cd && pwd` to avoid
potential issues with relative path resolution through symlink-based
runfiles trees. Also enhanced the diagnostic output to use `find` for
deeper inspection when the target lib directory is missing.

Ref #18

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ust-std

The Bazel download_and_extract + cp -R merge approach silently failed
on CI — the rlib files (libcore, libstd, etc.) never made it into the
assembled sysroot. Replace with download + tar --strip-components=2
which extracts rust-std directly into the sysroot directory, bypassing
the fragile stripPrefix + cp -R pipeline.

Ref #18

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Three bugs in verus-strip 0.2.0 that silently corrupted or truncated
stripped output. All hit while extracting verified primitives from
pulseengine/relay.

1. Backtick-escaped `verus!` in doc comments matched the naive
   `input.find("verus!")` and caused the macro split to start at the
   comment, truncating real input. Fix: new `find_verus_macro_pos`
   scanner skips line comments, block comments, and string literals,
   and requires a token boundary before `verus!`.

2. The `exec` mode qualifier on `pub exec const` / `pub exec fn` /
   `pub exec static` was passed through verbatim, leaving invalid Rust.
   Fix: new `is_mode_qualifier_at` check in `strip_body` drops the
   keyword.

3. Everything after the `verus! { ... }` block was discarded because
   `strip_file` bound `_after`. This silently dropped `#[cfg(test)] mod
   tests`, trailing `use` statements, additional `impl` blocks, etc.
   Fix: `strip_file` now uses the `after` segment with vstd imports
   stripped and the `// verus!` end-of-block marker comment removed.

Adds 4 regression tests, one per bug plus an `exec fn` variant. All
13 lib tests + 4 integration tests pass.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
rules_rust 0.56.0 used the Bazel built-in `CcInfo` symbol, which
current Bazel has removed — module evaluation fails when consumers
pick up our minimum and don't override rules_rust themselves.
0.58.0 was the first release to load `CcInfo` from
`@rules_cc//cc/common:cc_info.bzl`, so it works on current Bazel.

This was forcing pulseengine/rivet to mark Verus CI as
`continue-on-error: true` (see rivet/.github/workflows/ci.yml:399).
With this bump that workaround can be removed.

Verified: `bazel build //tools/verus-strip:verus-strip` succeeds
with the new minimum (verus-strip is the only thing rules_verus
itself uses rules_rust for).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Verus toolchain at HEAD (8a2bbf6) has librustc_driver .so mismatch

1 participant