Support Coq 8.17 (AU-COBRA#225)

4ever2 · Apr 28, 2023 · 9b25224 · 9b25224
1 parent 980f08b
commit 9b25224
Show file tree

Hide file tree

Showing 37 changed files with 157 additions and 155 deletions.
diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
@@ -10,16 +10,15 @@ homepage: "https://github.com/AU-COBRA/ConCert"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
-  "coq" {= "8.16.1"}
-  "coq-bignums" {= "9.0.0+coq8.16"}
-  "coq-equations" {= "1.3+8.16"}
-  "coq-metacoq-common" {= "1.2+8.16"}
-  "coq-metacoq-erasure" {= "1.2+8.16"}
-  "coq-metacoq-pcuic" {= "1.2+8.16"}
-  "coq-metacoq-safechecker" {= "1.2+8.16"}
-  "coq-metacoq-template" {= "1.2+8.16"}
-  "coq-metacoq-template-pcuic" {= "1.2+8.16"}
-  "coq-metacoq-utils" {= "1.2+8.16"}
+  "coq" {= "8.17.0"}
+  "coq-bignums" {= "9.0.0+coq8.17"}
+  "coq-metacoq-common" {= "1.2+8.17"}
+  "coq-metacoq-erasure" {= "1.2+8.17"}
+  "coq-metacoq-pcuic" {= "1.2+8.17"}
+  "coq-metacoq-safechecker" {= "1.2+8.17"}
+  "coq-metacoq-template" {= "1.2+8.17"}
+  "coq-metacoq-template-pcuic" {= "1.2+8.17"}
+  "coq-metacoq-utils" {= "1.2+8.17"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-quickchick" {= "1.6.5"}
@@ -38,10 +37,10 @@ dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
 pin-depends: [
   [
     "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#61fd34d9f2fed705a860c33691642d3339681ea1"
+    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#f31a52ba2c1bddd42e9f9df8fca6c297ac359fae"
   ]
   [
     "coq-elm-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#1dc7fdb299db35960174f48d813b1ea61f7e396c"
+    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#0c0a733486f915162a194ee646d5f11d2ffc5cc0"
   ]
 ]
diff --git a/.github/coq-errors.json b/.github/coq-errors.json
@@ -17,4 +17,4 @@
             ]
         }
     ]
-}
+}
diff --git a/.github/opam-errors.json b/.github/opam-errors.json
@@ -18,4 +18,4 @@
             ]
         }
     ]
-}
+}
diff --git a/.github/workflows/lint-opam.yml b/.github/workflows/lint-opam.yml
@@ -15,7 +15,7 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: 4.13.x
-          opam-repositories: | 
+          opam-repositories: |
             coq-released: https://coq.inria.fr/opam/released
             default: https://opam.ocaml.org
       - name: Set up problem matcher

diff --git a/README.md b/README.md
@@ -14,7 +14,7 @@ ConCert can find real-world attacks as explained
 ## How to build
 
 
-Our development works with Coq 8.16 and depends on MetaCoq, std++, and coq-equations.
+Our development works with Coq 8.17 and depends on MetaCoq, and std++.
 The tests depend on QuickChick.
 The dependencies can be installed through `opam`.
 
@@ -27,7 +27,7 @@ opam switch create . 4.10.2 --repositories default,coq-released=https://coq.inri
 eval $(opam env)
 ```
 
-If Coq 8.16 is already installed, run
+If Coq 8.17 is already installed, run
 
 ```bash
 git clone https://github.com/AU-COBRA/ConCert.git
