From df371dc50579eceda4fdfb0c8944e4347a0d1cf6 Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Wed, 20 Jan 2021 14:38:54 +0100 Subject: [PATCH] Replace 8.12 in all files with 8.13 --- DOC.md | 10 +++++----- INSTALL.md | 8 ++++---- README.md | 28 ++++++++++++++-------------- coq-metacoq-template.opam | 2 +- 4 files changed, 24 insertions(+), 24 deletions(-) diff --git a/DOC.md b/DOC.md index 0b0d20c6e..873c18648 100644 --- a/DOC.md +++ b/DOC.md @@ -13,19 +13,19 @@ The *main branch* or *current branch* is the one which appers when you go on Currently (unless you are reading the README of an outdated branch), it is the [coq-8.11](https://github.com/MetaCoq/metacoq/tree/coq-8.11). You should use it both for usage of MetaCoq and development of MetaCoq. -We should move soon to [coq-8.12](https://github.com/MetaCoq/metacoq/tree/coq-8.12). +We should move soon to [coq-8.13](https://github.com/MetaCoq/metacoq/tree/coq-8.12). The [master](https://github.com/MetaCoq/metacoq/tree/master) branch is following Coq's master branch and gets regular updates from the the main development branch which follows the latest stable release of Coq. -The branch [coq-8.10](https://github.com/MetaCoq/metacoq/tree/coq-8.10) -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.6](https://github.com/MetaCoq/metacoq/tree/coq-8.6), [coq-8.7](https://github.com/MetaCoq/metacoq/tree/coq-8.7), [coq-8.8](https://github.com/MetaCoq/metacoq/tree/coq-8.8) -and [coq-8.9](https://github.com/MetaCoq/metacoq/tree/coq-8.9) are frozen. +and [coq-8.9](https://github.com/MetaCoq/metacoq/tree/coq-8.9), and [coq-8.10](https://github.com/MetaCoq/metacoq/tree/coq-8.10) are frozen. diff --git a/INSTALL.md b/INSTALL.md index f007ab5e5..f0c9f6938 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -61,10 +61,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.12 origin/coq-8.12 + # git checkout -b coq-8.13 origin/coq-8.13 # git status -This checks that you are indeed on the `coq-8.12` branch. +This checks that you are indeed on the `coq-8.13` branch. ### Setting up an `opam` switch @@ -73,10 +73,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.12 4.07.1 + # opam switch create coq.8.13 4.07.1 # eval $(opam env) -This creates the `coq.8.12` switch which initially contains only the +This creates the `coq.8.13` switch which initially contains only the basic `OCaml` `4.07.1` compiler, and puts you in the right environment (check with `ocamlc -v`). diff --git a/README.md b/README.md index 4f6225cb8..2daec5930 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ MetaCoq

-[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.12)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com) +[![Build status](https://github.com/MetaCoq/metacoq/workflows/Test%20compilation/badge.svg?branch=coq-8.13)](https://github.com/MetaCoq/metacoq/actions) [![MetaCoq Chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com) MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins @@ -24,7 +24,7 @@ manipulating Coq terms and developing certified plugins ## Getting started -- You may want to start with a [demo](https://github.com/MetaCoq/metacoq/tree/coq-8.12/examples/demo.v). +- You may want to start with a [demo](https://github.com/MetaCoq/metacoq/tree/coq-8.13/examples/demo.v). - The current branch [documentation (as light coqdoc files)](https://metacoq.github.io/html/toc.html). @@ -34,13 +34,13 @@ manipulating Coq terms and developing certified plugins ## Installation instructions -See [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.12/INSTALL.md) +See [INSTALL.md](https://github.com/MetaCoq/metacoq/tree/coq-8.13/INSTALL.md) ## Documentation -See [DOC.md](https://github.com/MetaCoq/metacoq/tree/coq-8.12/DOC.md) +See [DOC.md](https://github.com/MetaCoq/metacoq/tree/coq-8.13/DOC.md) @@ -50,7 +50,7 @@ At the center of this project is the Template-Coq quoting library for Coq. The project currently has a single repository extending Template-Coq with additional features. Each extension is in dedicated folder. -### [Template-Coq](https://github.com/MetaCoq/metacoq/tree/coq-8.12/template-coq) +### [Template-Coq](https://github.com/MetaCoq/metacoq/tree/coq-8.13/template-coq) Template-Coq is a quoting library for [Coq](http://coq.inria.fr). It takes `Coq` terms and constructs a representation of their syntax tree as @@ -92,7 +92,7 @@ calculus has proofs of standard metatheoretical results: that singleton elimination (from Prop to Type) is only allowed on singleton inductives in Prop. -### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.12/safechecker) +### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.13/safechecker) Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of @@ -109,7 +109,7 @@ type-checker, one can use: MetaCoq CoqCheck -### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.12/erasure) +### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.13/erasure) An erasure procedure to untyped lambda-calculus accomplishing the same as the Extraction plugin of Coq. The extracted safe erasure is @@ -120,22 +120,22 @@ available in Coq through a new vernacular command: After importing `MetaCoq.Erasure.Loader`. -### [Translations](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations) +### [Translations](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations) Examples of translations built on top of this: -- a parametricity plugin in [translations/param_original.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations/param_original.v) +- a parametricity plugin in [translations/param_original.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations/param_original.v) -- a plugin to negate funext in [translations/times_bool_fun.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/translations/times_bool_fun.v) +- a plugin to negate funext in [translations/times_bool_fun.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/translations/times_bool_fun.v) ### Examples - An example Coq plugin built on the Template Monad, which can be used to - add a constructor to any inductive type is in [examples/add_constructor.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/examples/add_constructor.v) + add a constructor to any inductive type is in [examples/add_constructor.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/examples/add_constructor.v) -- The test-suite files [test-suite/erasure_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/test-suite/erasure_test.v) - and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.12/test-suite/safechecker_test.v) show example +- The test-suite files [test-suite/erasure_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/test-suite/erasure_test.v) + and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.13/test-suite/safechecker_test.v) show example uses (and current limitations of) the verified checker and erasure. @@ -227,7 +227,7 @@ Copyright (c) 2018-2020 Danil Annenkov, Yannick Forster, Théo Winterhalter ``` This software is distributed under the terms of the MIT license. -See [LICENSE](https://github.com/MetaCoq/metacoq/tree/coq-8.12/LICENSE) for details. +See [LICENSE](https://github.com/MetaCoq/metacoq/tree/coq-8.13/LICENSE) for details. diff --git a/coq-metacoq-template.opam b/coq-metacoq-template.opam index 6753eda4b..3ab7e7853 100644 --- a/coq-metacoq-template.opam +++ b/coq-metacoq-template.opam @@ -1,7 +1,7 @@ opam-version: "2.0" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.12" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.13" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand " "Simon Boulier "