This project is part of the Iris Masterplan. It aims at verifying OCaml 5 programs, including lockfree algorithms from Saturn and a work-stealing scheduler based on Domainslib.
Assuming that you have opam (>= 2.0) installed, run the following commands, which create a local opam switch, install dependencies and compile Coq proofs:
opam update --all --repositories
opam switch create . --yes --deps-only --repos default,coq-released=https://coq.inria.fr/opam/released,iris-dev=git+https://gitlab.mpi-sws.org/iris/opam.git
eval $(opam env --switch=. --set-switch)
make