viperproject
Prusti doesn’t run for the `thumbv7em-none-eabihf` target
(new user here) The rest of the project is well-configured, but it seems that Prusti is compiling in some kind of isolated environment and doesn’t take cross-compilation into account when running the Rust compiler.
Typical output:
Could you describe how to reproduce this issue? Do you run cargo prusti or something different?
Prusti by default uses the sysroot of the nightly rustc version specified in Prusti's repository. The RUST_SYSROOT environment variable can be used to force Prusti to use a different sysroot. Maybe that allows Prusti to work when cross-compiling, but we never tested this use case.
Could you describe how to reproduce this issue? Do you run
cargo prustior something different?
I used the Prusti extension in VSCode. I unfortunately couldn't get cargo prusti to run in my WSL machine for some reason
Prusti by default uses the sysroot of the nightly rustc version specified in Prusti's repository. The
RUST_SYSROOTenvironment variable can be used to force Prusti to use a different sysroot. Maybe that allows Prusti to work when cross-compiling, but we never tested this use case.
I understand, but this means all user configuration that allow their project to work will be lost. Cross-compilation requires the toolchain and linker, which you can't really have in this case. Does Prusti absolutely need a sysroot ?
cargo prusti and the IDE extension should ideally always work out of the box (i.e. in any situation where cargo clippy works), so what you reported is a bug in how Prusti interacts with the compiler. If I recall correctly, the sysroot is required by rustc, otherwise it'll not find the core/std libraries. Our decision of forcing a fixed Rust toolchain is very old; it's possible that we did that just to workaround some early issue and then forgot about it. If manually setting RUST_SYSROOT works for you, then we can easily remove the hardcoded toolchain version from Prusti. All the related code is here, and it should be enough to change 3 lines. The RUST_SYSROOT can be configured in the settings of the Prusti extension on VS Code. There is a prusti-assistant.extraPrustiEnv field that should be good enough.