From 1f9ed654693675a512ff87b90d0ea855d63bd1a5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 20 Apr 2023 18:11:34 +0200 Subject: [PATCH] Update install instructions for Coq 8.17 --- INSTALL.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 1070c62e8..6225eb095 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -36,10 +36,10 @@ MetaCoq is split into multiple packages that get all installed using the - `coq-metacoq-erasure-plugin` for the extracted verifed erasure plugin - `coq-metacoq-translations` for example translations from type theory to type theory: e.g. variants of parametricity. - - `coq-metacoq-quotation` for a quotation library, allowing to + - `coq-metacoq-quotation` for a quotation library, allowing to quote MetaCoq terms and typing derivations as MetaCoq terms, with a work-in-progress proof of Löb's theorem. - + There are also `.dev` packages available in the `extra-dev` repository of Coq, to get those you will need to activate the following repositories: @@ -67,10 +67,10 @@ to have a dedicated `opam` switch (see below). To get the source code: # git clone https://github.com/MetaCoq/metacoq.git - # git checkout -b coq-8.16 origin/coq-8.16 + # git checkout -b coq-8.17 origin/coq-8.17 # git status -This checks that you are indeed on the `coq-8.16` branch. +This checks that you are indeed on the `coq-8.17` branch. ### Setting up an `opam` switch @@ -79,10 +79,10 @@ To setup a fresh `opam` installation, you might want to create a one yet. You need to use **opam 2** to obtain the right version of `Equations`. - # opam switch create coq.8.16 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda + # opam switch create coq.8.17 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda # eval $(opam env) -This creates the `coq.8.16` switch which initially contains only the +This creates the `coq.8.17` switch which initially contains only the basic `OCaml` `4.13.1` compiler with the `flambda` option enabled, and puts you in the right environment (check with `ocamlc -v`). @@ -109,8 +109,8 @@ the sources directory. Then use: - `make` to compile the `template-coq` plugin, the `pcuic` - development and the `safechecker` and `erasure` plugins, - along with the `test-suite`, `translations`, `examples` + development and the `safechecker` and `erasure` plugins, + along with the `test-suite`, `translations`, `examples` and `quotation` libraries. You can also selectively build each target. @@ -127,5 +127,5 @@ For faster development one can use: to construct the template-coq plugin. The `safechecker` and `erasure` ML plugins *cannot* be built using this mode. -- `make quick` is a synonymous for `make vos` with the addition of a global `Unset Universe Checking` option, i.e. +- `make quick` is a synonymous for `make vos` with the addition of a global `Unset Universe Checking` option, i.e. universes are not checked anywhere.