chore(upgrade) Ergo compiler code switched to Coq 8.12

Signed-off-by: Jerome Simeon <[email protected]>

.circleci/config.yml

@@ -43,12 +43,12 @@ common_steps: &common_steps
     - run:
         name: "Install Coq"
         command: |
-          opam install -y -v coq.8.8.2 coq-flocq coq-jsast
+          opam install -y -v coq.8.12.0 coq-flocq coq-jsast
         no_output_timeout: 30m
     - run:
         name: "Install Q*cert"
         command: |
-          opam install -y -v coq-qcert.2.0.0
+          opam install -y -v coq-qcert.2.1.0
         no_output_timeout: 30m
     - save_cache:
         <<: *common_cache_key

.gitignore

@@ -18,9 +18,13 @@ Makefile.config
 *~
 .#*
 *.vo
+*.vos
+*.vok
 *.v.d
 *.glob
 *.aux
+*.lia.cache
+.Makefile.coq.d
 *.ctoj
 .DS_Store
 _CoqProject
@@ -48,4 +52,3 @@ thumbs.db
 # generated by dune
 *.merlin
 *.install
-

Makefile.config

@@ -13,4 +13,4 @@
 #
 
 ## Qcert compiler location
-#QCERT=../qcert-master
+QCERT=../qcert-master

compiler/core/Backend/Qcert/QcertData.v

@@ -109,7 +109,7 @@ Definition onddateTime {A} (f : DATE_TIME -> A) (d : data) : option A :=
 
 Definition lift_dateTimeList (l:list data) : option (list DATE_TIME) :=
   lift_map
-    (fun d =>
+    (fun d : data =>
        match d with
        | dforeign (enhanceddateTime fd) => Some fd
        | _ => None
@@ -512,7 +512,6 @@ Next Obligation.
   - destruct m; simpl in H;
       unfold ondfloat2, lift in H
       ; destruct d1; simpl in H; try discriminate
-      ; destruct f; simpl in H; try discriminate
       ; destruct d2; simpl in H; try discriminate
       ; try (destruct f; simpl in H; try discriminate)
       ; invcs H

compiler/core/Backend/Qcert/QcertEJson.v

@@ -413,7 +413,7 @@ Definition enhanced_ejson_date_time_runtime_op_interp op (dl:list ejson) : optio
          end) dl
   | EJsonRuntimeDateTimeDurationAmount =>
     apply_unary
-      (fun d =>
+      (fun d : ejson =>
          match d with
          | ejforeign (enhanceddateTimeduration fd) =>
            Some (ejbigint (DATE_TIME_DURATION_amount fd))

compiler/core/Backend/Qcert/QcertType.v

@@ -111,7 +111,7 @@ Proof.
     inversion H; inversion H0; congruence.
 Qed.
 
-Instance enhanced_type_lattice : Lattice enhanced_type eq
+#[refine] Instance enhanced_type_lattice : Lattice enhanced_type eq
   := {
       join := enhanced_type_join
       ; meet := enhanced_type_meet

compiler/core/Common/PrintTypedData.v

@@ -62,7 +62,7 @@ Section PrintTypedData.
       | _ => None
       end.
 
-    Definition fmt_nl := String.String (ascii_of_N 10) EmptyString.
+    Definition fmt_nl := String.String (ascii_of_nat 10) EmptyString.
     Definition fmt_dq := """".
 
     Definition js_quote_char (a:ascii) : string

compiler/core/Compiler/ErgoCompiler.v

@@ -12,8 +12,9 @@
  * limitations under the License.
  *)
 
-Require String.
-Require Qcert.Brands.BrandRelation.
+Require Import String.
+Require Import ZArith.
+Require Import Qcert.Brands.BrandRelation.
 
 Require ErgoSpec.Version.
 Require ErgoSpec.Utils.Misc.

compiler/core/ErgoC/Lang/ErgoCOverloaded.v

@@ -14,6 +14,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 Require Import Basics.
 
 Require Import ErgoSpec.Utils.Misc.

compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.v

@@ -18,6 +18,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 Require Import Qcert.NNRC.NNRCRuntime.
 Require Import ErgoSpec.Common.Names.
 Require Import ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.

compiler/core/Translation/ErgoAssembly.v

@@ -41,7 +41,7 @@ Section ErgoAssembly.
                                "org.accordproject.ergo.stdlib.toText"%string
                                (template::nil)))).
 
-  Fixpoint add_template_to_clauses (prov:provenance) (template:list (string * laergo_expr)) (cl:list laergo_clause) :=
+  Definition add_template_to_clauses (prov:provenance) (template:list (string * laergo_expr)) (cl:list laergo_clause) :=
     cl ++ (List.map (fun xy => toDraftClause prov (fst xy) (snd xy)) template).
 
   Definition add_template_to_contract (template:list (string * laergo_expr)) (c:laergo_contract) :=

compiler/core/Translation/ErgoCTtoErgoNNRC.v

@@ -16,6 +16,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 
 Require Import Qcert.NNRC.NNRCRuntime.
 

compiler/core/Types/ErgoTypetoQcertType.v

@@ -92,7 +92,7 @@ Section ErgoTypetoQcertType.
       | ErgoTypeContract _ _ _ => ctxt
       end.
 
-    Fixpoint ergo_expand_extends_in_declarations (decls:list laergo_type_declaration) : expand_ctxt :=
+    Definition ergo_expand_extends_in_declarations (decls:list laergo_type_declaration) : expand_ctxt :=
       List.fold_left
         (fun ctxt decl =>
            ergo_decl_expand_extends

compiler/core/Utils/Misc.v

@@ -49,7 +49,7 @@ Section Misc.
     Definition postpend {A} (ls : list A) (a : A) : list A :=
       ls ++ (a :: nil).
 
-    Fixpoint last_some {A} (l:list (option A)) : option A :=
+    Definition last_some {A} (l:list (option A)) : option A :=
       let proc_one (one:option A) (acc:option A) :=
           match acc with
           | Some x => Some x
@@ -61,7 +61,7 @@ Section Misc.
         None
         l.
 
-    Fixpoint last_some_pair {A} {B} (l:list ((option A) * (option B))) : ((option A) * (option B)) :=
+    Definition last_some_pair {A} {B} (l:list ((option A) * (option B))) : ((option A) * (option B)) :=
       let proc_one (one : ((option A) * (option B))) (acc : ((option A) * (option B))) :=
           match acc with
           | (Some x, Some y) => acc

compiler/lib/static_config.ml

@@ -1,2 +1,2 @@
 (* This file is generated *)
-let ergo_home = "/Users/jeromesimeon/git/ergo"
+let ergo_home = "/Users/jeromesimeon/git/ergo-release-1.0"