Closed zgrannan closed 7 months ago
@fpoli It seems like using [build.'cfg(...)']
in .cargo/config.toml
has no effect, in the CI it reports
warning: unused config key `build.cfg(all(windows, target_arch="x86_64", target_env="msvc"))` in `D:\a\prusti-dev\prusti-dev\.cargo\config.toml`
unlike other sections it seems that [build]
cannot be made dependent on cfg
.
But I was able to clean up the workflow changes to minimize the extra stuff for windows.
Could it be that for some weird reason some GitHub actions try to use by default the gnu
target_env
instead of msvc
? That would also explain why the [build]
filter doesn't match.
It appears to be msvc
. This is the output of running rustc --print=cfg
as a test step on the windows builder.
debug_assertions
overflow_checks
panic="unwind"
relocation_model="pic"
target_abi=""
target_arch="x86_64"
target_endian="little"
target_env="msvc"
target_family="windows"
target_feature="fxsr"
target_feature="sse"
target_feature="sse2"
target_has_atomic
target_has_atomic="16"
target_has_atomic="32"
target_has_atomic="64"
target_has_atomic="8"
target_has_atomic="ptr"
target_has_atomic_equal_alignment="16"
target_has_atomic_equal_alignment="32"
target_has_atomic_equal_alignment="64"
target_has_atomic_equal_alignment="8"
target_has_atomic_equal_alignment="ptr"
target_has_atomic_load_store
target_has_atomic_load_store="16"
target_has_atomic_load_store="32"
target_has_atomic_load_store="64"
target_has_atomic_load_store="8"
target_has_atomic_load_store="ptr"
target_os="windows"
target_pointer_width="64"
target_thread_local
target_vendor="pc"
windows
In this Configuration Format document it appears that [build]
cannot have any config attached (unlike e.g. target
which supports [target.<cfg>]
)
Thanks for checking!
// If prusti was compiled for a custom target, e.g. via x.py build --target
// <triple>, then the executables will be placed in /target/<triple>/debug
// rather than /target/debug.
That's interesting. When compiling Prusti the build script of prusti-contracts-build
starts a second cargo build
process in parallel to the main compilation, using the same target folder to (1) share the build cache and (2) make cargo clean
automatically delete the target of the second compilation. Maybe our root issue is that (on Windows) the target folder is not meant to be shared across parallel compilations. This would explain why making the main compilation generate executables in /target/<triple>/debug
instead of /target/debug
avoids the conflict. As far as I understand the second compilation keeps generating its executables in /target/debug
because it doesn't use an explicit --target
.
If this explanation is correct, an alternative solution would be to use a different target folder, target/prusti-contracts/<release_mode>/
, when launching the second compilation from prusti-contracts-build
. I have a weak preference for this rather than adding conditionals and environment variables to the workflows (including coverage.yml
and deploy.yml
? crates-io.yml
?), but I'm also fine with the current solution if you prefer. This commit may be useful to see all that needs to be changed when specifying a new CARGO_TARGET_DIR
. Until November 2022 we were using the target folder prusti-contracts/target/debug
, but then changed to target/debug
for reasons (1) and (2) above.
I'll give it a try, as it seems like a better sol'n. Currently, I assume people on Windows can't build without specifying the target explicitly, which is not ideal.
@fpoli It looks like that worked! So right now we have prusti-contracts-build
putting stuff in the following directory structure:
ROOT/target/prusti-contracts/MODE/bin/
- For putting cargo-prusti
, prusti-rustc
etc that it itself will run
ROOT/target/prusti-contracts/MODE/verify/MODE
- For the generated specs, rlib files, etc.
where MODE
is either debug
or release
.
It looks like, unfortunately this still doesnt work :(
Okay it seems to work if --jobs=1 is added to ./x.py test
.
It seems like windows doesn't like that the cargo-prusti executable being copied when there is build parallelism.
Currently, the CI is reporting warnings of this form when building on windows.
These warnings are probably related to the CI failures. For some reason, explicitly specifying the target (i.e.
x86_64-pc-windows-msvc
) when building for windows in CI eliminates these errors and the build succeeds.This PR implements those changes. Explicitly specifying the target causes the executables to be generated in different directories; this PR changes some of the test files accordingly.