ยซ Up

fiat-crypto 0.0.13 Error ๐Ÿ”ฅ

๐Ÿ“… (2022-10-11 09:27:55 UTC)

Context

# 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.15.1      Formal proof management system
dune                     3.4.1       Fast, portable, and opinionated build system
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.9.1       A library manager for OCaml
ocamlfind-secondary      1.9.1       Adds support for ocaml-secondary-compiler to ocamlfind
zarith                   1.12        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: [
  "ocaml" {build}
  "ocamlfind" {build}
  "conf-jq" {build}
  "coq" {>= "8.11~"}
  "coq-coqprime" {>= "1.2.0"}
  "coq-rewriter" {= "0.0.2"}
  "coq-rupicola" {= "0.0.4"}
]
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.13.tar.gz"
  checksum: "sha512=c8f3da07cc4d8b2be86c9239d14c04a8ed990a12f80ce9b00c926cd5064afe1393de5bc52c673d7c7e0e099434ac4c2a03e302b2d23c47d97ce8dddb5404b75d"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-fiat-crypto.0.0.13 coq.8.15.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-fiat-crypto.0.0.13 coq.8.15.1
Return code
0
Duration
51 m 11 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.13 coq.8.15.1
Return code
7936
Duration
3 h 26 m
Output
# 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
conf-jq                  1           Virtual package relying on jq
coq                      8.15.1      Formal proof management system
coq-bedrock2             0.0.1       A work-in-progress language and compiler for verified low-level programming
coq-bignums              8.15.0      Bignums, the Coq library of arbitrary large numbers
coq-coqprime             1.2.0       Certifying prime numbers in Coq
coq-coqutil              0.0.1       Coq library for tactics, basic definitions, sets, maps
coq-rewriter             0.0.2       Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography
coq-rupicola             0.0.4       Gallina to imperative code compilation, currently in design phase
dune                     3.4.1       Fast, portable, and opinionated build system
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.9.1       A library manager for OCaml
ocamlfind-secondary      1.9.1       Adds support for ocaml-secondary-compiler to ocamlfind
zarith                   1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.15.1).
The following actions will be performed:
  - install coq-fiat-crypto 0.0.13
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-fiat-crypto.0.0.13: http]
[coq-fiat-crypto.0.0.13] downloaded from https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.13.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" "-j7" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-fiat-crypto.0.0.13)
- ./src/Rewriter/PerfTesting/Specific/make.py primes.txt
- GENTEST --makefile fiat-amd64/*.asm > Makefile.test-amd64-files.mk
- 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).
- CP src/Algebra/NsatzTactic.v.v815 src/Algebra/NsatzTactic.v (Coq v8.15)
- 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
- *** Warning: in file src/Bedrock/End2End/X25519/MontgomeryLadder.v, library compiler.Pipeline is required and has not been found in the loadpath!
- *** Warning: in file src/Bedrock/End2End/X25519/MontgomeryLadder.v, library compiler.MMIO is required and has not been found in the loadpath!
- *** Warning: in file src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v, library compiler.Pipeline is required and has not been found in the loadpath!
- *** Warning: in file src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v, library compiler.MMIO is required and has not been found in the loadpath!
- *** Warning: in file src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v, library riscv.Spec.Decode is required and has not been found in the loadpath!
- fatal: not a git repository (or any parent up to mount point /)
- Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).
- 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
- COQC src/Util/Tactics/GetGoal.v
- COQC src/Util/Strings/Decimal.v
- COQC src/Util/Tactics/Contains.v
- COQC src/Util/Comparison.v
- COQC src/Util/ZUtil/Tactics/SplitMinMax.v
- COQC src/Util/Tactics/HasBody.v
- COQC src/Util/Tactics/PrintContext.v
- COQC src/Util/Tactics/DebugPrint.v
- COQC src/Util/ListUtil/NthExt.v
- COQC src/Util/Structures/Orders.v
- COQC src/Util/Bool/Equality.v
- COQC src/Util/ZUtil/Div/Bootstrap.v
- COQC src/Util/ZUtil/Modulo/Bootstrap.v
- COQC src/Util/ZUtil/Tactics/PrimeBound.v
- COQC src/Util/ZUtil/Tactics/CompareToSgn.v
- COQC src/Util/ZUtil/Tactics/DivideExistsMul.v
- COQC src/Util/ZUtil/Lnot.v
- File "./src/Util/ZUtil/Div/Bootstrap.v", line 10, characters 2-35:
- Warning: The default value for hint locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding hints outside of sections without
- specifying an explicit locality attribute is therefore deprecated. It is
- recommended to use "export" whenever possible. Use the attributes #[local],
- #[global] and #[export] depending on your choice. For example: "#[export]
- Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated]
- COQC src/Util/Bool/LeCompat.v
- COQC src/Util/ZUtil/N2Z.v
- File "./src/Util/ZUtil/Modulo/Bootstrap.v", line 11, characters 2-35:
- Warning: The default value for hint locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding hints outside of sections without
- specifying an explicit locality attribute is therefore deprecated. It is
- recommended to use "export" whenever possible. Use the attributes #[local],
- #[global] and #[export] depending on your choice. For example: "#[export]
- Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated]
- COQC src/Util/ZUtil/Pow2.v
- COQC src/Util/ZUtil/Tactics/PeelLe.v
- File "./src/Util/Bool/LeCompat.v", line 6, characters 6-69:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 10, characters 6-10:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le_implb"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 14, characters 6-10:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.implb_true_r"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 15, characters 4-13:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 15, characters 4-13:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 15, characters 4-13:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le_implb"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 15, characters 4-13:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.implb_true_r"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 16, characters 2-11:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 16, characters 2-11:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 16, characters 2-11:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le_implb"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 16, characters 2-11:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.implb_true_r"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 17, characters 0-8:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 17, characters 0-8:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 17, characters 0-8:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.le_implb"!
- [masking-absolute-name,deprecated]
- File "./src/Util/Bool/LeCompat.v", line 17, characters 0-8:
- Warning: Trying to mask the absolute name "Coq.Bool.Bool.implb_true_r"!
- [masking-absolute-name,deprecated]
- COQC src/Util/Tactics/NormalizeCommutativeIdentifier.v
- COQC src/Util/Tactics/SetEvars.v
- COQC src/Util/Tactics/SubstEvars.v
- COQC src/Util/PER.v
- COQC src/Util/ListUtil/FoldMap.v
- COQC src/Util/ListUtil/PermutationCompat.v
- COQC src/Util/NUtil/Sorting.v
- COQC src/Util/NUtil/Testbit.v
- COQC src/Util/ListUtil/RemoveN.v
- COQC src/Algebra/NsatzTactic.v
- COQC src/Util/ZUtil/Odd.v
- COQC src/Util/Tactics/OnSubterms.v
- COQC src/Util/Tactics/Revert.v
- File "./src/Util/ListUtil/PermutationCompat.v", line 42, characters 0-27:
- Warning:
- Trying to mask the absolute name "Coq.Sorting.Permutation.Permutation_Forall2"!
- [masking-absolute-name,deprecated]
- File "./src/Util/ListUtil/PermutationCompat.v", line 43, characters 0-16:
- Warning: Trying to mask the absolute name "Coq.Sorting.Permutation"!
- [masking-absolute-name,deprecated]
- File "./src/Util/ListUtil/PermutationCompat.v", line 43, characters 0-16:
- Warning:
- Trying to mask the absolute name "Coq.Sorting.Permutation.Permutation_Forall2"!
- [masking-absolute-name,deprecated]
- File "./src/Util/ListUtil/PermutationCompat.v", line 44, characters 0-12:
- W
[...] truncated
- File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- COQC src/ExtractionOCaml/base_conversion.v > src/ExtractionOCaml/base_conversion.ml
- COQC src/ExtractionOCaml/bedrock2_unsaturated_solinas.v > src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml
- File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/saturated_solinas.v", line 3, characters 41-84:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- COQC src/ExtractionOCaml/bedrock2_saturated_solinas.v > src/ExtractionOCaml/bedrock2_saturated_solinas.ml
- File "./src/ExtractionOCaml/bedrock2_unsaturated_solinas.v", line 3, characters 52-97:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_unsaturated_solinas.v", line 3, characters 52-97:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/base_conversion.v", line 3, characters 39-80:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/Bedrock/Field/Synthesis/Examples/X25519_64.v", line 55, characters 9-59:
- Warning: native_compute disabled at configure time; falling back to
- vm_compute. [native-compute-disabled,native-compiler]
- File "./src/ExtractionOCaml/bedrock2_saturated_solinas.v", line 3, characters 50-93:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_saturated_solinas.v", line 3, characters 50-93:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_unsaturated_solinas.v", line 3, characters 52-97:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_unsaturated_solinas.v", line 3, characters 52-97:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- Finished transaction in 94.007 secs (9.19u,0.025s) (successful)
- COQC src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v > src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
- File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/word_by_word_montgomery.v", line 3, characters 47-94:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_saturated_solinas.v", line 3, characters 50-93:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_saturated_solinas.v", line 3, characters 50-93:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- Finished transaction in 96.827 secs (9.436u,0.021s) (successful)
- COQC src/ExtractionOCaml/bedrock2_base_conversion.v > src/ExtractionOCaml/bedrock2_base_conversion.ml
- COQC src/ExtractionOCaml/perf_unsaturated_solinas.v > src/ExtractionOCaml/perf_unsaturated_solinas.ml
- File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/Bedrock/Field/Synthesis/Examples/X25519_64.v", line 73, characters 9-59:
- Warning: native_compute disabled at configure time; falling back to
- vm_compute. [native-compute-disabled,native-compiler]
- File "./src/ExtractionOCaml/bedrock2_base_conversion.v", line 3, characters 48-89:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_base_conversion.v", line 3, characters 48-89:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- COQC src/ExtractionOCaml/perf_word_by_word_montgomery.v > src/ExtractionOCaml/perf_word_by_word_montgomery.ml
- COQC src/Bedrock/End2End/X25519/MontgomeryLadder.v
- File "./src/Bedrock/End2End/X25519/MontgomeryLadder.v", line 7, characters 0-33:
- Error: Cannot find a physical path bound to logical path compiler.Pipeline.
- 
- make: *** [Makefile.coq:763: src/Bedrock/End2End/X25519/MontgomeryLadder.vo] Error 1
- make: *** Waiting for unfinished jobs....
- Finished transaction in 47.285 secs (4.486u,0.006s) (successful)
- File "./src/ExtractionOCaml/bedrock2_base_conversion.v", line 3, characters 48-89:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_base_conversion.v", line 3, characters 48-89:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- Finished transaction in 68.082 secs (7.372u,0.s) (successful)
- File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- Finished transaction in 100.6 secs (13.054u,0.023s) (successful)
- Finished transaction in 35.354 secs (6.895u,0.041s) (successful)
- Finished transaction in 22.063 secs (5.02u,0.034s) (successful)
- Finished transaction in 14.875 secs (2.94u,0.03s) (successful)
- Finished transaction in 2291.503 secs (239.93u,0.313s) (successful)
- Finished transaction in 24.338 secs (7.09u,0.011s) (successful)
[ERROR] The compilation of coq-fiat-crypto failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j7 EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 coq standalone-ocaml".
#=== ERROR while compiling coq-fiat-crypto.0.0.13 =============================#
# context              2.0.1 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-fiat-crypto.0.0.13
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j7 EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 coq standalone-ocaml
# exit-code            2
# env-file             ~/.opam/log/coq-fiat-crypto-29897-335865.env
# output-file          ~/.opam/log/coq-fiat-crypto-29897-335865.out
### output ###
# [...]
# File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
# Warning: The identifier __ contains __ which is reserved for the extraction
# [extraction-reserved-identifier,extraction]
# File "./src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v", line 3, characters 56-103:
# Warning: The identifier __ contains __ which is reserved for the extraction
# [extraction-reserved-identifier,extraction]
# Finished transaction in 100.6 secs (13.054u,0.023s) (successful)
# Finished transaction in 35.354 secs (6.895u,0.041s) (successful)
# Finished transaction in 22.063 secs (5.02u,0.034s) (successful)
# Finished transaction in 14.875 secs (2.94u,0.03s) (successful)
# Finished transaction in 2291.503 secs (239.93u,0.313s) (successful)
# Finished transaction in 24.338 secs (7.09u,0.011s) (successful)
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-fiat-crypto 0.0.13
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-fiat-crypto.0.0.13 coq.8.15.1' failed.
The middle of the output is truncated (maximum 20000 characters)

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none