search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
173 stars 18 forks source link

librustc_driver not found when running tests #780

Open maximebuyse opened 1 month ago

maximebuyse commented 1 month ago

When I run cargo test --test toolchain I get the following error: 

/home/maxime/cryspen/hax/target/debug/cargo-hax: error while loading shared libraries: librustc_driver-f4e5b0d07cf2a17f.so: cannot open shared object file: No such file or directory

Building hax first and then running CARGO_TESTS_ASSUME_BUILT=y cargo test --test toolchain -- let-else works as a workaround.

franziskuskiefer commented 1 month ago

So this is a regression from #743? @W95Psp why aren't there tests catching something like this?

W95Psp commented 1 month ago

I don't know whether that's a regression from #743. I suspect that's a brittle bug that depends on setup. The CI uses this test harness with no problem, @maximebuyse and I need to investigate.