Upgrade Rust toolchain to nightly-2026-01-14#4643
Merged
tautschnig merged 1 commit intoJul 15, 2026
Merged
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR upgrades the pinned Rust nightly toolchain and updates Kani’s library/std to ensure Kani’s overridden macros (e.g., println!, assert!, panic!) are the ones users resolve from the prelude after Rust’s change to explicitly re-export core/std macros via std::prelude::v1.
Changes:
- Bump the repo toolchain from
nightly-2026-01-13tonightly-2026-01-14. - Add a Kani-owned
std::preludemodule (behindnot(concrete_playback)) that re-exports the real std prelude plus explicit re-exports of Kani’s macro overrides, including apanic!re-export using the “private-module” technique.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| rust-toolchain.toml | Updates the pinned nightly toolchain version. |
| library/std/src/lib.rs | Introduces a shadowing prelude module to ensure Kani macro overrides win over std/core prelude macro exports. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
toolchain-2026-01-14-manual
branch
2 times, most recently
from
f3bad50 to
e85b2ff
Compare
rust-lang/rust "Explicitly export core and std macros" replaced the `#[macro_use] extern crate std` prelude injection with explicit macro re-exports in `std::prelude::v1`. Kani's `library/std` re-exports the real prelude via `pub use std::*`, so user code began resolving the *original* `println!`/`assert!`/etc. instead of Kani's `#[macro_export]` overrides. The real `println!` then pulled its full formatting/I/O machinery into verification, including an unbounded `core::slice::memchr::memrchr` loop that made symbolic execution nonterminating (this is what hung the automated upgrade). Kani cannot simply re-export its overrides from `std::prelude::v1`: `assert`, `debug_assert`, `unreachable` and `panic` are *core*-prelude macros, so a `#![no_std]` dependency that imports the std prelude explicitly (`extern crate std; use std::prelude::v1::*;`, e.g. `lazy_static`) would then be ambiguous against the injected core prelude, a hard error (rust-lang/rust E0659). rustc only downgrades that ambiguity to a warning for the *builtin* std/core `panic`, not for a custom override. Instead: * `library/std`'s prelude is kept in sync with the real one, overriding only the print family (`print`/`println`/`eprint`/`eprintln`), which is defined in `std` and has no core-prelude counterpart, so it is safe everywhere. * `kani-compiler` injects `#[macro_use] extern crate std as _kani_std_macros;` at the crate root of every crate it compiles (via `after_crate_root_parsing`), except when building the standard library itself, for `#![no_std]`/`#![no_core]` crates, or when no external `std` is available. The last case covers `kani verify-std`, which builds `std` itself and passes no `--extern std`; injecting there would pull in a second `std`/`core` and produce duplicate lang-item errors (E0152). `#[macro_use]` places the overrides in the higher-priority macro-use prelude, shadowing the std/core prelude macros crate-wide (nested modules included) without the glob-vs-prelude ambiguity. Dependencies are included so their assertions get the same instrumentation as the crate under verification; `#![no_std]` dependencies keep the plain core macros (Kani still intercepts the panics they lower to), which is what avoids the E0659 above. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
toolchain-2026-01-14-manual
branch
from
e85b2ff to
ce92d6c
Compare
feliperodri
approved these changes
Jul 15, 2026
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.
rust-lang/rust "Explicitly export core and std macros" replaced the
#[macro_use] extern crate stdprelude injection with explicit macro re-exports instd::prelude::v1. Kani'slibrary/stdre-exports the real prelude viapub use std::*, so user code began resolving the originalprintln!/assert!/etc. instead of Kani's#[macro_export]overrides. The realprintln!then pulled its full formatting/I/O machinery into verification, including an unboundedcore::slice::memchr::memrchrloop that made symbolic execution nonterminating (this is what hung the automated upgrade).Give Kani's
stdits ownpreludemodule (shadowing the glob-re-exported one) whosev1re-exports the std prelude and then explicitly re-exports Kani's overridden macros (assert, assert_eq, assert_ne, debug_assert{,_eq,_ne}, print, eprint, println, eprintln, unreachable, and panic via the same private-module trick std uses). Explicit imports take precedence over the globs, so only the overridden macros are replaced. The edition submodules re-export their overrides explicitly to resolve the otherwise-ambiguous v1-vs-core glob imports.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.