Merge pull request #1153 from MetaCoq/metarocq-renaming

Coq -> Rocq, MetaCoq -> MetaRocq, TemplateCoq -> TemplateRocq renaming

Author: mattam82

.github/workflows/build.yml

@@ -1,4 +1,4 @@
-name: MetaCoq CI
+name: MetaRocq CI
 
 on:
   push:
@@ -24,7 +24,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '9.0+rc1'
+          - '9.0'
         ocaml_version:
           - '4.14-flambda'
           # - '4.09-flambda'
@@ -45,33 +45,26 @@ jobs:
       - name: Docker-Coq-Action
         uses: coq-community/docker-coq-action@v1
         with:
-          coq_version: ${{ 'dev' }}
+          coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
-          before_script: |
-            startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .  # <--
-              opam exec -- ocamlfind list
-            endGroup
           before_install: |
             startGroup "Print opam config"
-              sudo chown -R coq:coq .
               opam config list; opam repo list; opam list
-              opam remove -y rocq-core rocq-runtime rocq-stdlib rocq-prover coq-core coq-stdlib coqide-server coq-stdlib coq
-              opam pin remove -y rocq-core rocq-runtime rocq-stdlib rocq-prover coq-core coq-stdlib coqide-server coq-stdlib coq
-              opam pin remove -n dune
-              opam pin add -y coq 9.0+rc1
-              opam install -y coq.9.0+rc1
+            endGroup
+            startGroup "Workaround permission issue"
+              sudo chown -R 1000:1000 .
             endGroup
           script: |
             startGroup "Build project"
               opam exec -- ./configure.sh --enable-${{matrix.target}}
               opam exec -- make -j 2 ci-${{matrix.target}}
             endGroup
+          # Already done by the ci-opam target 
           uninstall: |
             startGroup "Clean project"
             endGroup
-
       - name: Revert permissions
         # to avoid a warning at cleanup time
         if: ${{ always() }}
         run: sudo chown -R 1001:116 .  # <--
+        

.gitignore

@@ -1,16 +1,16 @@
-metacoq-config
+metarocq-config
 .history
 docs/_site
 *.annot
-.coq_config
+.rocq_config
 *.cm*
 *.vo
 *.vok
 *.vos
 *.v.d
 *.glob
-Makefile.coq
-Makefile.coq.conf
+Makefile.rocq
+Makefile.rocq.conf
 \#*#
 *~
 .*.aux
