Update coq-fiat-crypto{,-with-bedrock}.dev install (#2839)

We now generate (and install) a single unified binary, rather than a collection. There's also a short test to make sure it's installed correctly.
coq · Nov 18, 2023 · 57bff7e · 57bff7e
1 parent 7dd993e
commit 57bff7e
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git a/extra-dev/packages/coq-fiat-crypto-with-bedrock/coq-fiat-crypto-with-bedrock.dev/opam b/extra-dev/packages/coq-fiat-crypto-with-bedrock/coq-fiat-crypto-with-bedrock.dev/opam
@@ -11,14 +11,18 @@ homepage: "https://github.com/mit-plv/fiat-crypto"
 bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
 license: "MIT OR Apache-2.0 OR BSD-1-Clause"
 build: [
-  [make "-j%{jobs}%" "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "coq" "standalone-ocaml"]
+  [make "-j%{jobs}%" "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "coq" "standalone-unified-ocaml"]
+]
+install: [
+  [make "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "BINDIR=%{bin}%" "install" "install-standalone-unified-ocaml"]
+  ["etc/test-run-fiat-crypto-silent.sh" "%{bin}%/fiat_crypto"] {with-test}
+  ["etc/test-run-fiat-crypto-silent.sh" "fiat_crypto"] {with-test}
 ]
-install: [make "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "BINDIR=%{bin}%" "install" "install-standalone-ocaml"]
 depends: [
   "conf-findutils" {build}
   "ocaml" {build & >= "4.08~"}
   "ocamlfind" {build}
-  "coq" {>= "8.15~"}
+  "coq" {>= "8.16~"}
   "coq-coqprime"
   "coq-rewriter"
 ]

diff --git a/extra-dev/packages/coq-fiat-crypto/coq-fiat-crypto.dev/opam b/extra-dev/packages/coq-fiat-crypto/coq-fiat-crypto.dev/opam
@@ -11,14 +11,18 @@ homepage: "https://github.com/mit-plv/fiat-crypto"
 bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
 license: "MIT OR Apache-2.0 OR BSD-1-Clause"
 build: [
-  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "coq-without-bedrock2" "standalone-ocaml"]
+  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "coq-without-bedrock2" "standalone-unified-ocaml"]
+]
+install: [
+  [make "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "BINDIR=%{bin}%" "install-without-bedrock2" "install-standalone-unified-ocaml"]
+  ["etc/test-run-fiat-crypto-silent-no-bedrock2.sh" "%{bin}%/fiat_crypto"] {with-test}
+  ["etc/test-run-fiat-crypto-silent-no-bedrock2.sh" "fiat_crypto"] {with-test}
 ]
-install: [make "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "BINDIR=%{bin}%" "install-without-bedrock2" "install-standalone-ocaml"]
 depends: [
   "conf-findutils" {build}
   "ocaml" {build & >= "4.08~"}
   "ocamlfind" {build}
-  "coq" {>= "8.15~"}
+  "coq" {>= "8.16~"}
   "coq-coqprime"
   "coq-rewriter"
   "coq-coqutil"