@@ -74,7 +74,7 @@ We use the standard Coqdoc with improved styles and scripts of [CoqdocJS](https:
   <br>
   <details>
     <summary>Cite paper</summary>
-    
+
     ```
     @article{annenkov_milo_nielsen_spitters_2022,
       author={ANNENKOV, DANIL and MILO, MIKKEL and NIELSEN, JAKOB BOTSCH and SPITTERS, BAS},
@@ -94,7 +94,7 @@ We use the standard Coqdoc with improved styles and scripts of [CoqdocJS](https:
   <br>
   <details>
     <summary>Cite paper</summary>
-    
+
     ```
     @InProceedings{milo_et_al:OASIcs.FMBC.2022.2,
       author =	{Milo, Mikkel and Nielsen, Eske Hoy and Annenkov, Danil and Spitters, Bas},
@@ -122,7 +122,7 @@ We use the standard Coqdoc with improved styles and scripts of [CoqdocJS](https:
   <br>
   <details>
     <summary>Cite paper</summary>
-    
+
     ```
     @inproceedings{10.1145/3573105.3575685,
         author = {Nielsen, Eske Hoy and Annenkov, Danil and Spitters, Bas},
@@ -243,7 +243,7 @@ We use the standard Coqdoc with improved styles and scripts of [CoqdocJS](https:
   <br>
   <details>
     <summary>Cite paper</summary>
-    
+
     ```
     @inproceedings{smart-contract-interactions,
       author    = {Jakob Botsch Nielsen and

diff --git a/coq-concert.opam b/coq-concert.opam
@@ -14,25 +14,24 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.16" & < "8.17~"}
+  "coq" {>= "8.17" & < "8.18~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "1.6.4" & <= "1.6.5"}
-  "coq-equations" {= "1.3+8.16"}
-  "coq-metacoq-utils" {= "1.2+8.16"}
-  "coq-metacoq-common" {= "1.2+8.16"}
-  "coq-metacoq-template" {= "1.2+8.16"}
-  "coq-metacoq-template-pcuic" {= "1.2+8.16"}
-  "coq-metacoq-pcuic" {= "1.2+8.16"}
-  "coq-metacoq-safechecker" {= "1.2+8.16"}
-  "coq-metacoq-erasure" {= "1.2+8.16"}
+  "coq-metacoq-utils" {= "1.2+8.17"}
+  "coq-metacoq-common" {= "1.2+8.17"}
+  "coq-metacoq-template" {= "1.2+8.17"}
+  "coq-metacoq-template-pcuic" {= "1.2+8.17"}
+  "coq-metacoq-pcuic" {= "1.2+8.17"}
+  "coq-metacoq-safechecker" {= "1.2+8.17"}
+  "coq-metacoq-erasure" {= "1.2+8.17"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
   "coq-stdpp" {>= "1.6.0" & <= "1.8.0"}
 ]
 
 pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#61fd34d9f2fed705a860c33691642d3339681ea1"]
-  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#1dc7fdb299db35960174f48d813b1ea61f7e396c"]
+  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#f31a52ba2c1bddd42e9f9df8fca6c297ac359fae"]
+  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#0c0a733486f915162a194ee646d5f11d2ffc5cc0"]
 ]
 
 build: [

diff --git a/embedding/examples/AcornExamples.v b/embedding/examples/AcornExamples.v
@@ -35,7 +35,7 @@ Module AcornBool.
                     (eCase ("Bool", [])
                            (tyInd "Bool")
                            (eRel 0)
-                           [(pConstr "True_coq" [], eConstr "Bool" "False_coq"); 
+                           [(pConstr "True_coq" [], eConstr "Bool" "False_coq");
                             (pConstr "False_coq" [], eConstr "Bool" "True_coq")]))].
 
   MetaCoq Run (translateData [] Data).
@@ -48,12 +48,12 @@ End AcornBool.
 Module AcornMaybe.
   MetaCoq Run define_mod_prefix.
 
-  Definition Data := [gdInd "Maybe" 1 [("Nothing_coq", []); 
+  Definition Data := [gdInd "Maybe" 1 [("Nothing_coq", []);
                                        ("Just_coq", [(None, tyRel 0)])] false].
   (*---------------------*)
   Definition Functions := [
     ("isJust", eTyLam "A"
-                (eLambda "x" 
+                (eLambda "x"
                   (tyApp (tyInd "Maybe") (tyRel 0))
                   (eCase ("Maybe",[tyRel 0])
                     (tyInd "Bool")
@@ -78,7 +78,7 @@ Module AcornProd.
   Definition Functions :=
     [("fst", eTyLam "A"
               (eTyLam "A"
-                (eLambda "x" 
+                (eLambda "x"
                   (tyApp (tyApp (tyInd "Pair") (tyRel 1)) (tyRel 0))
                   (eCase ("Pair",[(tyRel 1); (tyRel 0)])
                     (tyRel 1)
@@ -535,7 +535,7 @@ Module AcornBlochain.
           (tyInd "string")
           (eRel 0)
           [(pConstr "InitContext_coq" ["x0"; "x1"], eRel 0)]))
-    ; ("initChain", eLambda "x" 
+    ; ("initChain", eLambda "x"
         (tyInd "InitContext")
         (eCase
           ("InitContext", [])

diff --git a/embedding/theories/Misc.v b/embedding/theories/Misc.v
@@ -68,7 +68,8 @@ Lemma forallb_In {A} x (xs : list A) p :
 Proof.
   revert x.
   induction xs; intros x Hin Hfa; auto.
-  simpl in *. propify; intuition; subst; auto.
+  simpl in *. propify.
+  now destruct_or_hyps.
 Qed.
 
 

diff --git a/embedding/theories/pcuic/PCUICCorrectness.v b/embedding/theories/pcuic/PCUICCorrectness.v
@@ -21,7 +21,6 @@ From Coq Require Import Basics.
 From Coq Require Import Lia.
 From Coq Require Import ssrbool.
 From Coq Require Import Arith.
-From Equations Require Import Equations.
 
 Import ListNotations.
 Import NamelessSubst.
-Original file line number
+Diff line change
@@ Expand Up / @@ -17,4 +17,4 @@ @@
                 ]
             }
         ]
-    }
+    }