From 9f126450eeddeb788713934ad1846de12c70852a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Jun 2018 10:19:36 +0200
Subject: [PATCH] improve README structure
---
README.md | 22 ++++++++++++++++++----
1 file changed, 18 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index 9453e1e25..99bde15e5 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,9 @@
This is the Coq development of the [Iris Project](http://iris-project.org), in
the MoSeL version.
-## Prerequisites
+## Building Iris
+
+### Prerequisites
This version is known to compile with:
@@ -15,7 +17,7 @@ For a version compatible with Coq 8.6, have a look at the
If you need to work with Coq 8.5, please check out the
[iris-3.0 branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/iris-3.0).
-## Installing via opam
+### Installing via opam
To obtain the latest stable release via opam (1.2.2 or newer), you have to add
the Coq opam repository:
@@ -28,7 +30,7 @@ To obtain a development version, add the Iris opam repository:
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
-## Building from source
+### Building from source
When building Iris from source, we recommend to use opam (1.2.2 or newer) for
installing Iris's dependencies. This requires the following two repositories:
@@ -98,7 +100,9 @@ that should be compatible with this version:
* [Iris Atomic](https://gitlab.mpi-sws.org/FP/iris-atomic/) is an experimental
formalization of logically atomic triples in Iris.
-## For Developers: How to update the std++ dependency
+## Notes for Iris Developers
+
+### How to update the std++ dependency
* Do the change in std++, push it.
* Wait for CI to publish a new std++ version on the opam archive, then run
@@ -107,3 +111,13 @@ that should be compatible with this version:
* Run `make build-dep` (in Iris) to install the new version of std++.
You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
+
+### How to write/update test cases
+
+The files in `tests/` are test cases. Each of the `.v` files comes with a
+matching `.ref` file containing the expected output of `coqc`. Adding `Show.`
+in selected places in the proofs makes `coqc` print the current goal state.
+This is used to make sure the proof mode prints goals and reduces terms the way
+we expect it to. You can run `make ref` to re-generate all the `.ref` files;
+this is useful after adding or removing `Show.` from a test. If you do this,
+make sure to check the diff for any unexpected changes in the output!
--
GitLab