# 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.0 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.10.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2 Official release 4.10.2
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
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: [
"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.6"}
"coq-bedrock2-compiler" {= "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.17.tar.gz"
checksum: "sha512=c7688c84fcc10cc063cff24d5d3d52edd04f26b16adb00e7389d648964e2a0cc0d81fa615d9091e491edd6fed81859f1ea4a12e19ba6793975be2b301369778a"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-fiat-crypto.0.0.17 coq.8.16.0Dry 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.17 coq.8.16.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.17 coq.8.16.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.16.0 Formal proof management system coq-bedrock2 0.0.4 A work-in-progress language and compiler for verified low-level programming coq-bedrock2-compiler 0.0.4 A work-in-progress language and compiler for verified low-level programming (compiler part) coq-bignums 8.16.0 Bignums, the Coq library of arbitrary large numbers coq-coqprime 1.2.0 Certifying prime numbers in Coq coq-coqutil 0.0.2 Coq library for tactics, basic definitions, sets, maps coq-record-update 0.3.1 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.3 RISC-V Specification in Coq, somewhat experimental coq-rupicola 0.0.6 Gallina to imperative code compilation, currently in design phase dune 3.6.2 Fast, portable, and opinionated build system ocaml 4.10.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.2 Official release 4.10.2 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is 8.16.0). The following actions will be performed: - install coq-fiat-crypto 0.0.17 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-fiat-crypto.0.0.17: http] [coq-fiat-crypto.0.0.17] downloaded from https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.17.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.10.2/.opam-switch/build/coq-fiat-crypto.0.0.17) - ./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:154: warning: overriding recipe for target 'all' - Makefile.coq:408: warning: ignoring old recipe for target 'all' - Makefile:489: 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:154: warning: overriding recipe for target 'all' - Makefile.coq:408: warning: ignoring old recipe for target 'all' - Makefile:489: 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/ZSimplify/Simple.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 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/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 - 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/Comparison.v - COQC src/Util/ZUtil/Tactics/SplitMinMax.v - 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 bidirectional version Nat.eqb_eq instead. - [deprecated-syntactic-definition,deprecated] - File "./s [...] truncated uction.v - COQC src/Arithmetic/FancyMontgomeryReduction.v - Finished transaction in 1355.226 secs (17.681u,0.344s) (successful) - COQC src/ArithmeticCPS/Freeze.v - COQC src/Bedrock/Field/Translation/Cmd.v - COQC src/Bedrock/Field/Translation/Parameters/Defaults.v - COQC src/PushButtonSynthesis/BarrettReductionReificationCache.v - COQC src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v - File "./src/Assembly/WithBedrock/Proofs.v", line 2945, characters 70-88: - 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] - build_inputs start - build_inputs end - build_merge_base_addresses start - build_merge_base_addresses end - build_merge_base_addresses start - Finished transaction in 57.671 secs (6.309u,0.023s) (successful) - Finished transaction in 51.089 secs (5.555u,0.021s) (successful) - Finished transaction in 21.695 secs (2.412u,0.009s) (successful) - COQC src/PushButtonSynthesis/SmallExamples.v - Finished transaction in 32.386 secs (3.594u,0.001s) (successful) - COQC src/Arithmetic/Freeze.v - File "./src/Assembly/WithBedrock/Proofs.v", line 2945, characters 70-88: - 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] - File "./src/Assembly/WithBedrock/Proofs.v", line 2945, characters 70-88: - 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] - build_merge_base_addresses end - COQC src/ArithmeticCPS/WordByWordMontgomery.v - COQC src/Bedrock/Field/Translation/Func.v - build_merge_stack_placeholders start - build_merge_stack_placeholders end - Finished transaction in 39.538 secs (4.17u,0.013s) (successful) - get callee_saved_registers start - get callee_saved_registers end - COQC src/Bedrock/Field/Translation/Parameters/Defaults32.v - Finished transaction in 41.214 secs (4.34u,0.02s) (successful) - get callee_saved_registers start - SymexLines start - SymexLines end - Finished transaction in 14.605 secs (1.509u,0.012s) (successful) - Finished transaction in 18.025 secs (1.85u,0.004s) (successful) - COQC src/Bedrock/Field/Translation/Parameters/FE310.v - Finished transaction in 36.246 secs (3.916u,0.011s) (successful) - get callee_saved_registers start - get callee_saved_registers end - Finished transaction in 1.879 secs (0.219u,0.s) (successful) - Finished transaction in 1.26 secs (0.113u,0.003s) (successful) - Finished transaction in 1.189 secs (0.107u,0.s) (successful) - Finished transaction in 1.22 secs (0.124u,0.s) (successful) - Finished transaction in 1.287 secs (0.125u,0.s) (successful) - Finished transaction in 1.574 secs (0.167u,0.s) (successful) - COQC src/Bedrock/Field/Translation/Parameters/Defaults64.v - COQC src/Curves/Montgomery/AffineInstances.v - LoadArray start - LoadArray end - LoadOutputs start - COQC src/Arithmetic/WordByWordMontgomery.v - COQC src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v - LoadOutputs end - LoadOutputs start - Finished transaction in 25.827 secs (2.814u,0.002s) (successful) - LoadOutputs end - Finished transaction in 17.311 secs (1.736u,0.007s) (successful) - Finished transaction in 24.368 secs (2.77u,0.007s) (successful) - Finished transaction in 21.81 secs (2.342u,0.002s) (successful) - Finished transaction in 17.779 secs (1.967u,0.012s) (successful) - Finished transaction in 14.202 secs (1.67u,0.s) (successful) - Finished transaction in 14.781 secs (1.544u,0.s) (successful) - Finished transaction in 10.297 secs (1.067u,0.004s) (successful) - Finished transaction in 12.044 secs (1.444u,0.007s) (successful) - COQC src/Curves/Montgomery/XZProofs.v - Finished transaction in 9.721 secs (1.031u,0.s) (successful) - Finished transaction in 5.081 secs (0.572u,0.s) (successful) - Finished transaction in 3.561 secs (0.399u,0.s) (successful) - Finished transaction in 7.638 secs (0.837u,0.s) (successful) - Finished transaction in 4.83 secs (0.58u,0.s) (successful) - Finished transaction in 8.252 secs (0.933u,0.s) (successful) - Finished transaction in 5.416 secs (0.58u,0.s) (successful) - Finished transaction in 14.237 secs (1.64u,0.004s) (successful) - Finished transaction in 12.797 secs (1.306u,0.s) (successful) - Finished transaction in 18.601 secs (1.954u,0.021s) (successful) - Finished transaction in 16.084 secs (1.69u,0.s) (successful) - Finished transaction in 21.604 secs (2.173u,0.014s) (successful) - Finished transaction in 17.322 secs (1.838u,0.s) (successful) - Finished transaction in 168.912 secs (18.187u,0.084s) (successful) - Warning: Native compiler is disabled, -native-compiler ondemand option - ignored. [native-compiler-disabled,native-compiler] - Warning: The native-compiler option is deprecated. To compile native files - ahead of time, use the coqnative binary instead. - [deprecated-native-compiler-option,deprecated] - Warning: Native compiler is disabled, -native-compiler ondemand option - ignored. [native-compiler-disabled,native-compiler] - Warning: The native-compiler option is deprecated. To compile native files - ahead of time, use the coqnative binary instead. - [deprecated-native-compiler-option,deprecated] - Finished transaction in 16.857 secs (1.777u,0.003s) (successful) - Finished transaction in 11.168 secs (1.118u,0.004s) (successful) - Finished transaction in 20.024 secs (1.803u,0.003s) (successful) - Finished transaction in 12.649 secs (1.144u,0.s) (successful) - Finished transaction in 22.772 secs (1.904u,0.008s) (successful) - Finished transaction in 12.694 secs (1.208u,0.s) (successful) - Finished transaction in 2.658 secs (0.259u,0.s) (successful) - Finished transaction in 1.786 secs (0.188u,0.s) (successful) - Finished transaction in 3.274 secs (0.315u,0.s) (successful) - Finished transaction in 1.496 secs (0.16u,0.s) (successful) - Finished transaction in 36.306 secs (3.267u,0.015s) (successful) - Finished transaction in 25.343 secs (2.358u,0.023s) (successful) - Finished transaction in 16.78 secs (1.747u,0.011s) (successful) - Finished transaction in 11.998 secs (1.137u,0.s) (successful) - COQC src/Arithmetic/BYInv.v - COQC src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v - Finished transaction in 323.082 secs (7.241u,0.415s) (successful) - Finished transaction in 48.248 secs (5.223u,0.003s) (successful) - Finished transaction in 71.826 secs (7.82u,0.008s) (successful) - Finished transaction in 35.622 secs (3.51u,0.s) (successful) - Finished transaction in 15.696 secs (1.712u,0.006s) (successful) - Finished transaction in 8.855 secs (0.992u,0.s) (successful) - Finished transaction in 15.703 secs (1.624u,0.007s) (successful) - Finished transaction in 8.867 secs (0.951u,0.s) (successful) - Finished transaction in 15.55 secs (1.62u,0.s) (successful) - Finished transaction in 7.695 secs (0.859u,0.s) (successful) - Finished transaction in 17.296 secs (1.783u,0.007s) (successful) - Finished transaction in 8.252 secs (0.878u,0.003s) (successful) - Finished transaction in 16.227 secs (1.729u,0.007s) (successful) - Finished transaction in 9.164 secs (0.951u,0.s) (successful) - Finished transaction in 0.563 secs (0.053u,0.s) (successful) - Finished transaction in 0.209 secs (0.019u,0.001s) (successful) - Finished transaction in 2.88 secs (0.296u,0.003s) (successful) - Finished transaction in 1.481 secs (0.167u,0.003s) (successful) - Finished transaction in 3.245 secs (0.338u,0.s) (successful) - Finished transaction in 1.604 secs (0.166u,0.s) (successful) - Finished transaction in 62.979 secs (6.538u,0.008s) (successful) - Finished transaction in 33.75 secs (3.483u,0.004s) (successful) - Finished transaction in 56.305 secs (6.028u,0.007s) (successful) - Finished transaction in 33.757 secs (3.668u,0.003s) (successful) - Finished transaction in 55.793 secs (5.835u,0.015s) (successful) - Finished transaction in 34.513 secs (3.571u,0.008s) (successful) - Finished transaction in 56.165 secs (5.913u,0.031s) (successful) - Finished transaction in 33.914 secs (3.335u,0.003s) (successful) - Finished transaction in 0.631 secs (0.059u,0.s) (successful) - Finished transaction in 0.166 secs (0.019u,0.s) (successful) - Finished transaction in 67.797 secs (7.1u,0.003s) (successful) - Finished transaction in 29.989 secs (3.177u,0.s) (successful) - COQC src/PushButtonSynthesis/BYInversionReificationCache.v - Finished transaction in 55.155 secs (5.821u,0.012s) (successful) - Finished transaction in 32.264 secs (3.257u,0.s) (successful) - Finished transaction in 2. secs (0.2u,0.s) (successful) - Finished transaction in 1.087 secs (0.107u,0.s) (successful) - Finished transaction in 4.581 secs (0.441u,0.s) (successful) - Finished transaction in 1.938 secs (0.223u,0.s) (successful) - COQC src/COperationSpecifications.v - COQC src/PushButtonSynthesis/Primitives.v - Finished transaction in 0.316 secs (0.03u,0.s) (successful) - Finished transaction in 0.106 secs (0.01u,0.s) (successful) - Finished transaction in 1.628 secs (0.174u,0.s) (successful) - Finished transaction in 0.504 secs (0.05u,0.004s) (successful) - Finished transaction in 1.951 secs (0.195u,0.s) (successful) - Finished transaction in 1.892 secs (0.195u,0.s) (successful) - Finished transaction in 0.968 secs (0.105u,0.s) (successful) - Finished transaction in 1.854 secs (0.186u,0.s) (successful) - Finished transaction in 5.866 secs (0.587u,0.s) (successful) - Finished transaction in 0.762 secs (0.074u,0.s) (successful) - Finished transaction in 0.12 secs (0.012u,0.s) (successful) - Finished transaction in 0.076 secs (0.004u,0.s) (successful) - Finished transaction in 4.521 secs (0.468u,0.s) (successful) - Finished transaction in 1.635 secs (0.182u,0.s) (successful) - Finished transaction in 1.363 secs (0.155u,0.s) (successful) - Finished transaction in 0.915 secs (0.093u,0.s) (successful) - COQC src/Bedrock/Field/Common/Util.v The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true