Skip to content

Commit

Permalink
Mention 8.20 in DOC.md and INSTALL.md (#1121)
Browse files Browse the repository at this point in the history
  • Loading branch information
yforster authored Nov 22, 2024
1 parent f251f2a commit 6e75b70
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 12 deletions.
12 changes: 4 additions & 8 deletions DOC.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@

## Branches and compatibility

**tl;dr** You should do your PRs against [coq-8.18](https://github.com/MetaCoq/metacoq/tree/coq-8.16).
**tl;dr** You should do your PRs against [coq-8.20](https://github.com/MetaCoq/metacoq/tree/coq-8.20).

Coq's kernel API is not stable yet, and changes there are reflected in MetaCoq's reified structures,
so we do not ensure any compatibility from version to version. There is one branch for each Coq version.

The *main branch* or *current branch* is the one which appers when you go on
[https://github.com/MetaCoq/metacoq](https://github.com/MetaCoq/metacoq).
Currently (unless you are reading the README of an outdated branch),
it is the [coq-8.16](https://github.com/MetaCoq/metacoq/tree/coq-8.16).
it is the [coq-8.20](https://github.com/MetaCoq/metacoq/tree/coq-8.20).
You should use it both for usage of MetaCoq and development of MetaCoq.

The [main](https://github.com/MetaCoq/metacoq/tree/main) branch is following Coq's master
Expand All @@ -21,10 +21,6 @@ stable release of Coq.
<!-- gets backports from `coq-8.11` when possible. Both `coq-8.11` and `coq-8.10` have associated -->
<!-- "alpha"-quality `opam` packages. -->

The branches [coq-8.17](https://github.com/MetaCoq/metacoq/tree/coq-8.17) and [coq-8.18](https://github.com/MetaCoq/metacoq/tree/coq-8.18) are being kept in sync.
The branches [coq-8.6](https://github.com/MetaCoq/metacoq/tree/coq-8.6) to [coq-8.15](https://github.com/MetaCoq/metacoq/tree/coq-8.16) are frozen.


## Program and Equations

MetaCoq relies on `Program` and `Equations` plugins, however try to avoid `Program` as it
Expand Down Expand Up @@ -89,7 +85,7 @@ a fresh level when `MetaCoq Strict Unquote Universe Mode` is off.

## Dependency graph between files

Generated on 2022/07/01, sources [there](https://github.com/MetaCoq/metacoq/tree/coq-8.16/dependency-graph).
Generated on 2022/07/01, sources [there](https://github.com/MetaCoq/metacoq/tree/coq-8.20/dependency-graph).

<center>
<img src="https://raw.githubusercontent.com/MetaCoq/metacoq.github.io/master/assets/depgraph-2022-07-01.png"
Expand All @@ -104,6 +100,6 @@ The file `README.md` in https://github.com/MetaCoq/metacoq.github.io is supposed
`README.md` in [https://github.com/MetaCoq/metacoq/](https://github.com/MetaCoq/metacoq/).

That's why we can't use relative links and have to use absolute ones.
E.g. [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.16/INSTALL.md) and not [INSTALL.md](INSTALL.md).
E.g. [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.20/INSTALL.md) and not [INSTALL.md](INSTALL.md).

Thus, when switching to a new default branch, we have to search and replace the old branch with the new one.
8 changes: 4 additions & 4 deletions INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +66,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.18 origin/coq-8.18
# git checkout -b coq-8.20 origin/coq-8.20
# git status

This checks that you are indeed on the `coq-8.18` branch.
This checks that you are indeed on the `coq-8.20` branch.

### Setting up an `opam` switch

Expand All @@ -78,10 +78,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.18 --packages="ocaml-variants.4.14.0+options,ocaml-option-flambda"
# opam switch create coq.8.20 --packages="ocaml-variants.4.14.0+options,ocaml-option-flambda"
# eval $(opam env)

This creates the `coq.8.18` switch which initially contains only the
This creates the `coq.8.20` 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`).

Expand Down

0 comments on commit 6e75b70

Please sign in to comment.