« Up

fiat-crypto 0.0.16 Error 🔥

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.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.16.tar.gz"
  checksum: "sha512=db5e3ce6eb30066150c3611222c48f0eaab02f5b6101faab20d8a586c4f23bacb0c46372eff03736d7f017195500b3ea0203895052bf6ade752030a08c77e86d"
}

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.16 coq.8.16.0
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.16 coq.8.16.0
Return code
0
Duration
2 h 16 m

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-fiat-crypto.0.0.16 coq.8.16.0
Return code
31744
Duration
4 h 1 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
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.16
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-fiat-crypto.0.0.16: http]
[coq-fiat-crypto.0.0.16] downloaded from https://github.com/mit-plv/fiat-crypto/archive/refs/tags/v0.0.16.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.16)
- ./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
- 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]
- COQC src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
- 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]
- 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]
- 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 "./src/Util/NatUtil.v", line 409, characters 10-22:
- Warning: Notation beq_nat_true is deprecated since 8.16.
- Use the bidirectional version Nat
[...] truncated
by_word_montgomery.v", line 4, characters 0-101:
- Warning: The identifier __ contains __ which is reserved for the extraction
- [extraction-reserved-identifier,extraction]
- COQC src/Bedrock/Field/Synthesis/New/Signature.v
- COQC src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
- COQC src/Bedrock/Group/AdditionChains.v
- COQC src/Bedrock/Group/ScalarMult/LadderStep.v
- COQC src/Bedrock/Field/Synthesis/Generic/Operation.v
- OCAMLOPT src/ExtractionOCaml/bedrock2_unsaturated_solinas.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- Section Variables:
- field_parameters
- : FieldParameters
- Section Variables:
- word
- : Interface.word width
- width
- : Z
- field_parameters
- : FieldParameters
- OCAMLOPT src/ExtractionOCaml/bedrock2_saturated_solinas.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/bedrock2_word_by_word_montgomery.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/bedrock2_base_conversion.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_saturated_solinas.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_base_conversion.mli
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- COQC src/Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.v
- COQC src/Bedrock/Field/Synthesis/Specialized/Tactics.v
- COQC src/Bedrock/Field/Synthesis/Specialized/ReifiedOperation.v
- File "./src/Bedrock/Group/AdditionChains.v", line 474, characters 6-44:
- Warning: Use of “Require” inside a section is fragile. It is not recommended
- to use this functionality in finished proof scripts.
- [require-in-section,fragile]
- COQC src/Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.v
- OCAMLOPT src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml -o src/ExtractionOCaml/bedrock2_unsaturated_solinas
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/bedrock2_saturated_solinas.ml -o src/ExtractionOCaml/bedrock2_saturated_solinas
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- File "src/ExtractionOCaml/bedrock2_saturated_solinas.ml", line 641936, characters 10-25:
- 641936 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/ExtractionOCaml/bedrock2_unsaturated_solinas.ml", line 715697, characters 10-25:
- 715697 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- OCAMLOPT src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml -o src/ExtractionOCaml/bedrock2_word_by_word_montgomery
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/bedrock2_base_conversion.ml -o src/ExtractionOCaml/bedrock2_base_conversion
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- ulimit
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml -o src/ExtractionOCaml/with_bedrock2_unsaturated_solinas
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- File "src/ExtractionOCaml/bedrock2_word_by_word_montgomery.ml", line 789681, characters 10-25:
- 789681 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/ExtractionOCaml/bedrock2_base_conversion.ml", line 636104, characters 10-25:
- 636104 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_saturated_solinas.ml -o src/ExtractionOCaml/with_bedrock2_saturated_solinas
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- File "src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml", line 715697, characters 10-25:
- 715697 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/ExtractionOCaml/with_bedrock2_saturated_solinas.ml", line 641936, characters 10-25:
- 641936 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml -o src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- OCAMLOPT src/ExtractionOCaml/with_bedrock2_base_conversion.ml -o src/ExtractionOCaml/with_bedrock2_base_conversion
- ulimit
- /bin/sh: 10: [: 8192: unexpected operator
- Warning: Stack size (8192) may be too small.
- Warning: To avoid stack overflows in OCaml compilation, setting stack size to the recommended minimum of 32768 kbytes
- COQC src/Bedrock/Field/Synthesis/New/ComputedOp.v
- COQC src/Bedrock/Group/ScalarMult/CSwap.v
- File "src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml", line 789681, characters 10-25:
- 789681 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- File "src/ExtractionOCaml/with_bedrock2_base_conversion.ml", line 636104, characters 10-25:
- 636104 | | S x' -> Pervasives.succ (int_of_nat x')
-                    ^^^^^^^^^^^^^^^
- Alert deprecated: module Stdlib.Pervasives
- Use Stdlib instead.
- 
- If you need to stay compatible with OCaml < 4.07, you can use the 
- stdlib-shims library: https://github.com/ocaml/stdlib-shims
- COQC src/Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.v
- COQC src/Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.v
- 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`.
- COQC src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v
- COQC src/Bedrock/Field/Synthesis/Examples/p256_64.v
- COQC src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
- COQC src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
- COQC src/Bedrock/Field/Synthesis/Examples/X25519_64.v
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