Fix windows CI builds

[zgrannan]

Currently, the CI is reporting warnings of this form when building on windows.

warning: output filename collision.
The bin target `prusti-driver` in package `prusti v0.2.2 (D:\a\prusti-dev\prusti-dev\prusti)` has the same output filename as the bin target `prusti-driver` in package `prusti v0.2.2 (D:\a\prusti-dev\prusti-dev\prusti)`.
Colliding filename is: D:\a\prusti-dev\prusti-dev\target\debug\deps\artifact\prusti-6354c6b870d0b669\bin\prusti_driver.exe
The targets should have unique names.
Consider changing their names to be unique or compiling them separately.
This may become a hard error in the future; see <https://github.com/rust-lang/cargo/issues/6313>.
warning: output filename collision.
The bin target `prusti-driver` in package `prusti v0.2.2 (D:\a\prusti-dev\prusti-dev\prusti)` has the same output filename as the bin target `prusti-driver` in package `prusti v0.2.2 (D:\a\prusti-dev\prusti-dev\prusti)`.
Colliding filename is: D:\a\prusti-dev\prusti-dev\target\debug\deps\artifact\prusti-6354c6b870d0b669\bin\prusti_driver.pdb

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.

[fpoli]

Awesome! I tried a few times to resolve that but without success. Would it work to specify the target triple in the .cargo/config.toml instead of adding logic to the workflows (src, src)?

[build.'cfg(...)']
target = "...triple..."

[zgrannan]

@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.

[fpoli]

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.

[zgrannan]

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>])

[fpoli]

Thanks for checking!

[fpoli]

Suggested change

	COMPILATION_TARGET_PRUSTI: ${{ matrix.os == 'windows-latest' && 'x86_64-pc-windows-msvc' || '' }}
	# Avoid file conflicts when compiling on Windows
	# See: https://github.com/viperproject/prusti-dev/pull/1476
	COMPILATION_TARGET_PRUSTI: ${{ matrix.os == 'windows-latest' && 'x86_64-pc-windows-msvc' || '' }}

[fpoli]

// 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.

[zgrannan]

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.

[zgrannan]

@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 :(

[zgrannan]

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.