Open pwnorbitals opened 8 months ago
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 prusti
or 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_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.
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.
(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:![image](https://github.com/viperproject/prusti-dev/assets/8146140/098dbb6d-d979-469a-8734-4c8acfdf8a07)