# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.17.0 The Coq Proof Assistant
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
authors: [
"Andres Erbsen <andreser@mit.edu>"
"Google Inc."
"Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com>"
"Massachusetts Institute of Technology"
"Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>"
]
maintainer: "Jason Gross <jgross@mit.edu>"
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_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "BINDIR=%{bin}%" "install" "install-standalone-ocaml"]
depends: [
"conf-findutils" {build}
"ocaml" {build & >= "4.08~"}
"ocamlfind" {build}
"coq" {>= "8.15~"}
"coq-coqprime" {>= "1.2.0"}
"coq-rewriter" {>= "0.0.6" & <= "0.0.7"}
"coq-rupicola" {= "0.0.5"}
"coq-bedrock2-compiler" {= "0.0.3"}
]
conflict-class: [
"coq-fiat-crypto"
]
dev-repo: "git+https://github.com/mit-plv/fiat-crypto.git"
synopsis: "Cryptographic Primitive Code Generation by Fiat"
description: """
Coq code and proofs for a command-line binary that can synthesize proven-correct
big-integer modular field arithmetic operations for cryptography.
Target languages include C, Rust, Zig, Go, and bedrock2.
"""
tags: ["logpath:Crypto"]
url {
src: "https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.15.tar.gz"
checksum: "sha512=0f761a739ca97dff99792e766516e122ee141670f3a28eaca2735f8a7fc6d924e16dccff2cf18b362c44e3cff7f73e407d2b8b33f7786cac96a9c425cca11b8e"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-fiat-crypto.0.0.15 coq.8.17.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-fiat-crypto.0.0.15 coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-fiat-crypto.0.0.15 coq.8.17.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.17.0 The Coq Proof Assistant
coq-bedrock2 0.0.3 A work-in-progress language and compiler for verified low-level programming
coq-bedrock2-compiler 0.0.3 A work-in-progress language and compiler for verified low-level programming (compiler part)
coq-bignums 9.0.0+coq8.17 Bignums, the Coq library of arbitrarily large numbers
coq-coqprime 1.4.0 Certifying prime numbers in Coq
coq-coqutil 0.0.2 Coq library for tactics, basic definitions, sets, maps
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-record-update 0.3.3 Generic support for updating record fields in Coq
coq-rewriter 0.0.7 Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography
coq-riscv 0.0.2 RISC-V Specification in Coq, somewhat experimental
coq-rupicola 0.0.5 Gallina to imperative code compilation, currently in design phase
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.17.0).
The following actions will be performed:
- install coq-fiat-crypto 0.0.15
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-fiat-crypto.0.0.15: http]
[coq-fiat-crypto.0.0.15] downloaded from https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.15.tar.gz
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-fiat-crypto: make coq]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml" (CWD=/home/bench/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-fiat-crypto.0.0.15)
- ./src/Rewriter/PerfTesting/Specific/make.py primes.txt
- GENTEST --makefile fiat-amd64/*.asm > Makefile.test-amd64-files.mk
- ECHO > _CoqProject
- COQ_MAKEFILE -f _CoqProject > Makefile.coq
- Warning: native compilation is globally deactivated by the configure flag
- fatal: not a git repository (or any parent up to mount point /)
- Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).
- Makefile:352: warning: overriding recipe for target 'all'
- Makefile.coq:408: warning: ignoring old recipe for target 'all'
- Makefile:963: warning: overriding recipe for target 'validate'
- Makefile.coq:536: warning: ignoring old recipe for target 'validate'
- ECHO > src/Util/Tactics.v
- fatal: not a git repository (or any parent up to mount point /)
- Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).
- COQDEP VFILES
- fatal: not a git repository (or any parent up to mount point /)
- Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).
- Makefile:352: warning: overriding recipe for target 'all'
- Makefile.coq:408: warning: ignoring old recipe for target 'all'
- Makefile:963: warning: overriding recipe for target 'validate'
- Makefile.coq:536: warning: ignoring old recipe for target 'validate'
- COQC src/Util/ZUtil/Hints/Core.v
- COQC src/Util/NatUtil.v
- COQC src/Util/Pointed.v
- COQC src/Util/IffT.v
- COQC src/Util/Isomorphism.v
- COQC src/Util/HProp.v
- COQC src/Util/GlobalSettings.v
- COQC src/Util/Tactics/Test.v
- COQC src/Util/Tactics/ConstrFail.v
- COQC src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
- File "./src/Util/NatUtil.v", line 14, characters 0-57:
- Warning: Notation plus_le_compat is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_le_mono instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 16, characters 25-32:
- Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 34, characters 13-32:
- Warning: Notation Min.min_case_strong is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 34, characters 13-32:
- Warning: Notation Min.min_case_strong is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Tactics/GetGoal.v
- File "./src/Util/NatUtil.v", line 36, characters 13-32:
- Warning: Notation Max.max_case_strong is deprecated since 8.16.
- The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 36, characters 13-32:
- Warning: Notation Max.max_case_strong is deprecated since 8.16.
- The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 50, characters 44-63:
- Warning: Notation Max.max_case_strong is deprecated since 8.16.
- The Arith.Max file is obsolete. Use Nat.max_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 49, characters 44-63:
- Warning: Notation Min.min_case_strong is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Strings/Decimal.v
- File "./src/Util/NatUtil.v", line 156, characters 43-50:
- Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Tactics/Contains.v
- File "./src/Util/NatUtil.v", line 156, characters 43-50:
- Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 178, characters 12-23:
- Warning: Notation mult_succ_r is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_succ_r instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 178, characters 12-23:
- Warning: Notation mult_succ_r is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_succ_r instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 178, characters 12-23:
- Warning: Notation mult_succ_r is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_succ_r instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 185, characters 12-23:
- Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 185, characters 12-23:
- Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 185, characters 12-23:
- Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 229, characters 8-21:
- Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 232, characters 23-39:
- Warning: Notation beq_nat_true_iff is deprecated since 8.16.
- Use Nat.eqb_eq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 233, characters 23-40:
- Warning: Notation beq_nat_false_iff is deprecated since 8.16.
- Use Nat.eqb_neq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 232, characters 23-39:
- Warning: Notation beq_nat_true_iff is deprecated since 8.16.
- Use Nat.eqb_eq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 232, characters 23-39:
- Warning: Notation beq_nat_true_iff is deprecated since 8.16.
- Use Nat.eqb_eq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 233, characters 23-40:
- Warning: Notation beq_nat_false_iff is deprecated since 8.16.
- Use Nat.eqb_neq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 233, characters 23-40:
- Warning: Notation beq_nat_false_iff is deprecated since 8.16.
- Use Nat.eqb_neq instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 252, characters 28-36:
- Warning: Notation mod_same is deprecated since 8.17.
- Use Div0.mod_same instead. [deprecated-syntactic-definition,deprecated]
- File "./src/Util/NatUtil.v", line 252, characters 28-36:
- Warning: Notation mod_same is deprecated since 8.17.
- Use Div0.mod_same instead. [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Comparison.v
- File "./src/Util/NatUtil.v", line 272, characters 10-17:
- Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead.
- [deprecated-syntactic-definition,deprecated]
- F
[...] truncated
e Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 280, characters 76-85:
- Warning: Notation minus_n_O is deprecated since 8.16.
- The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 280, characters 76-85:
- Warning: Notation minus_n_O is deprecated since 8.16.
- The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 289, characters 44-62:
- Warning: Notation minus_diag_reverse is deprecated since 8.16.
- The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 289, characters 44-62:
- Warning: Notation minus_diag_reverse is deprecated since 8.16.
- The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 289, characters 44-62:
- Warning: Notation minus_diag_reverse is deprecated since 8.16.
- The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/ZUtil/Ltz.v
- COQC src/Util/ZUtil/MulSplit.v
- COQC src/Util/ZUtil/Zselect.v
- COQC src/Util/ListUtil/Forall.v
- COQC src/Util/ZUtil/AddModulo.v
- COQC src/Util/ZUtil/Rshi.v
- COQC src/Util/ZUtil/Combine.v
- File "./src/Util/ListUtil.v", line 1485, characters 48-59:
- Warning: Tactic instantiate is deprecated since 8.16.
- [deprecated-tactic,deprecated]
- File "./src/Util/ListUtil.v", line 1656, characters 8-27:
- Warning: Notation Min.min_case_strong is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 1656, characters 8-27:
- Warning: Notation Min.min_case_strong is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Structures/Equalities/Option.v
- COQC src/Util/Structures/Orders/Prod.v
- COQC src/Util/Structures/Orders/Option.v
- COQC src/Util/Structures/Orders/Flip.v
- File "./src/Util/ListUtil.v", line 2236, characters 14-23:
- Warning: Notation Min.min_l is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 2236, characters 14-23:
- Warning: Notation Min.min_l is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 2236, characters 14-23:
- Warning: Notation Min.min_l is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 2236, characters 14-23:
- Warning: Notation Min.min_l is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_l instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ListUtil.v", line 2236, characters 14-23:
- Warning: Notation Min.min_l is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_l instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/ListUtil/IndexOf.v
- COQC src/Util/Structures/Orders/Unit.v
- COQC src/Util/FSets/FMapInterface.v
- COQC src/Util/FSets/FMapFacts.v
- COQC src/Util/ListUtil/SetoidListFlatMap.v
- COQC src/Util/FSets/FMapSect.v
- COQC src/Util/Structures/Equalities/List.v
- COQC src/Util/FSets/FMapTrie/Shape.v
- COQC src/Util/ErrorT/List.v
- COQC src/Algebra/Group.v
- COQC src/Util/ZUtil/ModInv.v
- File "./src/Algebra/Group.v", line 98, characters 2-316:
- Warning: A coercion will be introduced instead of an instance in future
- versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
- use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
- Beware that the default locality for '::' is #[export], as opposed to
- #[global] for ':>' currently. Add an explicit #[global] attribute to the
- field if you need to keep the current behavior. For example: "Class foo := {
- #[global] field :: bar }." [future-coercion-class-field,records]
- COQC src/Bedrock/Group/Loops.v
- File "./src/Algebra/Group.v", line 145, characters 2-400:
- Warning: A coercion will be introduced instead of an instance in future
- versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
- use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
- Beware that the default locality for '::' is #[export], as opposed to
- #[global] for ':>' currently. Add an explicit #[global] attribute to the
- field if you need to keep the current behavior. For example: "Class foo := {
- #[global] field :: bar }." [future-coercion-class-field,records]
- COQC src/Util/Wf2.v
- COQC src/Util/FSets/FMapEmpty.v
- COQC src/Util/MSets/MSetPositive/Facts.v
- COQC src/Util/SideConditions/ModInvPackage.v
- COQC src/Util/ZUtil/Pow.v
- COQC src/Util/Bool/Reflect.v
- COQC src/Util/Tuple.v
- COQC src/MiscCompilerPasses.v
- File "./src/Util/Tuple.v", line 261, characters 116-134:
- Warning: Notation Min.min_idempotent is deprecated since 8.16.
- The Arith.Min file is obsolete. Use Nat.min_id instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/Structures/Orders/Sum.v
- COQC src/Util/MSets/MSetIso.v
- COQC src/Util/Strings/Parse/Common.v
- COQC src/Util/Listable.v
- COQC src/MiscCompilerPassesProofs.v
- COQC src/Util/ZUtil/Div.v
- COQC src/Util/ZUtil/AddGetCarry.v
- File "./src/Util/ZUtil/Div.v", line 312, characters 13-25:
- Warning: Notation Z_div_mod_eq is deprecated since 8.14.
- Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ZUtil/Div.v", line 312, characters 13-25:
- Warning: Notation Z_div_mod_eq is deprecated since 8.14.
- Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ZUtil/Div.v", line 312, characters 13-25:
- Warning: Notation Z_div_mod_eq is deprecated since 8.14.
- Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
- File "./src/Util/ZUtil/Div.v", line 376, characters 6-17:
- Warning: Tactic instantiate is deprecated since 8.16.
- [deprecated-tactic,deprecated]
- COQC src/Assembly/Syntax.v
- COQC src/Util/Strings/ParseArithmetic.v
- COQC src/Util/Structures/OrdersEx.v
- COQC src/Util/FSets/FMapUnit.v
- COQC src/Util/FSets/FMapIso.v
- COQC src/Util/FSets/FMapFlip.v
- COQC src/Util/FSets/FMapSum.v
- COQC src/Util/FSets/FMapProd.v
- COQC src/Util/Structures/Orders/List.v
- COQC src/Util/MSets/MSetN.v
- COQC src/Util/Strings/ParseArithmeticToTaps.v
- COQC src/Algebra/ScalarMult.v
- COQC src/Algebra/Ring.v
- COQC src/Util/IdfunWithAlt.v
- COQC src/Assembly/WithBedrock/Semantics.v
- COQC src/Fancy/Spec.v
- COQC src/Util/AdditionChainExponentiation.v
- COQC src/Util/HList.v
- COQC src/Util/Decidable/Decidable2Bool.v
- COQC src/Util/FSets/FMapBool.v
- File "./src/Util/Decidable/Decidable2Bool.v", line 39, characters 10-22:
- Warning: Notation beq_nat_true is deprecated since 8.16.
- Use the bidirectional version Nat.eqb_eq instead.
- [deprecated-syntactic-definition,deprecated]
- File "./src/Util/Decidable/Decidable2Bool.v", line 39, characters 10-22:
- Warning: Notation beq_nat_true is deprecated since 8.16.
- Use the bidirectional version Nat.eqb_eq instead.
- [deprecated-syntactic-definition,deprecated]
- COQC src/Util/SideConditions/Autosolve.v
- COQC src/Util/ZUtil/Log2.v
- COQC src/Util/Level.v
- COQC src/Util/ZRange.v
- COQC src/Util/MSets/MSetSum.v
- COQC src/Util/ZUtil/Tactics/ZeroBounds.v
- COQC src/Util/ZUtil/Divide.v
- File "./src/Util/MSets/MSetSum.v", line 227, characters 4-11:
- Error: Cannot infer an instance of type "relation Prop" for the variable RA.
-
- make: *** [Makefile.coq:830: src/Util/MSets/MSetSum.vo] Error 1
- make: *** [src/Util/MSets/MSetSum.vo] Deleting file 'src/Util/MSets/MSetSum.glob'
- make: *** Waiting for unfinished jobs....
[ERROR] The compilation of coq-fiat-crypto failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4 EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 coq standalone-ocaml".
#=== ERROR while compiling coq-fiat-crypto.0.0.15 =============================#
# context 2.0.10 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/coq-fiat-crypto.0.0.15
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 coq standalone-ocaml
# exit-code 2
# env-file ~/.opam/log/coq-fiat-crypto-27228-335865.env
# output-file ~/.opam/log/coq-fiat-crypto-27228-335865.out
### output ###
# [...]
# COQC src/Util/ZUtil/Log2.v
# COQC src/Util/Level.v
# COQC src/Util/ZRange.v
# COQC src/Util/MSets/MSetSum.v
# COQC src/Util/ZUtil/Tactics/ZeroBounds.v
# COQC src/Util/ZUtil/Divide.v
# File "./src/Util/MSets/MSetSum.v", line 227, characters 4-11:
# Error: Cannot infer an instance of type "relation Prop" for the variable RA.
#
# make: *** [Makefile.coq:830: src/Util/MSets/MSetSum.vo] Error 1
# make: *** [src/Util/MSets/MSetSum.vo] Deleting file 'src/Util/MSets/MSetSum.glob'
# make: *** Waiting for unfinished jobs....
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-fiat-crypto 0.0.15
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-fiat-crypto.0.0.15 coq.8.17.0' failed.
The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true