Newer
Older
Discussion about the Iris Coq development happens on the mailing list
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club) and
in the [Iris Chat](https://mattermost.mpi-sws.org/iris). This is also the right
place to ask questions. The chat requires an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
Ralf Jung
committed
tab). If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/FP/iris-coq/issues), which also
Ralf Jung
committed
requires an MPI-SWS GitLab account.
Below, you can find some useful resources and an FAQ.
* Information on how to set up your editor for unicode input and output is
collected in [Editor.md](Editor.md).
* The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
* Naming conventions are documented at [Naming.md](Naming.md).
## How to submit a pull request
To contribute code, please send your MPI-SWS GitLab username to
[Ralf Jung](https://gitlab.mpi-sws.org/jung) to enable personal projects for
your account. Then you can fork the
[Iris git repository](https://gitlab.mpi-sws.org/FP/iris-coq/), make your
Ralf Jung
committed
changes in your fork, and create a merge request. Please do *not* use the
master branch of your fork, that might confuse CI. Use a feature branch
instead.
## 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
`opam update iris-dev`.
* In Iris, change the `opam` file to depend on the new 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=1 make` 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!
Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
Coq-8.8-specific `.ref` file). If you change one of these, remember to update
*all* the `.ref` files.