# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
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.12.2 Fast, portable, and opinionated build system
ocaml 5.1.1 The OCaml compiler (virtual package)
ocaml-base-compiler 5.1.1 Official release 5.1.1
ocaml-config 3 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.16~"}
"coq-coqprime" {>= "1.2.0"}
"coq-rewriter" {>= "0.0.6" & <= "0.0.9"}
"coq-rupicola" {= "0.0.8"}
"coq-bedrock2-compiler" {= "0.0.6"}
]
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.24.tar.gz"
checksum: "sha512=eb1a871b7ec2469be78a95e677f39e238cb0b13228530e297f2d9b5e4808711a7ff2dde823aebd00d64505acc4f3fb580b6a9646b6523bd49ad7253257336f53"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-fiat-crypto.0.0.24 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.24 coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-fiat-crypto.0.0.24 coq.8.17.0# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap 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.6 A work-in-progress language and compiler for verified low-level programming coq-bedrock2-compiler 0.0.6 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.4 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.9 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.4 RISC-V Specification in Coq, somewhat experimental coq-rupicola 0.0.8 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.12.2 Fast, portable, and opinionated build system ocaml 5.1.1 The OCaml compiler (virtual package) ocaml-base-compiler 5.1.1 Official release 5.1.1 ocaml-config 3 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.24 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/3: [coq-fiat-crypto.0.0.24: http] Processing 1/3: -> retrieved coq-fiat-crypto.0.0.24 (https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.24.tar.gz) Processing 2/3: [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.5.1.1/.opam-switch/build/coq-fiat-crypto.0.0.24) - ./src/Rewriter/PerfTesting/Specific/make.py primes.txt - GENTEST --makefile fiat-amd64/fiat_* > 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:153: warning: overriding recipe for target 'all' - Makefile.coq:408: warning: ignoring old recipe for target 'all' - Makefile:488: warning: overriding recipe for target 'validate' - Makefile.coq:536: warning: ignoring old recipe for target 'validate' - ECHO > src/Everything.v - ECHO > src/Bedrock/Everything.v - 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:153: warning: overriding recipe for target 'all' - Makefile.coq:408: warning: ignoring old recipe for target 'all' - Makefile:488: warning: overriding recipe for target 'validate' - Makefile.coq:536: warning: ignoring old recipe for target 'validate' - 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/Tactics/Contains.v - COQC src/Util/Comparison.v - COQC src/Util/Tactics/GetGoal.v - COQC src/Util/ListUtil/NthExt.v - COQC src/Util/Tactics/DebugPrint.v - COQC src/Util/ZUtil/Hints/Core.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] - 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/ZUtil/Tactics/SplitMinMax.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 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] - File "./src/Util/NatUtil.v", line 272, characters 10-17: - Warning: Notati [...] truncated g: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - OCAMLOPT src/ExtractionOCaml/with_bedrock2_dettman_multiplication.mli - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - OCAMLOPT src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.mli - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - OCAMLOPT src/ExtractionOCaml/with_bedrock2_base_conversion.mli - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - COQC src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v - COQC src/Bedrock/Group/ScalarMult/CSwap.v - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1136, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1136, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1136, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1136, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - OCAMLOPT src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml -o src/ExtractionOCaml/bedrock2_unsaturated_solinas - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1257, characters 10-22: - Warning: Notation Nat.mod_same is deprecated since 8.17. - Use Div0.mod_same instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1257, characters 10-22: - Warning: Notation Nat.mod_same is deprecated since 8.17. - Use Div0.mod_same instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1262, characters 10-21: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1262, characters 10-21: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1326, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1326, characters 12-23: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1349, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1349, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1349, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1349, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1371, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1371, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1371, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1371, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1383, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1383, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1383, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - File "./src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v", line 1383, characters 14-25: - Warning: Notation Nat.mod_mul is deprecated since 8.17. - Use Div0.mod_mul instead. [deprecated-syntactic-definition,deprecated] - Compilation incomplete. - You may need to add new compilation lemmas using `Hint Extern 1 => simple eapply … : compiler` or to tell Rupicola about your custom bindings using `Hint Extern 2 (IsRupicolaBinding (xlet (A := ?A) ?vars _ _)) => exact (RupicolaBinding A vars) : typeclass_instances`. - OCAMLOPT src/ExtractionOCaml/bedrock2_saturated_solinas.ml -o src/ExtractionOCaml/bedrock2_saturated_solinas - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - Evars: 6409 -> 6 - - Evars: 7889 -> 6 - - OCAMLOPT src/ExtractionOCaml/bedrock2_dettman_multiplication.ml -o src/ExtractionOCaml/bedrock2_dettman_multiplication - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - OCAMLOPT src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml -o src/ExtractionOCaml/bedrock2_word_by_word_montgomery - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - OCAMLOPT src/ExtractionOCaml/bedrock2_base_conversion.ml -o src/ExtractionOCaml/bedrock2_base_conversion - Warning: Stack size (8192) may be too small. - Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 66520 kbytes - Evars: 9375 -> 4 - - Fatal error: allocation failure during minor GC - Evars: 27270 -> 4 - - - as: out of memory allocating 4064 bytes after a total of 448974848 bytes - /opam-tmp/camlasmb29f20.s: Assembler messages: - /opam-tmp/camlasmb29f20.s: Fatal error: src/ExtractionOCaml/bedrock2_word_by_word_montgomery.o: memory exhausted - File "src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml", line 1: - Error: Assembler error, input left in file /opam-tmp/camlasmb29f20.s - make: *** [Makefile.standalone:40: src/ExtractionOCaml/bedrock2_word_by_word_montgomery] Error 2 - make: *** Waiting for unfinished jobs.... - ocamlopt.opt got signal and exited - make: *** [Makefile.standalone:40: src/ExtractionOCaml/bedrock2_base_conversion] Error 2 [ERROR] The compilation of coq-fiat-crypto.0.0.24 failed at "make -j4 EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 coq standalone-ocaml". #=== ERROR while compiling coq-fiat-crypto.0.0.24 =============================# # context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.1.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.5.1.1/.opam-switch/build/coq-fiat-crypto.0.0.24 # 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-30641-b4e21b.env # output-file ~/.opam/log/coq-fiat-crypto-30641-b4e21b.out ### output ### # [...] # Evars: 27270 -> 4 # # # as: out of memory allocating 4064 bytes after a total of 448974848 bytes # /opam-tmp/camlasmb29f20.s: Assembler messages: # /opam-tmp/camlasmb29f20.s: Fatal error: src/ExtractionOCaml/bedrock2_word_by_word_montgomery.o: memory exhausted # File "src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml", line 1: # Error: Assembler error, input left in file /opam-tmp/camlasmb29f20.s # make: *** [Makefile.standalone:40: src/ExtractionOCaml/bedrock2_word_by_word_montgomery] Error 2 # make: *** Waiting for unfinished jobs.... # ocamlopt.opt got signal and exited # make: *** [Makefile.standalone:40: src/ExtractionOCaml/bedrock2_base_conversion] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-fiat-crypto 0.0.24 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-fiat-crypto.0.0.24 coq.8.17.0' failed. The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true