Martin Constantino–Bodin authored 3 years ago and Björn Brandenburg committed 3 years ago

- add mathcomp-zify to esy
- Make esy work by having all the mathcomp packages
  install in the same place.

Martin Constantino–Bodin authored 3 years ago and Björn Brandenburg committed 3 years ago

`esy` is an `npm`-like package manager and build tool designed for
reproducibility, by preventing the use of unlisted dependencies and
pinning the exact version of each of these (a bit like `opam`, but
with more guarantees).

A nice feature of `esy` is ease of installation:

1. Install `esy` through `npm`. (However, note that `esy` is not a
   JavaScript program; the `esy` project just uses `npm` as a code
   hoster.

2. Run `esy` in the Prosa repository. 

This will download and compile all dependencies and compile the
repository. (On the flip side, this also means that Coq will be
compiled, so the first time, compilation will be slow.)

See the README.md file for usage instructions. 

See also the discussion: #80

For more information about `esy`, see: https://esy.sh/

No need to re-generate an unchanging file from scratch.

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.

An up-to-date version can always be generated with 'make html'.

First housekeeping steps...