@@ -30,75 +30,75 @@ _opam/
 erasure/src/*.ml
 erasure/src/*.mli
 
-template-coq/Ascii.ml
-template-coq/Ascii.mli
-template-coq/Ast0.ml
-template-coq/Ast0.mli
-template-coq/AstUtils.ml
-template-coq/AstUtils.mli
-template-coq/Basics.ml
-template-coq/Basics.mli
-template-coq/BinInt.ml
-template-coq/BinInt.mli
-template-coq/BinNat.ml
-template-coq/BinNat.mli
-template-coq/BinNums.ml
-template-coq/BinNums.mli
-template-coq/BinPos.ml
-template-coq/BinPos.mli
-template-coq/BinPosDef.ml
-template-coq/BinPosDef.mli
-template-coq/Bool.ml
-template-coq/Bool.mli
-template-coq/Checker0.ml
-template-coq/Checker0.mli
-template-coq/config0.ml
-template-coq/config0.mli
-template-coq/Datatypes.ml
-template-coq/Datatypes.mli
-template-coq/DecidableType.ml
-template-coq/DecidableType.mli
-template-coq/Decimal.ml
-template-coq/Decimal.mli
-template-coq/Equalities.ml
-template-coq/Equalities.mli
-template-coq/FMapWeakList.ml
-template-coq/FMapWeakList.mli
-template-coq/FSetWeakList.ml
-template-coq/FSetWeakList.mli
-template-coq/Induction.ml
-template-coq/Induction.mli
-template-coq/LiftSubst.ml
-template-coq/LiftSubst.mli
-template-coq/List0.ml
-template-coq/List0.mli
-template-coq/Logic.ml
-template-coq/Logic.mli
-template-coq/MSetWeakList.ml
-template-coq/MSetWeakList.mli
-template-coq/Makefile.conf
-template-coq/Nat0.ml
-template-coq/Nat0.mli
-template-coq/PeanoNat.ml
-template-coq/PeanoNat.mli
-template-coq/Specif.ml
-template-coq/Specif.mli
-template-coq/String0.ml
-template-coq/String0.mli
-template-coq/Typing0.ml
-template-coq/Typing0.mli
-template-coq/UnivSubst0.ml
-template-coq/UnivSubst0.mli
-template-coq/Wf.ml
-template-coq/Wf.mli
-template-coq/monad_utils.ml
-template-coq/monad_utils.mli
-template-coq/uGraph0.ml
-template-coq/uGraph0.mli
-template-coq/universes0.ml
-template-coq/universes0.mli
-template-coq/utils.ml
-template-coq/utils.mli
+template-rocq/Ascii.ml
+template-rocq/Ascii.mli
+template-rocq/Ast0.ml
+template-rocq/Ast0.mli
+template-rocq/AstUtils.ml
+template-rocq/AstUtils.mli
+template-rocq/Basics.ml
+template-rocq/Basics.mli
+template-rocq/BinInt.ml
+template-rocq/BinInt.mli
+template-rocq/BinNat.ml
+template-rocq/BinNat.mli
+template-rocq/BinNums.ml
+template-rocq/BinNums.mli
+template-rocq/BinPos.ml
+template-rocq/BinPos.mli
+template-rocq/BinPosDef.ml
+template-rocq/BinPosDef.mli
+template-rocq/Bool.ml
+template-rocq/Bool.mli
+template-rocq/Checker0.ml
+template-rocq/Checker0.mli
+template-rocq/config0.ml
+template-rocq/config0.mli
+template-rocq/Datatypes.ml
+template-rocq/Datatypes.mli
+template-rocq/DecidableType.ml
+template-rocq/DecidableType.mli
+template-rocq/Decimal.ml
+template-rocq/Decimal.mli
+template-rocq/Equalities.ml
+template-rocq/Equalities.mli
+template-rocq/FMapWeakList.ml
+template-rocq/FMapWeakList.mli
+template-rocq/FSetWeakList.ml
+template-rocq/FSetWeakList.mli
+template-rocq/Induction.ml
+template-rocq/Induction.mli
+template-rocq/LiftSubst.ml
+template-rocq/LiftSubst.mli
+template-rocq/List0.ml
+template-rocq/List0.mli
+template-rocq/Logic.ml
+template-rocq/Logic.mli
+template-rocq/MSetWeakList.ml
+template-rocq/MSetWeakList.mli
+template-rocq/Makefile.conf
+template-rocq/Nat0.ml
+template-rocq/Nat0.mli
+template-rocq/PeanoNat.ml
+template-rocq/PeanoNat.mli
+template-rocq/Specif.ml
+template-rocq/Specif.mli
+template-rocq/String0.ml
+template-rocq/String0.mli
+template-rocq/Typing0.ml
+template-rocq/Typing0.mli
+template-rocq/UnivSubst0.ml
+template-rocq/UnivSubst0.mli
+template-rocq/Wf.ml
+template-rocq/Wf.mli
+template-rocq/monad_utils.ml
+template-rocq/monad_utils.mli
+template-rocq/uGraph0.ml
+template-rocq/uGraph0.mli
+template-rocq/universes0.ml
+template-rocq/universes0.mli
+template-rocq/utils.ml
+template-rocq/utils.mli
 
 checker/src/ascii.ml
 checker/src/ascii.mli
@@ -223,9 +223,9 @@ checker/src/wf.mli
 /pcuic/src/pCUICNormal.mli
 /pcuic/src/pCUICPosition.ml
 /pcuic/src/pCUICPosition.mli
-/template-coq/theories/*.vio
-/template-coq/theories/kernel/*.vio
-/template-coq/theories/TemplateMonad/*.vio
+/template-rocq/theories/*.vio
+/template-rocq/theories/kernel/*.vio
+/template-rocq/theories/TemplateMonad/*.vio
 /pcuic/src/logic0.mli
 /pcuic/src/logic0.ml
 /pcuic/src/logic.mli
@@ -234,32 +234,32 @@ checker/src/wf.mli
 /pcuic/src/init.ml
 /pcuic/src/classes0.mli
 /pcuic/src/classes0.ml
-/checker/metacoq-config
-/template-coq/metacoq-config
-/common/metacoq-config
-/translations/metacoq-config
-/erasure/_CoqProject
+/checker/metarocq-config
+/template-rocq/metarocq-config
+/common/metarocq-config
+/translations/metarocq-config
+/erasure/_RocqProject
 /erasure/_PluginProject
-/erasure/metacoq-config
-/pcuic/_CoqProject
+/erasure/metarocq-config
+/pcuic/_RocqProject
 /pcuic/_PluginProject
-/pcuic/metacoq-config
-/checker/_CoqProject
-/safechecker/metacoq-config
+/pcuic/metarocq-config
+/checker/_RocqProject
+/safechecker/metarocq-config
 /safechecker/_PluginProject
-/safechecker/_CoqProject
-/template-coq/_CoqProject
-/template-coq/_PluginProject
-/template-coq/_TemplateCoqProject
-/common/_CoqProject
+/safechecker/_RocqProject
+/template-rocq/_RocqProject
+/template-rocq/_PluginProject
+/template-rocq/_TemplateRocqProject
+/common/_RocqProject
 /safechecker/Makefile.safechecker.conf
 /safechecker/Makefile.safechecker
 /safechecker/Makefile.plugin.conf
 /safechecker/Makefile.plugin
 /pcuic/src/signature.ml
 /pcuic/src/signature.mli
-/template-coq/Makefile.template
-/template-coq/Makefile.template.conf
+/template-rocq/Makefile.template
+/template-rocq/Makefile.template.conf
 /checker/_PluginProject
 /checker/Makefile.plugin.conf
 /checker/Makefile.plugin
@@ -287,20 +287,20 @@ pcuic/src/pCUICUtils.mli
 /_opam
 
 
-template-coq/gen-src/cRelationClasses.mli.rej
+template-rocq/gen-src/cRelationClasses.mli.rej
 .DS_Store
 
-/translations/_CoqProject
+/translations/_RocqProject
 test-suite/vs.mli
 test-suite/vs.ml
 test-suite/myMain.mli
 test-suite/myMain.ml
 test-suite/plugin-demo/Makefile.plugin
 
 
-template-coq/Makefile.plugin-e
-template-coq/Makefile.template-e
-template-coq/src/g_template_coq.ml
+template-rocq/Makefile.plugin-e
+template-rocq/Makefile.template-e
+template-rocq/src/g_template_coq.ml
 pcuic/Makefile.plugin-e
 erasure/Makefile.plugin-e
 safechecker/Makefile.plugin-e
@@ -315,12 +315,12 @@ _build/**
 extraction/src/*.ml
 extraction/src/*.mli
 test-suite/plugin-demo/Makefile.plugin
-template-coq/gen-src/cRelationClasses.mli.bak
-template-coq/gen-src/specFloat.ml.rej
+template-rocq/gen-src/cRelationClasses.mli.bak
+template-rocq/gen-src/specFloat.ml.rej
 
-bidirectional/CoqMakefile
+bidirectional/RocqMakefile
 
-bidirectional/CoqMakefile.conf
+bidirectional/RocqMakefile.conf
 
 bidirectional/.vscode/
 erasure/src/decidableType.ml
@@ -362,50 +362,54 @@ erasure/src/eEnvMap.mli
 erasure/src/eGlobalEnv.mli
 erasure/src/eGlobalEnv.ml
 Makefile.conf
-test-suite/plugin-demo/src/META.coq-metacoq-demo-plugin
-pcuic/src/META.coq-metacoq-pcuic
-examples/_CoqProject
-test-suite/_CoqProject
-quotation/metacoq-config
-examples/metacoq-config
-test-suite/metacoq-config
-test-suite/plugin-demo/_CoqProject
+test-suite/plugin-demo/src/META.rocq-metarocq-demo-plugin
+pcuic/src/META.rocq-metarocq-pcuic
+examples/_RocqProject
+test-suite/_RocqProject
+quotation/metarocq-config
+examples/metarocq-config
+test-suite/metarocq-config
+test-suite/plugin-demo/_RocqProject
 test-suite/plugin-demo/_PluginProject
-test-suite/plugin-demo/metacoq-config
+test-suite/plugin-demo/metarocq-config
 erasure/META
 safechecker/META
-template-coq/META
+template-rocq/META
 
 
 template-pcuic/demo.v
 template-pcuic/Makefile.local
-template-pcuic/_CoqProject
+template-pcuic/_RocqProject
 template-pcuic/Makefile.templatepcuic
 template-pcuic/Makefile.templatepcuic.conf
 
 quotation/Makefile.local
-quotation/_CoqProject
+quotation/_RocqProject
 quotation/Makefile.quotation
 quotation/Makefile.quotation.conf
 
-safechecker-plugin/metacoq-config
+safechecker-plugin/metarocq-config
 safechecker-plugin/demo.v
 safechecker-plugin/Makefile.local
-safechecker-plugin/_CoqProject
+safechecker-plugin/_RocqProject
 safechecker-plugin/_PluginProject
 safechecker-plugin/Makefile.safecheckerplugin
 safechecker-plugin/Makefile.safecheckerplugin.conf
 safechecker-plugin/Makefile.plugin
 safechecker-plugin/Makefile.plugin.conf
 
-erasure-plugin/metacoq-config
+erasure-plugin/metarocq-config
 erasure-plugin/demo.v
 erasure-plugin/Makefile.local
-erasure-plugin/_CoqProject
+erasure-plugin/_RocqProject
 erasure-plugin/_PluginProject
 erasure-plugin/Makefile.erasureplugin
 erasure-plugin/Makefile.erasureplugin.conf
 erasure-plugin/Makefile.plugin
 erasure-plugin/Makefile.plugin.conf
 erasure-plugin/META
 safechecker-plugin/META
+template-rocq/_TemplateRocqProject
+.gitignore
+template-rocq/_PluginProject
+template-rocq/_RocqProject