Build failure on Arch Linux (could not find abi in rustc_target)

[orhun]

Hello, the maintainer of kani package here 👋🏼

I'm getting the following error(s) while building 0.59.0 in a clean Arch Linux chroot:

Logs

   Compiling charon v0.1.62 (/build/kani/src/kani-0.59.0/charon/charon)
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:17:19
   |
17 | use rustc_target::abi::{TagEncoding, Variants};
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:23:19
   |
23 | use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0433]: failed to resolve: could not find `abi` in `rustc_target`
  --> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:20:19
   |
20 | use rustc_target::abi::{
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:13:19
   |
13 | use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:20:19
   |
20 | use rustc_target::abi::{
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0433]: failed to resolve: could not find `abi` in `rustc_target`
  --> kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:38:19
   |
38 | use rustc_target::abi::call::FnAbi;
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:43:19
   |
43 | use rustc_target::abi::Endian;
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_target::abi`
  --> kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:39:19
   |
39 | use rustc_target::abi::{HasDataLayout, TargetDataLayout};
   |                   ^^^ could not find `abi` in `rustc_target`
                                                                                                                                                                                                                     
error[E0432]: unresolved import `rustc_data_structures::sync::Lrc`
 --> kani-compiler/src/session.rs:7:5
  |
7 | use rustc_data_structures::sync::Lrc;
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no `Lrc` in `sync`
                                                                                                                                                                                                                     
error[E0532]: expected tuple struct or tuple variant, found variant `Code`
   --> kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:260:21
    |
260 |                 let Code(term) = mapping.kind else { unreachable!() };
    |                     ^^^^^^^^^^ help: use struct pattern syntax instead: `Code { bcb: term }`
   --> /build/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_middle/src/mir/coverage.rs:170:5
    |
    = note: `Code` defined here
                                                                                                                                                                                                                     
error[E0433]: failed to resolve: could not find `abi` in `rustc_target`
  --> kani-compiler/src/kani_middle/transform/internal_mir.rs:45:51
   |
45 |                 maybe_field_idx.map(rustc_target::abi::FieldIdx::from_usize),
   |                                                   ^^^ could not find `abi` in `rustc_target`
   |
help: consider importing one of these items
   |
10 + use rustc_abi::FieldIdx;
   |
10 + use stable_mir::mir::FieldIdx;
   |
help: if you import `FieldIdx`, refer to it directly
   |
45 -                 maybe_field_idx.map(rustc_target::abi::FieldIdx::from_usize),
45 +                 maybe_field_idx.map(FieldIdx::from_usize),
   |
                                                                                                                                                                                                                     
error[E0433]: failed to resolve: could not find `abi` in `rustc_target`
   --> kani-compiler/src/kani_middle/transform/internal_mir.rs:210:47
    |
210 | ...                   rustc_target::abi::FieldIdx::from_usize(*field_idx),
    |                                     ^^^ could not find `abi` in `rustc_target`
    |
help: consider importing one of these items
    |
10  + use rustc_abi::FieldIdx;
    |
10  + use stable_mir::mir::FieldIdx;
    |
help: if you import `FieldIdx`, refer to it directly
    |
210 -                                 rustc_target::abi::FieldIdx::from_usize(*field_idx),
210 +                                 FieldIdx::from_usize(*field_idx),
    |
                                                                                                                                                                                                                     
error[E0277]: the trait bound `GotocCtx<'tcx>: HasDataLayout` is not satisfied
   --> kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:331:38
    |
331 | impl<'tcx> LayoutOfHelpers<'tcx> for GotocCtx<'tcx> {
    |                                      ^^^^^^^^^^^^^^ the trait `HasDataLayout` is not implemented for `GotocCtx<'tcx>`
    |
    = help: the following other types implement trait `HasDataLayout`:
              &TargetDataLayout
              LayoutCx<'tcx>
              TargetDataLayout
              TyCtxt<'tcx>
              TyCtxtAt<'tcx>
              rustc_const_eval::interpret::eval_context::InterpCx<'tcx, M>
              rustc_lint::context::LateContext<'tcx>
              rustc_smir::rustc_smir::Tables<'tcx>
note: required by a bound in `LayoutOfHelpers`
   --> /build/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_middle/src/ty/layout.rs:666:1

error[E0277]: the trait bound `GotocCtx<'tcx>: HasDataLayout` is not satisfied
   --> kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:346:32
    |
346 | impl<'tcx> HasTyCtxt<'tcx> for GotocCtx<'tcx> {
    |                                ^^^^^^^^^^^^^^ the trait `HasDataLayout` is not implemented for `GotocCtx<'tcx>`
    |
    = help: the following other types implement trait `HasDataLayout`:
              &TargetDataLayout
              LayoutCx<'tcx>
              TargetDataLayout
              TyCtxt<'tcx>
              TyCtxtAt<'tcx>
              rustc_const_eval::interpret::eval_context::InterpCx<'tcx, M>
              rustc_lint::context::LateContext<'tcx>
              rustc_smir::rustc_smir::Tables<'tcx>
note: required by a bound in `HasTyCtxt`
   --> /build/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_middle/src/ty/layout.rs:528:1

error[E0277]: the trait bound `GotocCtx<'tcx>: HasDataLayout` is not satisfied
   --> kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:359:37
    |
359 | impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
    |                                     ^^^^^^^^^^^^^^ the trait `HasDataLayout` is not implemented for `GotocCtx<'tcx>`
    |
    = help: the following other types implement trait `HasDataLayout`:
              &TargetDataLayout
              LayoutCx<'tcx>
              TargetDataLayout
              TyCtxt<'tcx>
              TyCtxtAt<'tcx>
              rustc_const_eval::interpret::eval_context::InterpCx<'tcx, M>
              rustc_lint::context::LateContext<'tcx>
              rustc_smir::rustc_smir::Tables<'tcx>
    = note: required for `GotocCtx<'tcx>` to implement `LayoutOfHelpers<'tcx>`
note: required by a bound in `FnAbiOfHelpers`
   --> /build/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_middle/src/ty/layout.rs:1304:1

Some errors have detailed explanations: E0277, E0432, E0433, E0532.
For more information about an error, try `rustc --explain E0277`.
error: could not compile `kani-compiler` (bin "kani-compiler") due to 15 previous errors

The nightly version is the following:

info: syncing channel updates for 'nightly-x86_64-unknown-linux-gnu'
info: latest update on 2025-02-12, rust version 1.86.0-nightly (92bedea1c 2025-02-11)

The build steps can be found at here. (It's simply cargo build after checking out the submodules).

Any idea why this is happening?

[tautschnig]

From your build steps I understand that you will always build against the latest nightly toolchain? If so you'll have to bear with us until we have addressed #3884.

[carolynzech]

We recommend that instead you use our release of 0.59, which has a rust-toolchain.toml file to pin the nightly version to 1/28. If you would prefer to build from source (not the recommended approach, but you can), you can clone from our main branch, which is currently up to 2/10's toolchain. See our installation instructions and how to build from source.

[carolynzech]

I took at look at your linked build steps, and I'm curious about lines 37-38:

rm -f rust-toolchain.toml
export RUSTUP_TOOLCHAIN=nightly

Why are you removing the rust-toolchain file? We do not recommend this approach--it means that the build will fail if Kani is not up-to-date with the most recent version of nightly (as you're seeing). We have a workflow to update our toolchain every day, but if upstream changes require changes in Kani, it does sometimes take us a few days to fix those errors, which means our toolchain will fall a bit behind.

[orhun]

I think the initial reasoning for that was keeping the package reproducible, but I now fail to see how that would work. So bringing the rust-toolchain.toml file and building that way actually solved the issue and I updated the package in the repos!

Thanks for the tips on building, I'll keep an eye on the build-from-source docs in case anything changes in the future!

Closing 🥂