Overview

The submodules must initialised to obtain the 3rd-party libraries, as shown below. Furthermore, we need a C++ compiler to build the mCRL2 toolset. This can be Visual Studio on Windows, AppleClang on MacOS or either GCC or Clang on Linux. In the latter case it uses whatever compiler is provided by the CC and CXX environment variables.

git submodule update --init --recursive
cargo build

By default this will build in dev or debug mode, and a release build can be obtained by passing --release. Note that it is necessary to run git submodule update --init after switching branches or pulling from the remote whenever any of the modules have been changed.

The mcrl2-sys crate uses cxx to set up a C-like FFI between the Rust code and C++ code, with static assertions to ensure that the FFI matches and some helpers for standard functionality such as std::unique_ptr. The resulting interface is generally unpleasant to work with so the crate mcrl2 has Rust wrappers around the resulting functionality.

Features

• cpptrace — provides stack traces on exceptions and assertions in the mCRL2 code, see Stack traces below. Requires cmake to be found on PATH to build the necessary components.
• jittyc — compiles the jittyc rewriter of mCRL2, which generates C++ code for the rewrite rules at run time and compiles it with the compiler found at run time. Enables mcrl2_create_rewriter_jittyc, which is not declared otherwise.

Native library

This crate declares links = "mcrl2", so at most one version of it can occur in a dependency graph and it owns the linking of the (statically built) mCRL2 sources. The build script emits no cargo::metadata= keys, so there are no DEP_MCRL2_* variables for downstream build scripts to read; everything needed to use the toolset is exposed through the cxx bridges in src/.

Stack traces

The cpptrace feature can be enabled to provide stack traces on exceptions and assertions in the mCRL2 code. This requires cmake to be found on PATH to build the necessary components.

IDEs

The cc crate used to build the mCRL2 toolset unfortunately does not generate a compile_commands.json that IDEs typically use to provide IDE support for C++ programs. There is a third-party tool called bear that can produce such a file for Rust projects, including ones that build internal C libraries. From a fresh cargo clean it can generate the necessary file by running the following command from this directory:

bear -- cargo build

It is also convenient to open the current directory directly in vscode since opening the root directory can make it confused by the different workspaces.

Caching

The cc crate does not support incremental compilation for all targets. Since the C++ code is slow to compile due to the heavy usage of templated code in header files it can be useful to install sccache with cargo install sccache and define the RUSTC_WRAPPER=sccache environment variable. This can be put into .bashrc for a more permanent solution. This cache will speed up both Rust and C++ compilation.