Skip to content
Snippets Groups Projects
Forked from Iris / lambda-rust
1144 commits behind the upstream repository.
Ralf Jung's avatar
Ralf Jung authored
New opam-based CI and build system

Submodules are gone. If you have opam set up, `make build-dep` will install the right version of everything.

This is *not* exactly what we discussed last week; I think I found something better. In particular, this approach lets us also figure out for historic lambdaRust versions, which commit of iris they needed. No magic branches in other repositories are needed, everything is local here.

Essentially, since the `opam` files do not support documenting detailed enough version information, I added a new file `opam.pins` that "enhances" the opam file appropriately. This file contains pins (one per line) that have to be set to compile lambdaRust. The script in `build/opam-pins.sh` applies those pins - and crucially, it does so recursively: When it finds a pin that is one of our git repositories, it will download the `opam.pins` files for *that* commit and also apply its pins. So if lambdaRust pins a particular commit of iris, and iris pins a particular commit of the prelude, then doing `make build-dep` in lambdaRust will follow this transitive chain and install the correct versions of iris and the prelude.

Cc @jjourdan @robbertkrebbers

See merge request !2
80da656e
History

LAMBDA-RUST COQ DEVELOPMENT

This is the Coq formalization of lambda-Rust.

Prerequisites

This version is known to compile with:

  • Coq 8.5pl3
  • Ssreflect 1.6
  • A development version of Iris

The easiest way to install the correct versions of the dependencies is through opam. Once you got opam set up, just run make build-dep to install the right versions of the dependencies.

Alternatively, you can manually determine the required Iris commit by consulting the opam.pins file.

Building Instructions

Run make to build the full development.