Merge 2a16a6c into e29bd7c

.circleci/config.yml

@@ -1,5 +1,5 @@
 common_cache_key: &common_cache_key
-  key: dependency-cache-{{ checksum "../ocaml-version" }}-{{ checksum ".circleci/config.yml" }}
+  key: dependency-cache-{{ checksum "../ocaml-version" }}-{{ checksum ".circleci/config.yml" }}-{{ checksum "coq-ergo-lang.opam" }}
 
 common_steps: &common_steps
   steps:
@@ -41,11 +41,6 @@ common_steps: &common_steps
         name: "Install OPAM deps"
         command: opam install . --deps-only --jobs=$NJOBS --yes
         no_output_timeout: 45m
-    - run:
-        name: "Install Q*cert"
-        command: |
-          opam install -y -v coq-qcert.2.1.1
-        no_output_timeout: 45m
     - save_cache:
         <<: *common_cache_key
         paths:
@@ -57,7 +52,7 @@ common_steps: &common_steps
           eval $(opam env)
           make cleanall
     - run:
-        name: 'Build the Ergo compiler'
+        name: 'Build Ergo'
         command:  |
           eval $(opam env)
           make configure

DEVELOPERS.md

@@ -54,7 +54,7 @@ To rebuild the compiler from the source, you will need Coq 8.12 and OCaml >=4.09
 ```sh
 $ opam repo add coq-released https://coq.inria.fr/opam/released
 $ opam install dune menhir base64 js_of_ocaml js_of_ocaml-ppx yojson atdgen re calendar uri
-$ opam install coq.8.12.2 coq-qcert.2.1.0
+$ opam install coq.8.12.2 coq-qcert.2.1.1
 ```
 
 ##### Build the Ergo Compiler and REPL

coq-ergo-lang.opam

@@ -27,14 +27,18 @@ depends: [
   "ocaml" {>= "4.07.1"}
   "ocamlfind"
   "dune"
-  "coq" {>= "8.8.2" & < "8.9~"}
-  "coq-flocq" {>= "2.6.1" & < "3.0~"}
-  "coq-jsast" {>= "1.0.9"}
-  "coq-qcert" {>= "2.0.0~alpha.1"}
+  "coq" {= "8.12.2"}
+  "coq-jsast" {>= "2.0.0"}
+  "coq-qcert" {>= "2.1.1"}
   "menhir"
   "base64"
-  "uri"
+  "js_of_ocaml"
+  "js_of_ocaml-ppx"
+  "yojson"
+  "atdgen"
+  "re"
   "calendar"
+  "uri"
 ]
 
 tags: [ "keyword:dsl" "keyword:legal" "keyword:smartcontract" "keyword:blockchain" "date:2020-01-30" "logpath:ErgoSpec" ]