# 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.16.1 Formal proof management system
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
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.16.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-fiat-crypto.0.0.15 coq.8.16.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.15 coq.8.16.1# 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.16.1 Formal proof management system 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.16 Bignums, the Coq library of arbitrary large numbers coq-coqprime 1.3.0 Certifying prime numbers in Coq coq-coqutil 0.0.2 Coq library for tactics, basic definitions, sets, maps 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 dune 3.12.1 Fast, portable, and opinionated build system ocaml 4.13.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.13.1 Official release 4.13.1 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.16.1). 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.13.1/.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 - 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 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] - 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/Tactics/ConstrFail.v - COQC src/Util/ZUtil/Tactics/ReplaceNegWithPos.v - COQC src/Util/Tactics/GetGoal.v - 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] - COQC src/Util/Strings/Decimal.v - 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] - COQC src/Util/Tactics/Contains.v - COQC src/Util/Comparison.v - COQC src/Util/ZUtil/Tactics/SplitMinMax.v - File "./src/Util/NatUtil.v", line 330, characters 13-24: - Warning: Notation Max.max_0_l is deprecated since 8.16. - The Arith.Max file is obsolete. Use Nat.max_0_l instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 330, characters 25-36: - Warning: Notation Max.max_0_r is deprecated since 8.16. - The Arith.Max file is obsolete. Use Nat.max_0_r instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 330, characters 37-55: - Warning: Notation Max.max_idempotent is deprecated since 8.16. - The Arith.Max file is obsolete. Use Nat.max_id instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 330, characters 56-67: - Warning: Notation Min.min_0_l is deprecated since 8.16. - The Arith.Min file is obsolete. Use Nat.min_0_l instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 330, characters 68-79: - Warning: Notation Min.min_0_r is deprecated since 8.16. - The Arith.Min file is obsolete. Use Nat.min_0_r instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 330, characters 80-98: - 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/Tactics/HasBody.v - File "./src/Util/NatUtil.v", line 408, characters 12-19: - Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 408, characters 12-19: - Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Util/NatUtil.v", line 409, characters 10-22: - Warning: Notation beq_nat_true is deprecated since 8.16. - Use the bidir [...] truncated start - Finished transaction in 1.45 secs (1.425u,0.s) (successful) - Finished transaction in 1.096 secs (1.089u,0.003s) (successful) - Finished transaction in 0.498 secs (0.498u,0.s) (successful) - LoadOutputs end - LoadOutputs start - Finished transaction in 0.41 secs (0.41u,0.s) (successful) - Finished transaction in 0.728 secs (0.724u,0.003s) (successful) - Finished transaction in 0.665 secs (0.644u,0.015s) (successful) - LoadOutputs end - Finished transaction in 0.634 secs (0.618u,0.011s) (successful) - Finished transaction in 0.359 secs (0.359u,0.s) (successful) - Finished transaction in 0.899 secs (0.899u,0.s) (successful) - Finished transaction in 1.368 secs (1.363u,0.004s) (successful) - Finished transaction in 1.146 secs (1.13u,0.015s) (successful) - Finished transaction in 1.139 secs (1.134u,0.004s) (successful) - Finished transaction in 1.684 secs (1.675u,0.004s) (successful) - Finished transaction in 1.611 secs (1.588u,0.004s) (successful) - Finished transaction in 1.516 secs (1.491u,0.012s) (successful) - Finished transaction in 0.949 secs (0.938u,0.004s) (successful) - Finished transaction in 0.859 secs (0.842u,0.015s) (successful) - Finished transaction in 0.938 secs (0.914u,0.011s) (successful) - Finished transaction in 1.244 secs (1.221u,0.007s) (successful) - Finished transaction in 0.998 secs (0.987u,0.004s) (successful) - Finished transaction in 0.216 secs (0.206u,0.003s) (successful) - Finished transaction in 0.151 secs (0.147u,0.003s) (successful) - Finished transaction in 0.222 secs (0.218u,0.s) (successful) - Finished transaction in 0.08 secs (0.076u,0.003s) (successful) - Finished transaction in 2.573 secs (2.558u,0.007s) (successful) - Finished transaction in 1.908 secs (1.904u,0.s) (successful) - Finished transaction in 1.423 secs (1.418u,0.004s) (successful) - Finished transaction in 0.915 secs (0.915u,0.s) (successful) - COQC src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v - Finished transaction in 6.613 secs (6.568u,0.04s) (successful) - Finished transaction in 3.634 secs (3.561u,0.s) (successful) - Finished transaction in 1.37 secs (1.362u,0.007s) (successful) - Finished transaction in 0.992 secs (0.989u,0.s) (successful) - Finished transaction in 1.224 secs (1.196u,0.004s) (successful) - Finished transaction in 0.957 secs (0.932u,0.003s) (successful) - Finished transaction in 1.383 secs (1.354u,0.s) (successful) - Finished transaction in 0.87 secs (0.856u,0.s) (successful) - Finished transaction in 1.387 secs (1.362u,0.s) (successful) - Finished transaction in 0.972 secs (0.952u,0.s) (successful) - Finished transaction in 1.318 secs (1.289u,0.s) (successful) - Finished transaction in 0.966 secs (0.966u,0.s) (successful) - Finished transaction in 0.044 secs (0.044u,0.s) (successful) - Finished transaction in 0.02 secs (0.02u,0.s) (successful) - Finished transaction in 0.248 secs (0.248u,0.s) (successful) - Finished transaction in 0.169 secs (0.169u,0.s) (successful) - Finished transaction in 0.282 secs (0.282u,0.s) (successful) - Finished transaction in 0.166 secs (0.166u,0.s) (successful) - Finished transaction in 5.477 secs (5.469u,0.007s) (successful) - Finished transaction in 2.993 secs (2.993u,0.s) (successful) - Finished transaction in 5.383 secs (5.342u,0.007s) (successful) - Finished transaction in 2.015 secs (2.015u,0.s) (successful) - Finished transaction in 5.766 secs (5.758u,0.007s) (successful) - Finished transaction in 3.057 secs (2.992u,0.003s) (successful) - Finished transaction in 5.379 secs (5.269u,0.011s) (successful) - Finished transaction in 3.405 secs (3.381u,0.004s) (successful) - Finished transaction in 0.05 secs (0.05u,0.s) (successful) - Finished transaction in 0.017 secs (0.017u,0.s) (successful) - Finished transaction in 6.06 secs (5.979u,0.011s) (successful) - Finished transaction in 3.22 secs (3.16u,0.s) (successful) - COQC src/CompilersTestCases.v - COQC src/ArithmeticCPS/WordByWordMontgomery.v - COQC src/BoundsPipeline.v - COQC src/Arithmetic/BYInv.v - COQC src/Bedrock/Field/Translation/Cmd.v - COQC src/Bedrock/Field/Translation/Parameters/Defaults.v - COQC src/PushButtonSynthesis/SmallExamples.v - COQC src/COperationSpecifications.v - COQC src/PushButtonSynthesis/BYInversionReificationCache.v - Finished transaction in 4.715 secs (4.517u,0.015s) (successful) - Finished transaction in 4.837 secs (4.642u,0.008s) (successful) - Finished transaction in 5.446 secs (5.301u,0.016s) (successful) - Finished transaction in 1.305 secs (1.247u,0.019s) (successful) - Finished transaction in 1.64 secs (1.536u,0.s) (successful) - Finished transaction in 3.32 secs (3.245u,0.023s) (successful) - Finished transaction in 0.155 secs (0.151u,0.003s) (successful) - Finished transaction in 0.082 secs (0.082u,0.s) (successful) - Finished transaction in 0.088 secs (0.084u,0.s) (successful) - Finished transaction in 0.109 secs (0.1u,0.s) (successful) - Finished transaction in 0.099 secs (0.095u,0.003s) (successful) - Finished transaction in 0.133 secs (0.125u,0.004s) (successful) - COQC src/Bedrock/Field/Common/Util.v - Finished transaction in 3.122 secs (3.092u,0.s) (successful) - Finished transaction in 0.143 secs (0.143u,0.s) (successful) - Finished transaction in 0.096 secs (0.092u,0.s) (successful) - Finished transaction in 0.325 secs (0.317u,0.s) (successful) - Finished transaction in 0.208 secs (0.204u,0.s) (successful) - COQC src/Bedrock/Field/Translation/Func.v - COQC src/Bedrock/Field/Translation/Parameters/Defaults32.v - COQC src/Bedrock/Field/Translation/Parameters/FE310.v - COQC src/Bedrock/Field/Translation/Parameters/Defaults64.v - COQC src/PushButtonSynthesis/Primitives.v - COQC src/Bedrock/Field/Common/Tactics.v - Finished transaction in 0.099 secs (0.083u,0.015s) (successful) - Finished transaction in 0.008 secs (0.008u,0.s) (successful) - COQC src/Bedrock/End2End/RupicolaCrypto/Broadcast.v - Finished transaction in 0.583 secs (0.583u,0.s) (successful) - Finished transaction in 0.044 secs (0.044u,0.s) (successful) - Finished transaction in 0.443 secs (0.443u,0.s) (successful) - Finished transaction in 0.146 secs (0.146u,0.s) (successful) - Finished transaction in 0.075 secs (0.075u,0.s) (successful) - Finished transaction in 0.053 secs (0.053u,0.s) (successful) - Finished transaction in 0.086 secs (0.086u,0.s) (successful) - Finished transaction in 0.055 secs (0.055u,0.s) (successful) - Finished transaction in 0.009 secs (0.009u,0.s) (successful) - Finished transaction in 0.003 secs (0.003u,0.s) (successful) - Finished transaction in 0.171 secs (0.171u,0.s) (successful) - Finished transaction in 0.146 secs (0.146u,0.s) (successful) - Finished transaction in 0.121 secs (0.121u,0.s) (successful) - Finished transaction in 0.613 secs (0.613u,0.s) (successful) - COQC src/Bedrock/Field/Translation/Proofs/UsedVarnames.v - File "./src/Bedrock/Field/Translation/Proofs/UsedVarnames.v", line 55, characters 26-37: - Warning: Notation le_lt_or_eq is deprecated since 8.16. - The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead. - [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/Field/Translation/Proofs/UsedVarnames.v", line 55, characters 26-37: - Warning: Notation le_lt_or_eq is deprecated since 8.16. - The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead. - [deprecated-syntactic-definition,deprecated] - COQC src/Bedrock/Field/Common/Arrays/ByteBounds.v - COQC src/PushButtonSynthesis/BarrettReduction.v - COQC src/PushButtonSynthesis/FancyMontgomeryReduction.v - COQC src/PushButtonSynthesis/SaturatedSolinas.v - COQC src/PushButtonSynthesis/UnsaturatedSolinas.v - Finished transaction in 242.328 secs (237.709u,0.263s) (successful) - COQC src/PushButtonSynthesis/WordByWordMontgomery.v - Finished transaction in 19.542 secs (19.374u,0.028s) (successful) - COQC src/PushButtonSynthesis/BaseConversion.v - COQC src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v - COQC src/Fancy/Barrett256.v - Finished transaction in 37.656 secs (37.142u,0.191s) (successful) - COQC src/Bedrock/Field/Translation/Proofs/Flatten.v - File "./src/Bedrock/Field/Translation/Proofs/Flatten.v", line 58, characters 10-29: - 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/Bedrock/Field/Translation/Proofs/Flatten.v", line 58, characters 10-29: - 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/Bedrock/Field/Translation/Proofs/Flatten.v", line 83, characters 10-29: - 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/Bedrock/Field/Translation/Proofs/Flatten.v", line 83, characters 10-29: - 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/PushButtonSynthesis/WordByWordMontgomery.v", line 1039, characters 71-75: - Error: (in proof selectznz_correct): Attempt to save an incomplete proof - - make: *** [Makefile.coq:793: src/PushButtonSynthesis/WordByWordMontgomery.vo] Error 1 - make: *** Waiting for unfinished jobs.... - File "./src/Bedrock/Field/Translation/Proofs/Flatten.v", line 281, characters 10-29: - 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/Bedrock/Field/Translation/Proofs/Flatten.v", line 281, characters 10-29: - 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] The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true