# 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.2 Formal proof management system
dune 3.4.1 Fast, portable, and opinionated build system
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-fiat-crypto.0.0.13 coq.8.15.2Dry 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.13 coq.8.15.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.13 coq.8.15.2# 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.2 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.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 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.2). 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" "-j4" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml" (CWD=/home/bench/.opam/ocaml-base-compiler.4.07.1/.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 - 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/ZUtil/Tactics/DivideExistsMul.v - COQC src/Util/ZUtil/Lnot.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/Bool/LeCompat.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/ZUtil/N2Z.v - COQC src/Util/ZUtil/Pow2.v - COQC src/Util/ZUtil/Tactics/PeelLe.v - 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 - 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: - Warning: Trying to mask the absolute name "Coq.Sorting.Permutation"! - [masking-absolute-name,deprecated] - File "./src/Util/ListUti [...] truncated 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] - Finished transaction in 75.838 secs (11.48u,0.016s) (successful) - 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/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_unsaturated_solinas.v > src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml - Finished transaction in 34.414 secs (5.438u,0.007s) (successful) - COQC src/ExtractionOCaml/bedrock2_saturated_solinas.v > src/ExtractionOCaml/bedrock2_saturated_solinas.ml - Finished transaction in 56.807 secs (8.625u,0.004s) (successful) - 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_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/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 100.926 secs (15.378u,0.012s) (successful) - 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/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 52.232 secs (8.055u,0.012s) (successful) - COQC src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v > src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml - COQC src/ExtractionOCaml/bedrock2_base_conversion.v > src/ExtractionOCaml/bedrock2_base_conversion.ml - Finished transaction in 39.901 secs (6.208u,0.027s) (successful) - COQC src/ExtractionOCaml/perf_unsaturated_solinas.v > src/ExtractionOCaml/perf_unsaturated_solinas.ml - Finished transaction in 22.918 secs (3.49u,0.003s) (successful) - Finished transaction in 56.98 secs (8.827u,0.s) (successful) - COQC src/ExtractionOCaml/perf_word_by_word_montgomery.v > src/ExtractionOCaml/perf_word_by_word_montgomery.ml - 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] - 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/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/StandaloneDebuggingExamples.v - COQC src/Bedrock/Field/Synthesis/New/ComputedOp.v - COQC src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v - COQC src/Bedrock/Group/ScalarMult/MontgomeryLadder.v - 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/Group/ScalarMult/MontgomeryLadder.v", line 122, characters 11-12: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 122, characters 15-19: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 122, characters 40-41: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 122, characters 59-65: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - OCAMLOPT src/ExtractionOCaml/unsaturated_solinas.ml -o src/ExtractionOCaml/unsaturated_solinas - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 256, characters 12-13: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 256, characters 16-20: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 257, characters 12-13: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - File "./src/Bedrock/Group/ScalarMult/MontgomeryLadder.v", line 257, characters 31-37: - Warning: Ignoring implicit binder declaration in unexpected position. - [unexpected-implicit-declaration,syntax] - OCAMLOPT src/ExtractionOCaml/saturated_solinas.ml -o src/ExtractionOCaml/saturated_solinas - OCAMLOPT src/ExtractionOCaml/word_by_word_montgomery.ml -o src/ExtractionOCaml/word_by_word_montgomery - OCAMLOPT src/ExtractionOCaml/base_conversion.ml -o src/ExtractionOCaml/base_conversion - OCAMLOPT src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml -o src/ExtractionOCaml/bedrock2_unsaturated_solinas - OCAMLOPT src/ExtractionOCaml/bedrock2_saturated_solinas.ml -o src/ExtractionOCaml/bedrock2_saturated_solinas - OCAMLOPT src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml -o src/ExtractionOCaml/bedrock2_word_by_word_montgomery - OCAMLOPT src/ExtractionOCaml/bedrock2_base_conversion.ml -o src/ExtractionOCaml/bedrock2_base_conversion - OCAMLOPT src/ExtractionOCaml/perf_unsaturated_solinas.ml -o src/ExtractionOCaml/perf_unsaturated_solinas - OCAMLOPT src/ExtractionOCaml/perf_word_by_word_montgomery.ml -o src/ExtractionOCaml/perf_word_by_word_montgomery - COQC src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v - COQC src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v - COQC src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true