Rocq renaming

.github/dependabot.yml

@@ -17,6 +17,22 @@ updates:
       interval: "daily"
     labels:
       - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.20"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.19"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
   - package-ecosystem: "github-actions"
     directory: "/"
     target-branch: "coq-8.18"

.nix/coq-overlays/equations/default.nix

@@ -63,5 +63,5 @@ with lib; (mkCoqDerivation {
     maintainers = with maintainers; [ jwiegley ];
   };
 }).overrideAttrs (o: {
-  preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
+  preBuild = "rocq makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
 })

.vscode/metacoq.code-workspace

@@ -7,7 +7,7 @@
 	"settings": {
 
 	// A list of arguments to send to coqtop. Use seperate elements instead of spaces to seperate each argument, especially when a flag expects another trailing argument, e.g. `["-I","./bin"]` instead of `["-I ./bin"]`
-        "coqtop.args": [
+	"coqtop.args": [
 		// "-bt", // get backtraces from Coq on errors
 		"-R", "utils/theories", "MetaCoq.Utils",
 		"-R", "common/theories", "MetaCoq.Common",
@@ -90,7 +90,6 @@
 	    ],
 	 // When enabled, will trim trailing whitespace when saving a file.
 	"files.trimTrailingWhitespace": true,
-	"coqtop.binPath": "_opam/bin",
 	"vscoq.path": "_opam/bin/vscoqtop",
 	"coq-lsp.path": "_opam/bin/coq-lsp",
 	"files.exclude": {
@@ -107,5 +106,8 @@
 		"**/Thumbs.db": true
 	},
 	"coq-lsp.check_only_on_request": true,
+	"coqtop.binPath": "_opam/bin",
+	"coqtop.coqtopExe": "coqtop",
+	"coqtop.coqidetopExe": "coqidetop",
   }
 }

DOC.md

@@ -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
@@ -21,18 +21,14 @@ 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
 inserts some JMeq and UIP axioms silently, whereas we try to keep the development axiom-free.
 You can use `Equations` to do some dependent induction (`dependent induction`,
 `dependent destruction`, `depelim`). You may need to add:
 ```
-Require Import Equations.Prop.DepElim.
+From Equations.Prop Require Import DepElim.
 ```
 
 ## ident vs. qualid. vs kername
@@ -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"
@@ -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.

INSTALL.md

@@ -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
 
