# 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 dev Formal proof management system
dune 3.0.3 Fast, portable, and opinionated build system
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
homepage: "https://github.com/coq-community/hydra-battles"
dev-repo: "git+https://github.com/coq-community/hydra-battles.git"
bug-reports: "https://github.com/coq-community/hydra-battles/issues"
license: "MIT"
synopsis: "Exponentiation algorithms following addition chains"
description: """
Addition chains are algorithms for computations of the p-th power of some x,
with the least number of multiplication as possible. We present a few implementations of addition chains, with proofs of their correctness"""
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.5"}
"coq" {(>= "8.11" & < "8.14~") | (= "dev")}
"coq-paramcoq" {(>= "1.1.2" & < "1.2~") | (= "dev")}
"coq-mathcomp-ssreflect" {(>= "1.11.0" & < "1.13~") | (= "dev")}
"coq-mathcomp-algebra"
]
tags: [
"category:Mathematics/Combinatorics and Graph Theory"
"keyword:addition chains"
"keyword:exponentiation algorithms"
"logpath:additions"
"date:2021-05-19"
]
authors: [
"Pierre Castéran"
"Yves Bertot"
]
url {
src: "https://github.com/coq-community/hydra-battles/archive/v0.4.tar.gz"
checksum: "sha256=bba82794e49e03fd82fcee592b2b037ec20669d10e6c47ed8b4f8a7f851756eb"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-addition-chains.0.4 coq.devDry 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-addition-chains.0.4 coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-addition-chains.0.4 coq.dev# 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 dev Formal proof management system
coq-mathcomp-algebra dev Mathematical Components Library on Algebra
coq-mathcomp-fingroup dev Mathematical Components Library on finite groups
coq-mathcomp-ssreflect dev Small Scale Reflection
coq-paramcoq dev Paramcoq
dune 3.0.3 Fast, portable, and opinionated build system
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 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 dev).
The following actions will be performed:
- install coq-addition-chains 0.4
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-addition-chains.0.4: http]
[coq-addition-chains.0.4] downloaded from https://github.com/coq-community/hydra-battles/archive/v0.4.tar.gz
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-addition-chains: dune build]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coq-addition-chains" "-j" "4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-addition-chains.0.4)
- File "theories/additions/_unknown_", line 1, characters 0-0:
- (cd _build/default/theories/additions && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqdep -R . additions -dyndep opt Addition_Chains.v) > _build/default/theories/additions/Addition_Chains.v.d
- in file Addition_Chains.v, paramcoq is not a valid plugin name anymore.
- Plugins should be loaded using their public name according to findlib,
- for example package-name.foo and not foo_plugin.
- If you are building with dune < 2.9.4 you must specify both
- the legacy and the findlib plugin name as in:
- Declare ML Module "foo_plugin:package-name.foo".
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Monoid_def.v)
- Mult_op = fun A : Type => A -> A -> A
- : Type -> Type
-
- Arguments Mult_op A%type_scope
- mult_op =
- fun (A : Type) (Mult_op : Mult_op A) => Mult_op
- : forall A : Type, Mult_op A -> A -> A -> A
-
- Arguments mult_op {A}%type_scope {Mult_op} _ _
- File "./theories/additions/Monoid_def.v", line 44, characters 0-46:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_def.v", line 50, characters 0-47:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_def.v", line 126, characters 0-132:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_def.v", line 132, characters 0-129:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_def.v", line 138, characters 0-128:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_def.v", line 144, characters 0-131:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/FirstSteps.v)
- = 1024%Z
- : Z
- = 1024%Z
- : Z
- = "abababababababababababab"
- : string
- = "abababababababababababab"
- : string
- = 10946%N
- : N
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Naive.v)
- = 1024
- : Z
- = 9086410%N
- : N
- = 10946%N
- : N
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Pow_variant.v)
- File "./theories/additions/Pow_variant.v", line 166, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Pow_variant.v", line 166, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Pow_variant.v", line 166, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- = fun x : A =>
- x *
- (x * x * (x * x) * (x * x * (x * x)) *
- (x * x * (x * x) * (x * x * (x * x))))
- : A -> A
- = fun x : A =>
- x *
- (x *
- (x *
- (x *
- (x *
- (x *
- (x *
- (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * E_one))))))))))))))))
- : A -> A
- = fun x : A =>
- x * x * (x * x) * (x * x * (x * x)) *
- (x * x * (x * x) * (x * x * (x * x))) * x
- : A -> A
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Monoid_instances.v)
- File "./theories/additions/Monoid_instances.v", line 19, characters 0-40:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_instances.v", line 21, characters 0-37:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-witho
[...] truncated
xport" whenever possible. Use the attributes #[local],
- #[global] and #[export] depending on your choice. For example: "#[export]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_instances.v", line 106, characters 0-48:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/Monoid_instances.v", line 108, characters 0-46:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- = Npos (xI (xO (xO (xI (xI xH)))))
- : N
- = Npos
- (xI (xO (xO (xI (xI (xI (xO (xO (xI (xI (xI (xO (xI xH)))))))))))))
- : N
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Pow.v)
- File "./theories/additions/Pow.v", line 167, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Pow.v", line 167, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Pow.v", line 167, characters 38-47:
- Warning: Notation plus_comm is deprecated since 8.16.
- The Arith.Plus file is obsolete. Use Nat.add_comm instead.
- [deprecated-syntactic-definition,deprecated]
- = fun x : A =>
- x *
- (x * x * (x * x) * (x * x * (x * x)) *
- (x * x * (x * x) * (x * x * (x * x))))
- : A -> A
- = fun x : A =>
- x *
- (x *
- (x *
- (x *
- (x *
- (x *
- (x *
- (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * E_one))))))))))))))))
- : A -> A
- = fun x : A =>
- x * x * (x * x) * (x * x * (x * x)) *
- (x * x * (x * x) * (x * x * (x * x))) * x
- : A -> A
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Demo_power.v)
- = 705429498686404044207947776
- : Z
- = 2131755008%int31
- : int31
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/fib.v)
- = [:: 1%Z; 0%Z; 0%Z]
- : seq Z
- = [:: 233%Z; 89%Z; 144%Z]
- : seq Z
- = 233%Z
- : Z
- = true
- : bool
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Compatibility.v)
- fun x y : A => x * y
- : A -> A -> A
- File "./theories/additions/Compatibility.v", line 82, characters 14-23:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Compatibility.v", line 82, characters 14-23:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Compatibility.v", line 82, characters 14-23:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Compatibility.v", line 105, characters 13-22:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Compatibility.v", line 105, characters 13-22:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- File "./theories/additions/Compatibility.v", line 105, characters 13-22:
- Warning: Notation mult_comm is deprecated since 8.16.
- The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
- [deprecated-syntactic-definition,deprecated]
- = 1
- : Z
- Finished transaction in 9.824 secs (4.73u,0.s) (successful)
- = 1
- : Z
- Finished transaction in 0. secs (0.u,0.s) (successful)
- Z.pow =
- fun x y : Z =>
- match y with
- | 0 => 1
- | Z.pos p => Z.pow_pos x p
- | Z.neg _ => 0
- end
- : Z -> Z -> Z
-
- Arguments Z.pow (x y)%Z_scope
- Z.pow_pos = fun z : Z => Pos.iter (Z.mul z) 1
- : Z -> positive -> Z
-
- Arguments Z.pow_pos z%Z_scope _%positive_scope
- = fun x : nat => S (S (S (S (S (S (S (S (S (S (S (S x)))))))))))
- : nat -> nat
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/BinaryStrat.v)
- File "./theories/additions/BinaryStrat.v", line 21, characters 0-38:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- File "./theories/additions/BinaryStrat.v", line 26, characters 0-34:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
- (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Dichotomy.v)
- = 4
- : positive
- = 8
- : positive
- = 16
- : positive
- = 8
- : positive
- File "./theories/additions/Dichotomy.v", line 190, characters 0-38:
- Warning: The default value for instance locality is currently "local" in a
- section and "global" otherwise, but is scheduled to change in a future
- release. For the time being, adding instances 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]
- Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
[ERROR] The compilation of coq-addition-chains failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-addition-chains -j 4".
#=== ERROR while compiling coq-addition-chains.0.4 ============================#
# context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-addition-chains.0.4
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-addition-chains -j 4
# exit-code 1
# env-file ~/.opam/log/coq-addition-chains-22828-335865.env
# output-file ~/.opam/log/coq-addition-chains-22828-335865.out
### output ###
# (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.09.1/bin/coqc -w -notation-overridden -w -ambiguous-paths -R theories/additions additions theories/additions/Dichotomy.v)
# [...]
# : positive
# = 8
# : positive
# File "./theories/additions/Dichotomy.v", line 190, characters 0-38:
# Warning: The default value for instance locality is currently "local" in a
# section and "global" otherwise, but is scheduled to change in a future
# release. For the time being, adding instances 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]
# Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-addition-chains 0.4
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-addition-chains.0.4 coq.dev' failed.
The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true