Skip to content

Conversation

@tautschnig
Copy link
Member

@tautschnig tautschnig commented Jul 28, 2025

Relevant upstream PR:

The update was done via

git grep -l 'stable_mir::' | xargs sed -i 's/stable_mir::/rustc_public::/'
git grep -l 'rustc_smir::' | xargs sed -i 's/rustc_smir::/rustc_public_bridge::/'

followed by manual touch-ups in kani-compiler/src/main.rs,
kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs,
tools/scanner/src/lib.rs, and then running scripts/kani-fmt.sh.

Resolves: #4229

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@tautschnig tautschnig requested a review from a team as a code owner July 28, 2025 09:52
@github-actions github-actions bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 28, 2025
Relevant upstream PR:
- rust-lang/rust#143848 (Rename `stable_mir` and
  `rustc_smir`)

The update was done via
```
git grep -l 'stable_mir::' | xargs sed -i 's/stable_mir::/rustc_public::/'
git grep -l 'rustc_smir::' | xargs sed -i 's/rustc_smir::/rustc_public_bridge::/'
```
followed by manual touch-ups in `kani-compiler/src/main.rs`,
`kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs`,
`tools/scanner/src/lib.rs`,  and then running `scripts/kani-fmt.sh`.

Resolves: model-checking#4229
@tautschnig tautschnig force-pushed the toolchain-2025-07-15-manual branch from bc54f0b to c45c8e8 Compare July 28, 2025 09:58
@tautschnig tautschnig changed the title Upgrade Rust toolchain to 2025-07-15 Upgrade Rust toolchain to 2025-07-21 Jul 28, 2025
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should also replace the StableMIR string inside our comments and documentation as well, so that later viewers of Kani don't need historical context to know what that refers to.

@tautschnig
Copy link
Member Author

I think we should also replace the StableMIR string inside our comments and documentation as well, so that later viewers of Kani don't need historical context to know what that refers to.

Isn't there a difference between the general idea of a stable MIR representation and the specific crates (now called rustc_public) that implement it? I am not sure that upstream PR has generally done away with the name if the overall idea.

@carolynzech
Copy link
Contributor

Isn't there a difference between the general idea of a stable MIR representation and the specific crates (now called rustc_public) that implement it? I am not sure that upstream PR has generally done away with the name if the overall idea.

My concern is more that future developers (or readers of our documentation) won't understand what all the references to StableMIR mean anymore. I think we typically use StableMIR as a proper noun, i.e., to refer to the crate. So you're right that the general idea holds, but I don't think that's how we're using it currently.

@tautschnig
Copy link
Member Author

My concern is more that future developers (or readers of our documentation) won't understand what all the references to StableMIR mean anymore. I think we typically use StableMIR as a proper noun, i.e., to refer to the crate. So you're right that the general idea holds, but I don't think that's how we're using it currently.

Thanks, I have adjusted comments and docs as I deemed it appropriate.

@tautschnig tautschnig enabled auto-merge July 29, 2025 09:06
@tautschnig tautschnig added this pull request to the merge queue Jul 29, 2025
Merged via the queue into model-checking:main with commit 9707a9c Jul 29, 2025
17 of 18 checks passed
@tautschnig tautschnig deleted the toolchain-2025-07-15-manual branch July 29, 2025 11:17
github-merge-queue bot pushed a commit that referenced this pull request Aug 7, 2025
from the autogenerated : 

