« Up

addition-chains 0.4 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                 dev         Formal proof management system
dune                3.0.3       Fast, portable, and opinionated build system
ocaml               4.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1      Official release 4.08.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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-addition-chains.0.4 coq.dev
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-addition-chains.0.4 coq.dev
Return code
0
Duration
9 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-addition-chains.0.4 coq.dev
Return code
7936
Duration
1 m 0 s
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                    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.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler    4.08.1      Official release 4.08.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.08.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.08.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.08.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.08.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.08.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.08.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-without-locality,deprecated]
- File "./theories/additions/Monoid_instances.v", line 27, 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_instances.v", line 36, characters 0-50:
- 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 41, characters 0-50:
- Warning: The default value for instance locality is currently "local" in a
- section and "global
[...] truncated
ty,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.08.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.08.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.08.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.08.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.08.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 11.272 secs (4.182u,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.08.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.08.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.5 | linux/x86_64 | ocaml-base-compiler.4.08.1 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.08.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-9735-335865.env
# output-file          ~/.opam/log/coq-addition-chains-9735-335865.out
### output ###
# (cd _build/default && /home/bench/.opam/ocaml-base-compiler.4.08.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)

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none