@@ -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`).
 

Makefile

@@ -5,7 +5,7 @@ all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker
 
 ifeq '$(METACOQ_CONFIG)' 'local'
   ifeq ($(shell which cygpath 2>/dev/null),)
-  OCAMLPATH := $(shell pwd)/template-coq/:$(OCAMLPATH)
+  OCAMLPATH := $(shell pwd)/template-coq/:$(shell pwd)/safechecker-plugin/src:$(shell pwd)/erasure-plugin/src:$(OCAMLPATH)
   else
   OCAMLPATH := $(shell cygpath -m `pwd`)/template-coq/;$(OCAMLPATH)
   endif

common/Makefile

@@ -25,7 +25,7 @@ mrproper:
 	rm -f Makefile.coq
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+	rocq makefile -f _CoqProject -o Makefile.coq
 
 .merlin: Makefile.coq
 	$(MAKE) -f $< $@

common/theories/BasicAst.v

@@ -1,8 +1,8 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Morphisms Orders Setoid.
+From Stdlib Require Import ssreflect Morphisms Orders Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Export Kernames.
-From Coq Require Floats.SpecFloat.
+From Stdlib Require Floats.SpecFloat.
 From Equations Require Import Equations.
 
 (** Identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax). *)

common/theories/EnvMap.v

@@ -1,6 +1,6 @@
 
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect RelationClasses OrderedTypeAlt FMapAVL FMapFacts.
+From Stdlib Require Import ssreflect RelationClasses OrderedTypeAlt FMapAVL FMapFacts.
 From MetaCoq.Utils Require Import utils String2pos CanonicalTries.
 From MetaCoq.Common Require Import config uGraph Reflect BasicAst Kernames.
 From Equations Require Import Equations.

common/theories/Environment.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes.
 From Equations.Prop Require Import Classes EqDecInstances.
@@ -218,7 +218,7 @@ Module Environment (T : Term).
        decl_body := decl_body x;
        decl_type := decl_type x |}.
 
-  (** Count the number of assumptions in a context (i.e. declarations that do not 
+  (** Count the number of assumptions in a context (i.e. declarations that do not
       contain a body). *)
   Fixpoint context_assumptions (Γ : context) : nat :=
     match Γ with
@@ -327,7 +327,7 @@ Module Environment (T : Term).
         `ind_bodies ,,, ind_params ,,, cstr_args |- cstr_indices`. *)
     cstr_indices : list term;
     (** Full type of the constructor, which can depend on the inductives in the same block :
-        `ind_bodies |- cstr_type`. This should be equal to 
+        `ind_bodies |- cstr_type`. This should be equal to
         `forall ind_params cstr_args, I ind_params cstr_indices` *)
     cstr_type : term;
     (** Number of arguments of the constructor, _without_ let-in arguments and _without_ parameters.
@@ -341,7 +341,7 @@ Module Environment (T : Term).
     proj_name : ident;
     (** Relevance of the projection. *)
     proj_relevance : relevance;
-    (** Type of the projection, wich can depend on the parameters of the inductive 
+    (** Type of the projection, wich can depend on the parameters of the inductive
         and on the object we are projecting from : `ind_params ,,, x |- proj_type`. *)
     proj_type : term;
   }.
@@ -365,21 +365,21 @@ Module Environment (T : Term).
   (** Data associated to a single inductive in a mutual inductive block. *)
   Record one_inductive_body := {
     (** Name of the inductive, without the module path. *)
-    ind_name : ident; 
+    ind_name : ident;
     (** Indices of the inductive, which can depend on the parameters :
         `ind_params |- ind_indices`. *)
     ind_indices : context;
-    (** Sort of the inductive. *) 
-    ind_sort : Sort.t; 
+    (** Sort of the inductive. *)
+    ind_sort : Sort.t;
     (** Full type of the inductive. This should be equal to
         `forall ind_params ind_indices, tSort ind_sort` *)
-    ind_type : term; 
+    ind_type : term;
     (** Allowed eliminations for the inductive. *)
-    ind_kelim : allowed_eliminations; 
+    ind_kelim : allowed_eliminations;
     (** Constructors of the inductive. Order is important. *)
     ind_ctors : list constructor_body;
     (** Names and types of primitive projections, if any. *)
-    ind_projs : list projection_body; 
+    ind_projs : list projection_body;
     (** Relevance of the inductive. *)
     ind_relevance : relevance }.
 

common/theories/EnvironmentReflect.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun Morphisms Setoid.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Primitive Universes Environment Reflect.
 From Equations.Prop Require Import Classes EqDecInstances.

common/theories/EnvironmentTyping.v

@@ -1,6 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect ssrbool.
-From Coq Require CMorphisms CRelationClasses.
+From Stdlib Require Import ssreflect ssrbool.
+From Stdlib Require CMorphisms CRelationClasses.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config BasicAst Universes Environment Primitive.
 From Equations Require Import Equations.

common/theories/Kernames.v

@@ -1,8 +1,8 @@
 
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Lia MSetList OrderedTypeAlt OrderedTypeEx FMapAVL FMapFacts MSetAVL MSetFacts MSetProperties.
+From Stdlib Require Import Lia MSetList OrderedTypeAlt OrderedTypeEx FMapAVL FMapFacts MSetAVL MSetFacts MSetProperties.
 From MetaCoq.Utils Require Import utils MCMSets MCFSets.
-From Coq Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 From Equations Require Import Equations.
 
 Local Open Scope string_scope2.

common/theories/Primitive.v

@@ -1,6 +1,6 @@
 (* Primitive types *)
 
-From Coq Require Import Uint63 PrimFloat SpecFloat FloatOps ZArith HexadecimalString.
+From Stdlib Require Import Uint63 PrimFloat SpecFloat FloatOps ZArith HexadecimalString.
 From MetaCoq.Utils Require Import bytestring MCString.
 Local Open Scope bs.
 

common/theories/Reflect.v

@@ -1,9 +1,9 @@
 (* Distributed under the terms of the MIT license. *)
 (* For primitive integers and floats  *)
-From Coq Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
+From Stdlib Require Numbers.Cyclic.Int63.Uint63 Floats.PrimFloat Floats.FloatAxioms.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Universes Kernames.
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 From Equations Require Import Equations.
 
 #[program,global] Instance reflect_prim_int : ReflectEq Numbers.Cyclic.Int63.Uint63.int :=
@@ -260,7 +260,7 @@ Proof.
   f_equal. apply uip.
 Qed.
 
-Require Import RelationClasses.
+From Stdlib Require Import RelationClasses.
 
 Lemma constraint_lt_irrel (x y : UnivConstraint.t) (l l' : UnivConstraint.lt_ x y) : l = l'.
 Proof.

common/theories/Transform.v

@@ -3,7 +3,7 @@
 (** Generic transofmations from one language to another,
     preserving an evaluation relation up-to some observational equality. *)
 
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 Import bytestring.

common/theories/Universes.v

@@ -1,8 +1,8 @@
-From Coq Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
+From Stdlib Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils MCMSets MCFSets.
 From MetaCoq.Common Require Import BasicAst config.
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Local Open Scope nat_scope.
 Local Open Scope string_scope2.

common/theories/UniversesDec.v

@@ -1,4 +1,4 @@
-From Coq Require Import PArith NArith ZArith Lia.
+From Stdlib Require Import PArith NArith ZArith Lia.
 From MetaCoq.Utils Require Import MCList MCOption MCUtils.
 From MetaCoq.Common Require Import uGraph.
 From MetaCoq.Common Require Import Universes.

common/theories/uGraph.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-Require Import ssreflect ssrbool OrderedTypeAlt MSetAVL MSetFacts MSetProperties MSetDecide Morphisms.
+From Stdlib Require Import ssreflect ssrbool OrderedTypeAlt MSetAVL MSetFacts MSetProperties MSetDecide Morphisms.
 From MetaCoq.Utils Require Import utils wGraph.
 From MetaCoq.Common Require Import config Universes.
 From Equations.Prop Require Import DepElim.
@@ -3079,7 +3079,7 @@ Proof.
 Qed.
 
 
-Require Import SetoidTactics.
+From Stdlib Require Import SetoidTactics.
 
 #[global] Instance is_graph_of_uctx_proper {cf : checker_flags} G : Proper ((=_cs) ==> iff) (is_graph_of_uctx G).
 Proof.

configure.sh

@@ -8,11 +8,9 @@ make -f Makefile mrproper
 # should already be available in $(COQMF_LIB)/user-contrib/MetaCoq/*
 # For local builds, we set specific dependencies of each subproject in */metacoq-config
 
-# CWD=`pwd`
-
-if command -v coqc >/dev/null 2>&1
+if command -v rocq >/dev/null 2>&1
 then
-    COQLIB=` coqc -where | tr -d '\r' | tr '\\\\' '/'`
+    COQLIB=` rocq c -where | tr -d '\r' | tr '\\\\' '/'`
 
     if [[ "$1" = "local" ]] || [[ "$1" = "--enable-local" ]] || [[ "$1" = "--enable-quick" ]]
     then
@@ -78,5 +76,5 @@ then
     echo ${PLUGIN_DEMO_DEPS} >> test-suite/plugin-demo/metacoq-config
 
 else
-    echo "Error: coqc not found in path"
+    echo "Error: rocq not found in path"
 fi

erasure-plugin/Makefile

@@ -9,12 +9,12 @@ _CoqProject: _CoqProject.in metacoq-config
 	cat _CoqProject.in >> _CoqProject
 
 Makefile.plugin: _PluginProject
-	coq_makefile -f _PluginProject -o Makefile.plugin $(DEPS)
+	rocq makefile -f _PluginProject -o Makefile.plugin $(DEPS)
 # Avoid conflicting dependency file creation for the template plugin
 	sed -e s/coqdeps/coqdeps.plugin/g Makefile.plugin > Makefile.plugin.tmp && mv -f Makefile.plugin.tmp Makefile.plugin
 
 Makefile.erasureplugin: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.erasureplugin $(DEPS)
+	rocq makefile -f _CoqProject -o Makefile.erasureplugin $(DEPS)
 
 theory: Makefile.erasureplugin
 	$(MAKE) -f Makefile.erasureplugin

erasure-plugin/clean_extraction.sh

@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+SED=`which gsed || which sed`
+
 echo "Cleaning result of extraction"
 
 if [ ! -d "src" ]
@@ -9,7 +11,7 @@ fi
 
 shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
-files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | ${SED} -e s/gen-src/src/`
 
 if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]

erasure-plugin/theories/ETransform.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Program ssreflect ssrbool.
+From Stdlib Require Import Program ssreflect ssrbool.
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import Environment Transform config BasicAst uGraph.