## What's Changed
* Ensure that contract closures are FnOnce by @vonaka in
#4151
* Adjust sized hierarchy for Kani's memory predicates by @tautschnig in
#4193
* Update to Rust edition 2024 by @tautschnig in
#4197
* `ptr_offset_from`: Replace arithmetic over pointers by offset
arithmetic by @tautschnig in
#4180
* Automatic cargo update to 2025-07-07 by @github-actions[bot] in
#4208
* Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by
@dependabot[bot] in #4209
* Upgrade Rust toolchain to 2025-07-04 by @tautschnig in
#4199
* Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in
#4215
* Update CBMC dependency to 6.7.1 by @tautschnig in
#4178
* Split compiler flags to avoid dependency recompilation by
@AlexanderPortland in #4211
* Fix the bug that assign clause cannot be inferred for the inner loop
of nested loops by @thanhnguyen-aws in
#4179
* Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in
#4219
* Automatic toolchain upgrade to nightly-2025-07-12 by
@github-actions[bot] in #4222
* Fix bug: `goto-cc` crash when there are two quantifers in one proof by
@thanhnguyen-aws in #4221
* Automatic toolchain upgrade to nightly-2025-07-13 by
@github-actions[bot] in #4223
* Automatic cargo update to 2025-07-14 by @github-actions[bot] in
#4224
* Cleanup links to issues that have been addressed by @tautschnig in
#4200
* Selectively enable and fix (slow) Tokio tests by @tautschnig in
#4203
* Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by
@dependabot[bot] in #4227
* Implement support for Cargo.toml's default-members by @tautschnig in
#4201
* Do not invoke memset with count of zero by @tautschnig in
#4205
* Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig
in #4218
* Use CBMC's shuffle_vector expression by @tautschnig in
#4204
* Move tests from slow/kani back to regular suite by @tautschnig in
#4202
* Automatic toolchain upgrade to nightly-2025-07-14 by
@github-actions[bot] in #4225
* Enable GitHub Linux/Arm runners in CI by @tautschnig in
#3841
* Automatic cargo update to 2025-07-21 by @github-actions[bot] in
#4231
* Skip codegen for unneeded harnesses by @AlexanderPortland in
#4213
* Strongly type differing compiler args for clarity by
@AlexanderPortland in #4220
* Remove StableMIR ICE workaround by @carolynzech in
#4235
* Fix bug: Kani unwinds loops with contract in generic function (with -Z
loop-contracts) by @thanhnguyen-aws in
#4232
* Automatic cargo update to 2025-07-28 by @github-actions[bot] in
#4238
* Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by
@dependabot[bot] in #4242
* Upgrade Rust toolchain to 2025-07-21 by @tautschnig in
#4241
* Remove `pretty_ty` and use rustc_public's formatter instead by
@tautschnig in #4243
* Upgrade Rust toolchain to 2025-07-24 by @tautschnig in
#4244
* Documentation cleanup of UB detected by Kani by @tautschnig in
#4245
* Upgrade Rust toolchain to 2025-07-29 by @tautschnig in
#4247
* Automatic toolchain upgrade to nightly-2025-07-30 by
@github-actions[bot] in #4253
* Add unstable option prove-safety-only by @tautschnig in
#4239
* Set bits_per_byte in byte_extract expressions by @tautschnig in
#4255
* `KaniAttributes` Path Resolution Refactor by @carolynzech in
#4249
* Automatic toolchain upgrade to nightly-2025-07-31 by
@github-actions[bot] in #4256
* Support contracts & stubs in trait implementations (partial fix) by
@carolynzech in #4250
* [Breaking Changes] Remove unstable list feature and default memory
checks by @carolynzech in
#4258
* Upgrade Rust toolchain to 2025-08-01 by @tautschnig in
#4261
* Autoharness: add support for references by @tautschnig in
#4234
* Turn off debug assertions under `--prove-safety-only` by @tautschnig
in #4262
* Automatic toolchain upgrade to nightly-2025-08-02 by
@github-actions[bot] in #4264
* Automatic toolchain upgrade to nightly-2025-08-03 by
@github-actions[bot] in #4265
* Automatic cargo update to 2025-08-04 by @github-actions[bot] in
#4267
* Automatic toolchain upgrade to nightly-2025-08-04 by
@github-actions[bot] in #4266
* Introduce thread pool for writing goto binaries in parallel by
@AlexanderPortland in #4236
* Major-version update cargo dependencies by @tautschnig in
#4240
* Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by
@dependabot[bot] in #4270
* Automatic toolchain upgrade to nightly-2025-08-05 by
@github-actions[bot] in #4271
* Automatic toolchain upgrade to nightly-2025-08-06 by
@github-actions[bot] in #4272
* Avoid updating irrelevant symbols when handling quantifiers by
@AlexanderPortland in #4268
* Lazily evaluate debug info by @AlexanderPortland in
#4269
* Clone a template `BodyTransformer` to avoid re-initialization by
@AlexanderPortland in #4259
* Ensuring that MIR constants are marked as static consts by @vonaka in
#4233
* Fix release job dependencies by @tautschnig in
#4273

## New Contributors
* @vonaka made their first contribution in
#4151

**Full Changelog**:
kani-0.64.0...kani-0.65.0

---------

Co-authored-by: Zyad Hassan <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2025-07-15 failed

3 participants