facebookexperimental/MIRAI

Build failure

Closed this issue · 3 comments

croizier commented

Issue

Hi, I failed to build MIRAI on Windows 11, both with mingw64 and WSL2, with more or less the same problems each time.

Steps to Reproduce and actual results

I followed the installation guide, that is git clone https://github.com/facebookexperimental/MIRAI.git, cd MIRAI, cargo install --locked --path ./checker and failed to build Z3. Since I have noticed in commit messages that Z3 was now optional, I tried cargo install --locked --path ./checker --no-default-features, which succeeded but cargo mirai does nothing (or at least doesn't output anything) and mirai complains that it doesn't find some dynamic libraries (librustc_driver-*.dll and std-*.dll, the * meaning some generated integer).

That was with mingw64, so I switched to WSL2 (Ubuntu 22 LTS). cargo install --locked --path ./checker fails to build Z3 due to a compilation error and after cargo install --locked --path ./checker --no-default-features, mirai complains that librustc_driver-*.so is missing.

Expected Behavior

Mingw64 is an offbeat platform but I'd expect MIRAI to build just fine on Ubuntu.

Environment

$ rustup show
Default host: x86_64-unknown-linux-gnu
rustup home:  /home/val/.rustup

installed toolchains
--------------------

stable-x86_64-unknown-linux-gnu (default)
nightly-2022-11-24-x86_64-unknown-linux-gnu

active toolchain
----------------

nightly-2022-11-24-x86_64-unknown-linux-gnu (overridden by '/home/val/src/MIRAI/rust-toolchain.toml')

$ uname -a
Linux acer 5.15.79.1-microsoft-standard-WSL2 #1 SMP Wed Nov 23 01:01:46 UTC 2022 x86_64 x86_64 x86_64 GNU/Linux

$ head -1 /etc/os-release 
PRETTY_NAME="Ubuntu 22.04.1 LTS"
croizier commented

I've found the solution in the documentation of the fork hermanventer/MIRAI, which contains a guide for Linux.

Package openssl-sys failed to build but the error messages were helpful. All it needed was sudo apt install pkg-config libssl-dev.

hermanventer commented

The CI tests for MIRAI also builds and runs on Windows (see https://github.com/facebookexperimental/MIRAI/actions/runs/3569975751/jobs/6000497469). When running MIRAI on MIRAI on Windows, Z3 crashes, so this is is disabled in the CI. It may work in other scenarios.

See also prove-rs/z3.rs#203

croizier commented

Using tag v1.1.3 instead of branch main works better. Without Z3, MIRAI builds (real quick) on Mingw. With Z3, I haven't found the right setup to please CMake, but skipping Z3 may be OK for my use case (I just want to statically prevent out of bounds indexing.).