README.md 3.8 KB
Newer Older
1
# Coq-std++ [[coqdoc]](https://plv.mpi-sws.org/coqdoc/stdpp/)
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

This project contains an extended "Standard Library" for Coq called coq-std++.
The key features of this library are as follows:

- It provides a great number of definitions and lemmas for common data
  structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
  monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
  having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
  equality can be used as much as possible (for example, for maps we have
  `m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
  setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  `done` tactic for finishing trivial goals, a simple breadth-first solver
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20
  `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
  for proving compatibility of functions with respect to relations, and a solver
  `set_solver` for goals involving set operations.
Ralf Jung's avatar
Ralf Jung committed
21
- It is entirely dependency- and axiom-free.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23 24 25 26 27 28 29 30
## Side-effects

Importing std++ has some side effects as the library sets some global options.
Notably:

* `Generalizable All Variables`: This option enables implicit generalization in
  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
  also enables implicit generalization in `Instance`.  We think that the fact
Ralf Jung's avatar
Ralf Jung committed
31
  that both behaviors are coupled together is a
32 33 34
  [bug in Coq](https://github.com/coq/coq/issues/6030).
* The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
  `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
Ralf Jung's avatar
Ralf Jung committed
35
  [`base.v`](theories/base.v) for further details.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
* It blocks `simpl` on all operations involving integers `Z` (by setting
37
  `Arguments op : simpl never`). We do this because `simpl` tends to expose
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
39 40
  As a consequence of blocking `simpl`, due to
  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
  becomes unreliable. We do not consider this an issue since we use `lia` (for
  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
43

Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47
## Prerequisites

This version is known to compile with:

Ralf Jung's avatar
Ralf Jung committed
48
 - Coq version 8.8.2 / 8.9.1 / 8.10.2 / 8.11.2
Robbert Krebbers's avatar
Robbert Krebbers committed
49

Ralf Jung's avatar
Ralf Jung committed
50 51
## Installing via opam

Ralf Jung's avatar
Ralf Jung committed
52
To obtain the latest stable release via opam (2.0.0 or newer), you have to add
Ralf Jung's avatar
Ralf Jung committed
53
the Coq opam repository:
Ralf Jung's avatar
Ralf Jung committed
54

Ralf Jung's avatar
Ralf Jung committed
55
    opam repo add coq-released https://coq.inria.fr/opam/released
Ralf Jung's avatar
Ralf Jung committed
56 57 58

Then you can do `opam install coq-stdpp`.

Ralf Jung's avatar
Ralf Jung committed
59 60
To obtain a development version, add the Iris opam repository:

Ralf Jung's avatar
Ralf Jung committed
61
    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Ralf Jung's avatar
Ralf Jung committed
62

Ralf Jung's avatar
Ralf Jung committed
63
## Building from source
Robbert Krebbers's avatar
Robbert Krebbers committed
64

Ralf Jung's avatar
Ralf Jung committed
65 66
Run `make -jN` in this directory to build the library, where `N` is the number
of your CPU cores.  Then run `make install` to install the library.
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81

## Contributing to std++

If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/iris/stdpp/issues).  You will have to
create an account at the
[MPI-SWS GitLab](https://gitlab.mpi-sws.org/users/sign_in) (use the "Register"
tab).

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
[Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
changes in your fork, and create a merge request.

82 83 84 85 86
## Common problems

On Windows, differences in line endings may cause tests to fail. This can be 
fixed by setting Git's autocrlf option to true:

Ralf Jung's avatar
Ralf Jung committed
87
    git config --global core.autocrlf true