Commit e0b0748c authored by MEVEL Glen's avatar MEVEL Glen
Browse files

Add instructions for installing TLC from source.

parent 30fbb97f
......@@ -5,18 +5,23 @@ The project is known to compile with:
* coq-iris dev.2018-11-01.3.19aae59a (development version of Iris)
* coq-tlc 20181116 (for the proof of union-find)
As those dependencies (especially Iris) often make breaking changes,
compatibility with other versions is not guaranteed.
### Step 1: Install opam
_If opam is not already installed:_ See instructions [there][install-opam] to
install it; then:
opam init --comp=4.06.1
eval $(opam config env)
(This will create a `~/.opam` directory.)
_If opam is already installed:_ Create a new switch for the project:
opam switch -A 4.06.1 iris-time-proofs
eval $(opam config env)
### Step 2: Install Coq
......@@ -31,9 +36,6 @@ it as well:
### Step 3: Install a development version of Iris
Do _not_ install the latest development version, as this project does not
support it.
opam repo add iris-dev
opam update
opam pin add coq-iris -k version dev.2018-11-01.3.19aae59a
......@@ -50,6 +52,12 @@ available through an opam package in the Coq repository (added earlier).
opam pin add coq-tlc -k version 20181116
Alternatively, TLC can be installed from source:
git clone ''
( cd tlc && git checkout a7c9f61 )
opam pin add coq-tlc -k path ./tlc
## Compiling
To compile the Coq scripts:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment