# 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.6.2 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.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.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.17 coq.8.15.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.17 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 coq 8.15.2 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.15.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.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.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.15.2). 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.13.1/.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:386: warning: ignoring old recipe for target 'all' - Makefile:489: warning: overriding recipe for target 'validate' - Makefile.coq:514: 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:386: warning: ignoring old recipe for target 'all' - Makefile:489: warning: overriding recipe for target 'validate' - Makefile.coq:514: 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 - 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/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 - COQC src/Util/Bool/LeCompat.v - 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/Unit.v - COQC src/Util/ListUtil/SetoidListRev.v - COQC src/Util/ListUtil/RemoveN.v - COQC src/Algebra/Nsatz.v - COQC src/Util/ZUtil/Odd.v - COQC src/Util/Tactics/OnSubterms.v - COQC src/Util/Tactics/Revert.v - COQC src/Util/Factorize.v - COQC src/Util/Decidable/Bool2Prop.v - COQC src/Util/FueledLUB.v - COQC src/Util/Tactics/SimplifyRepeatedIfs.v - COQC src/TAPSort.v - COQC src/Util/ZUtil/Z2Nat.v - COQC src/Util/Tactics/ETransitivity.v - COQC src/Util/Tactics/SubstLet.v - COQC src/Util/ZUtil/ModExp.v - COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised.v - COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.v - COQC src/Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.v - COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v - COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v - COQC src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.v - COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v - COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.v - COQC src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.v - COQC src/Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.v - COQC src/Util/Loops.v - COQC src/PushButtonSynthesis/InvertHighLow.v - COQC src/Util/Tactics/ChangeInAll.v - COQC src/Util/DefaultedTypes.v - COQC src/Util/Pos.v - COQC src/Util/Sumbool.v - COQC src/Util/Bool/IsTrue.v - COQC src/Util/ZUtil/DistrIf.v - COQC src/Util/ZUtil/Ge.v - COQC src/Util/ZUtil/Mul.v - COQC src/Util/ZUtil/Sgn.v - COQC src/Util/ZUtil/Sorting.v - COQC src/Util/SideConditions/CorePackages.v - COQC src/Util/Logic/ImplAnd.v - COQC src/Util/Sigma/Associativity.v - COQC src/Util/Sigma/Lift.v - COQC src/Util/Sigma/MapProjections.v - COQC src/Util/Sigma/Related.v - COQC src/Util/Tactics/CPSId.v - COQC src/Util/Tactics/EvarNormalize.v - COQC src/Util/Tactics/ClearFree.v - COQC src/Util/Tactics/ClearAll.v - COQC src/Util/Tactics/ClearDuplicates.v - COQC src/Util/Tactics/ClearbodyAll.v - COQC src/Util/Tactics/ConvoyDestruct.v - COQC src/Util/Tactics/DestructTrivial.v - COQC src/Util/Tactics/ESpecialize.v - COQC src/Util/Tactics/EvarExists.v - COQC src/Util/Tactics/Forward.v - COQC src/Util/Tactics/PoseTermWithName.v - COQC src/Util/Tactics/SideConditionsBeforeToAfter.v - COQC src/Util/Tactics/SimplifyProjections.v - COQC src/Util/Tactics/TransparentAssert.v - COQC src/Util/Tactics/UnfoldArg.v - COQC src/Util/Tactics/UnifyAbstractReflexivity.v - COQC src/Util/Tactics/VM.v - COQC src/Util/ZUtil/Hints/ZArith.v - COQC src/Util/ZUtil/Hints/Ztestbit.v - COQC src/Util/ZUtil/Hints/PullPush.v - COQC src/Util/ZUtil/ZSimplify/Core.v - COQC src/Util/Equality.v - COQC src/Util/FixCoqMistakes.v - COQC src/Util/Tactics/Not.v - COQC src/Util/Tactics/SetoidSubst.v - COQC src/Util/PrimitiveProd.v - COQC src/Util/Tactics/FindHyp.v - COQC src/Util/DynList.v - COQC src/Util/Tactics/CountBinders.v - COQC src/Util/Tactics/AppendUnderscores.v - COQC src/Util/Tactics/PrintGoal.v - COQC src/Util/PrimitiveHList.v - COQC src/Util/Tactics/RunTacticAsConstr.v - COQC src/Util/Structures/Equalities.v - COQC src/Util/Structures/Equalities/Iso.v - COQC src/Util/Logic/Forall.v - COQC src/Util/Logic/Exists.v - COQC src/Util/ZUtil/Tactics/DivModToQuotRem.v - COQC src/Util/ZUtil/Modulo/PullPush.v - COQC src/Util/ZUtil/Tactics/LinearSubstitute.v - COQC src/Util/ZUtil/Opp.v - COQC src/Util/Logic/ProdForall.v - COQC src/Util/ListUtil/Partition.v - COQC src/Util/ListUtil/StdlibCompat.v - COQC src/Util/Structures/Equalities/Project.v - COQC src/Util/ListUtil/Concat.v - COQC src/Util/ListUtil/Filter.v - COQC src/Util/Logic.v - COQC src/Util/Structures/Equalities/Unit.v - COQC src/Util/Tactics/WarnIfGoalsRemain.v - COQC src/Util/ListUtil/CombineExtend.v - COQC src/Util/ZUtil/Nat2Z.v - COQC src/Util/Telescope/Core.v - COQC src/Util/ListUtil/Split.v - COQC src/Util/Tactics/RevertUntil.v - COQC src/Util/Curry.v - COQC src/Util/Tactics.v - COQC src/Util/Tower.v - COQC src/Util/Wf.v - COQC src/Util/Tactics/HeadUnderBinders.v - COQC src/Util/Structures/Equalities/Empty.v - COQC src/Util/Strings/String_as_OT.v - COQC src/Util/Strings/String_as_OT_old.v - COQC src/Util/Tactics/CacheTerm.v - COQC src/Util/Tactics/Delta1.v - COQC src/Util/ZUtil/Hints.v - COQC src/Util/Prod.v - COQC src/Util/Sigma.v - COQC src/Util/Tactics/Head.v - COQC src/Util/Tactics/DestructHyps.v - COQC src/Util/Notations.v - File "./src/Util/Sigma.v", line 376, characters 0-52: - Warning: The Ltac name inversion_sigma may be unusable because of a conflict - with a notation. [unusable-identifier,parsing] - COQC src/Util/Tactics/SpecializeBy.v - COQC src/Util/Tactics/DoWithHyp.v - COQC src/Util/Tac [...] truncated . - Refining with verified rewriter... - COQC src/Rewriter/Passes/FlattenThunkedRects.v - Reifying... - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 0.484 secs (0.048u,0.s) (success) - Tactic call ran for 0.115 secs (0.011u,0.s) (success) - Tactic call ran for 0.846 secs (0.082u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 0.193 secs (0.017u,0.s) (success) - Tactic call ran for 1.322 secs (0.144u,0.s) (success) - Proving Rewriter_Interp... - Tactic call ran for 3.266 secs (0.348u,0.001s) (success) - Tactic call ran for 0.535 secs (0.058u,0.s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Rewriter/Passes/MulSplit.v - Reifying... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 20.554 secs (2.199u,0.004s) (success) - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 2.596 secs (0.328u,0.s) (success) - Tactic call ran for 7.485 secs (0.76u,0.s) (success) - Tactic call ran for 1.274 secs (0.129u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 3.7 secs (0.42u,0.006s) (success) - Tactic call ran for 41.055 secs (4.389u,0.031s) (success) - Proving Rewriter_Interp... - Tactic call ran for 110.421 secs (11.548u,0.027s) (success) - Tactic call ran for 45.692 secs (4.883u,0.031s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Rewriter/Passes/MultiRetSplit.v - Reifying... - Tactic call ran for 1448.251 secs (151.922u,0.339s) (success) - Tactic call ran for 5.268 secs (0.55u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 26.186 secs (2.808u,0.s) (success) - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 3.596 secs (0.411u,0.s) (success) - Tactic call ran for 38.169 secs (4.025u,0.007s) (success) - Tactic call ran for 19.3 secs (2.124u,0.s) (success) - Tactic call ran for 1.507 secs (0.15u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Proving Rewriter_Interp... - Tactic call ran for 6.75 secs (0.7u,0.004s) (success) - Tactic call ran for 68.768 secs (7.655u,0.003s) (success) - Tactic call ran for 101.563 secs (10.77u,0.039s) (success) - Proving Rewriter_Interp... - Tactic call ran for 60.139 secs (6.407u,0.s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - Tactic call ran for 169.903 secs (17.665u,0.028s) (success) - COQC src/Rewriter/Passes/NoSelect.v - Reifying... - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 1.407 secs (0.142u,0.s) (success) - Tactic call ran for 0.253 secs (0.017u,0.s) (success) - Tactic call ran for 0.894 secs (0.093u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 0.419 secs (0.045u,0.s) (success) - Tactic call ran for 7.026 secs (0.731u,0.004s) (success) - Proving Rewriter_Interp... - Tactic call ran for 92.197 secs (9.658u,0.035s) (success) - Tactic call ran for 15.848 secs (1.716u,0.s) (success) - Tactic call ran for 9.329 secs (1.009u,0.s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Rewriter/Passes/RelaxBitwidthAdcSbb.v - Reifying... - Assembling verified rewriter... - Compiling decision tree... - Refining with verified rewriter... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 1.568 secs (0.164u,0.s) (success) - Tactic call ran for 0.683 secs (0.072u,0.s) (success) - Tactic call ran for 1.034 secs (0.108u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 0.898 secs (0.092u,0.s) (success) - Tactic call ran for 8.516 secs (0.898u,0.s) (success) - Proving Rewriter_Interp... - Tactic call ran for 23.341 secs (2.442u,0.s) (success) - Tactic call ran for 7.606 secs (0.759u,0.004s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Rewriter/Passes/ToFancy.v - Reifying... - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 0.264 secs (0.028u,0.s) (success) - Tactic call ran for 0.088 secs (0.008u,0.s) (success) - Tactic call ran for 0.818 secs (0.082u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 0.138 secs (0.011u,0.s) (success) - Tactic call ran for 0. secs (0.u,0.s) (success) - Proving Rewriter_Interp... - Tactic call ran for 2.825 secs (0.284u,0.s) (success) - Tactic call ran for 0. secs (0.u,0.s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Rewriter/Passes/ToFancyWithCasts.v - COQC src/Rewriter/Passes/UnfoldValueBarrier.v - Reifying... - Reifying... - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 0.312 secs (0.039u,0.s) (success) - Tactic call ran for 0.052 secs (0.008u,0.s) (success) - Tactic call ran for 0.612 secs (0.075u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 0.095 secs (0.011u,0.s) (success) - Tactic call ran for 0.421 secs (0.04u,0.s) (success) - Proving Rewriter_Interp... - Tactic call ran for 3.951 secs (0.388u,0.s) (success) - Tactic call ran for 0.001 secs (0.001u,0.s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/AbstractInterpretation/WfExtra.v - COQC src/AbstractInterpretation/Proofs.v - Compiling decision tree... - Splitting rewrite rules... - Assembling rewrite_head... - Reducing rewrite_head... - Tactic call ran for 16.498 secs (1.703u,0.004s) (success) - Tactic call ran for 2159.453 secs (230.45u,0.408s) (success) - Tactic call ran for 3.896 secs (0.429u,0.s) (success) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Proving Rewriter_Wf... - Tactic call ran for 35.903 secs (3.759u,0.s) (success) - COQC src/Arithmetic/BaseConversion.v - COQC src/PushButtonSynthesis/SaturatedSolinasReificationCache.v - Tactic call ran for 108.856 secs (11.416u,0.004s) (success) - Finished transaction in 38.591 secs (4.192u,0.022s) (successful) - Finished transaction in 22.58 secs (2.505u,0.s) (successful) - COQC src/PushButtonSynthesis/BaseConversionReificationCache.v - Tactic call ran for 565.722 secs (59.607u,0.242s) (success) - Tactic call ran for 2.728 secs (0.307u,0.s) (success) - Proving Rewriter_Interp... - Finished transaction in 18.585 secs (2.079u,0.027s) (successful) - Assembling rewrite_head_no_dtree... - Reducing rewrite_head_no_dtree... - Finished transaction in 16.252 secs (1.703u,0.s) (successful) - Proving Rewriter_Wf... - COQC src/Stringification/C.v - COQC src/Stringification/Rust.v - Tactic call ran for 20.949 secs (2.271u,0.s) (success) - COQC src/Stringification/Go.v - COQC src/Stringification/Java.v - COQC src/Stringification/JSON.v - COQC src/Stringification/Zig.v - COQC src/Arithmetic/BarrettReduction.v - Tactic call ran for 98.981 secs (10.232u,0.024s) (success) - Proving Rewriter_Interp... - Tactic call ran for 284.216 secs (30.276u,0.035s) (success) - COQC src/Arithmetic/FancyMontgomeryReduction.v - Tactic call ran for 104.859 secs (11.15u,0.s) (success) - Finished transaction in 4165.526 secs (436.239u,0.327s) (successful) - File "./src/UnsaturatedSolinasHeuristics/Tests.v", line 155, characters 0-1766: - Warning: native_compute disabled at configure time; falling back to - vm_compute. [native-compute-disabled,native-compiler] - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/ArithmeticCPS/BaseConversion.v - COQC src/Assembly/WithBedrock/Proofs.v - Tactic call ran for 290.17 secs (30.881u,0.035s) (success) - Tactic call ran for 76.052 secs (8.32u,0.007s) (success) - Assembling verified rewriter... - Refining with verified rewriter... - COQC src/Bedrock/Field/Stringification/FlattenVarData.v - COQC src/Curves/Montgomery/AffineInstances.v - COQC src/PushButtonSynthesis/BarrettReductionReificationCache.v - Finished transaction in 66.8 secs (6.951u,0.023s) (successful) - COQC src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v - Finished transaction in 40.441 secs (4.262u,0.004s) (successful) - COQC src/Rewriter/All.v - COQC src/Arithmetic/Freeze.v - Finished transaction in 57.021 secs (5.937u,0.027s) (successful) - COQC src/CompilersTestCases.v - Finished transaction in 27.157 secs (2.969u,0.s) (successful) - COQC src/ArithmeticCPS/Freeze.v - COQC src/Curves/Montgomery/XZProofs.v - COQC src/BoundsPipeline.v - COQC src/Arithmetic/WordByWordMontgomery.v - Finished transaction in 169.766 secs (18.284u,0.071s) (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] The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true