# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.8.0 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Hugo.Herbelin@inria.fr"
homepage: "http://mattam.org/research/russell/fingertrees.en.html"
license: "LGPL"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/FingerTree"]
depends: [
"coq" {>= "8.8" & < "8.9~"}
]
tags: [ "keyword: data structures" "keyword: dependent types" "keyword: Finger Trees" "category: Computer Science/Data Types and Data Structures" "date: 2009-02" ]
authors: [ "Matthieu Sozeau <mattam@mattam.org> [http://mattam.org]" ]
bug-reports: "https://github.com/coq-contribs/finger-tree/issues"
dev-repo: "git+https://github.com/coq-contribs/finger-tree.git"
synopsis: "Dependent Finger Trees"
description: """
A verified generic implementation of Finger Trees"""
flags: light-uninstall
url {
src: "https://github.com/coq-contribs/finger-tree/archive/v8.8.0.tar.gz"
checksum: "md5=f706927eba694ff80886621fab015dac"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-finger-tree.8.8.0 coq.8.8.0Dry 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-finger-tree.8.8.0 coq.8.8.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-finger-tree.8.8.0 coq.8.8.0# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.8.0 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
[NOTE] Package coq is already installed (current version is 8.8.0).
The following actions will be performed:
- install coq-finger-tree 8.8.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/1: [coq-finger-tree.8.8.0: http]
[coq-finger-tree.8.8.0] downloaded from https://github.com/coq-contribs/finger-tree/archive/v8.8.0.tar.gz
Processing 1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing 1/2: [coq-finger-tree: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0)
- coq_makefile -f Make -o Makefile.coq
- Warning: -extra and -extra-phony are deprecated.
- Warning: Write the extra targets in Makefile.coq.local.
-
- make -f Makefile.coq Makefile
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0'
- COQDEP VFILES
- make[1]: Nothing to be done for 'Makefile'.
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0'
- make -f Makefile.coq all
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0'
- COQC StringInterface.v
- COQC Reduce.v
- COQC Monoid.v
- COQC OrderedType.v
- COQC Modules.v
- COQC Notations.v
- File "./StringInterface.v", line 7, characters 0-49:
- Warning: Notation _ ~= _ was already used. [notation-overridden,parsing]
- COQC KeyMonoid.v
- File "./StringInterface.v", line 21, characters 2-14:
- Warning: Notation _ ~= _ was already used. [notation-overridden,parsing]
- File "./StringInterface.v", line 42, characters 2-14:
- Warning: Notation _ ~= _ was already used. [notation-overridden,parsing]
- COQC Digit.v
- COQC DigitModule.v
- File "./DigitModule.v", line 129, characters 4-78:
- Warning: Notation lparr _ rparr was already used.
- [notation-overridden,parsing]
- File "./DigitModule.v", line 155, characters 4-78:
- Warning: Notation lparr _ rparr was already used.
- [notation-overridden,parsing]
- COQC DependentFingerTreeModule.v
- File "./DependentFingerTreeModule.v", line 42, characters 4-50:
- Warning: Notation lparr _ rparr was already used.
- [notation-overridden,parsing]
- COQC DependentFingerTree.v
- File "./DependentFingerTree.v", line 529, characters 6-27:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./DependentFingerTreeModule.v", line 1209, characters 6-80:
- Warning: Notation lparr _ rparr was already used.
- [notation-overridden,parsing]
- Finished transaction in 26.581 secs (8.355u,0.026s) (successful)
- File "./DependentFingerTreeModule.v", line 1296, characters 6-80:
- Warning: Notation lparr _ rparr was already used.
- [notation-overridden,parsing]
- COQC FingerTreeModule.v
- COQC FingerTree.v
- COQC DependentSequence.v
- File "./FingerTreeModule.v", line 9, characters 0-45:
- Warning: There is no option Standard Proposition Elimination Names.
- [unknown-option,option]
- File "./FingerTree.v", line 10, characters 0-43:
- Warning: Implicit Arguments is deprecated; use Arguments instead
- [deprecated-implicit-arguments,deprecated]
- Inductive
- tree_split (p : Digits.v -> bool) (A : Type) (measure : A -> Digits.v)
- (i : Digits.v) : Digits.v -> Type :=
- mkTreeSplit : forall xsm : Digits.v,
- {xs : fingertree measure xsm |
- isEmpty xs \/ p (i cdot xsm) = false} ->
- forall (x : A) (ysm : Digits.v),
- {ys : fingertree measure ysm |
- isEmpty ys \/ p (i cdot xsm cdot measure x) = true} ->
- tree_split p measure i (xsm cdot measure x cdot ysm)
-
- For tree_split: Argument A is implicit
- For mkTreeSplit: Arguments A, measure, xsm, ysm are implicit
- For tree_split: Argument scopes are [function_scope type_scope function_scope
- _ _]
- For mkTreeSplit: Argument scopes are [function_scope type_scope
- function_scope _ _ _ _ _ _]
- File "./FingerTree.v", line 66, characters 2-22:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- COQC RopeModule.v
- File "./FingerTree.v", line 187, characters 4-40:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- COQC Sequence.v
- COQC PrioQueue.v
- COQC OrdSequence.v
- File "./RopeModule.v", line 12, characters 2-18:
- Warning: Notation _ ~= _ was already used. [notation-overridden,parsing]
- File "./RopeModule.v", line 34, characters 0-159:
- Warning: Notation _ ~= _ was already used. [notation-overridden,parsing]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.t"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.eq"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.eq_equiv"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.zero"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.succ"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.pred"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.S"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.P"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.succ_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.pred_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.pred_succ"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.bi_induction"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.one"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.two"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.one_succ"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.two_succ"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.lt"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.le"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.lt_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.lt_eq_cases"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.lt_irrefl"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.lt_succ_r"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.add"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.sub"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.mul"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.add_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.sub_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.mul_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.add_0_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.add_succ_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.sub_0_r"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.sub_succ_r"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.mul_0_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.mul_succ_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.max"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.max_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.max_r"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.min"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.min_l"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.min_r"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.pred_0"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.recursion"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.recursion_wd"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.recursion_0"!
- [masking-absolute-name,deprecated]
- File "./RopeModule.v", line 40, characters 2-11:
- Warning: Trying to mask the absolute name "NAxioms.recursion_succ"!
- [masking-absolute-name,deprecated]
- File "./Sequence.v", line 34, characters 2-23:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./DependentSequence.v", line 210, characters 2-38:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./DependentSequence.v", line 211, characters 2-48:
- Warning: Use of “Require” inside a section is deprecated.
- [require-in-section,deprecated]
- File "./DependentSequence.v", line 212, characters 2-55:
- Warning: Notation _ ::> _ was already used. [notation-overridden,parsing]
- File "./RopeModule.v", line 107, characters 2-89:
- Warning: sub is declared as a local axiom [local-declaration,scope]
- make -f Makefile.coq test
- cd extraction/ml/; rm -f *.ml *.mli *.cm* *.o; "coqc" -q -opt -R ../.. FingerTree Extract.v
- File "./Extract.v", line 22, characters 0-46:
- Warning: The following logical axioms were
- encountered: split_size view_right_size.
- Having invalid logical axiom in the
- environment when extracting may lead to incorrect or non-terminating ML
- terms.
- [extraction-logical-axiom,extraction]
- File "./Extract.v", line 23, characters 0-40:
- Warning: The following axiom must be realized in the extracted code:
- sub.
- [extraction-axiom-to-realize,extraction]
- File "./Extract.v", line 23, characters 0-40:
- Warning: The following logical axioms were
- encountered: split_size view_right_size.
- Having invalid logical axiom in the
- environment when extracting may lead to incorrect or non-terminating ML
- terms.
- [extraction-logical-axiom,extraction]
- cd extraction/ml/; make all
- ocamldep -native StringInterface.mli > ._ncdi/StringInterface.di
- ocamldep -native RopeModule.mli > ._ncdi/RopeModule.di
- ocamldep -native FingerTreeModule.mli > ._ncdi/FingerTreeModule.di
- ocamldep -native DigitModule.mli > ._ncdi/DigitModule.di
- ocamldep -native DependentFingerTreeModule.mli > ._ncdi/DependentFingerTreeModule.di
- ocamldep -native Modules.mli > ._ncdi/Modules.di
- ocamldep -native NDefOps.mli > ._ncdi/NDefOps.di
- ocamldep -native NAxioms.mli > ._ncdi/NAxioms.di
- ocamldep -native NBase.mli > ._ncdi/NBase.di
- ocamldep -native OrdersTac.mli > ._ncdi/OrdersTac.di
- ocamldep -native NZAxioms.mli > ._ncdi/NZAxioms.di
- ocamldep -native Orders.mli > ._ncdi/Orders.di
- ocamldep -native Equalities.mli > ._ncdi/Equalities.di
- ocamldep -native Specif.mli > ._ncdi/Specif.di
- ocamldep -native Sumbool.mli > ._ncdi/Sumbool.di
- ocamldep -native Bool.mli > ._ncdi/Bool.di
- ocamldep -native Nat.mli > ._ncdi/Nat.di
- ocamldep -native Logic.mli > ._ncdi/Logic.di
- ocamldep -native Datatypes.mli > ._ncdi/Datatypes.di
- ocamldep StringInterface.ml > ._d/StringInterface.d
- ocamldep RopeModule.ml > ._d/RopeModule.d
- ocamldep FingerTreeModule.ml > ._d/FingerTreeModule.d
- ocamldep DependentFingerTreeModule.ml > ._d/DependentFingerTreeModule.d
- ocamldep NDefOps.ml > ._d/NDefOps.d
- ocamldep NBase.ml > ._d/NBase.d
- ocamldep Modules.ml > ._d/Modules.d
- ocamldep NAxioms.ml > ._d/NAxioms.d
- ocamldep NZAxioms.ml > ._d/NZAxioms.d
- ocamldep DigitModule.ml > ._d/DigitModule.d
- ocamldep OrdersTac.ml > ._d/OrdersTac.d
- ocamldep Orders.ml > ._d/Orders.d
- ocamldep Equalities.ml > ._d/Equalities.d
- ocamldep Sumbool.ml > ._d/Sumbool.d
- ocamldep Specif.ml > ._d/Specif.d
- ocamldep Nat.ml > ._d/Nat.d
- ocamldep Datatypes.ml > ._d/Datatypes.d
- ocamldep Bool.ml > ._d/Bool.d
- ocamldep Logic.ml > ._d/Logic.d
- ocamlc -c -for-pack Fingertrees Datatypes.mli
- ocamlc -c -for-pack Fingertrees Sumbool.mli
- ocamlc -c -for-pack Fingertrees Logic.mli
- ocamlopt -c -for-pack Fingertrees -inline 1000 Decimal.ml
- ocamlc -c -for-pack Fingertrees Decimal.mli
- ocamlc -c -for-pack Fingertrees Bool.mli
- ocamlc -c -for-pack Fingertrees Modules.mli
- File "Decimal.ml", line 1:
- Error: Could not find the .cmi file for interface Decimal.mli.
- make[5]: *** [OCamlMakefile:966: Decimal.cmx] Error 2
- make[5]: *** Waiting for unfinished jobs....
- ocamlc -c -for-pack Fingertrees Specif.mli
- make[4]: *** [OCamlMakefile:744: native-code-library] Error 2
- make[3]: *** [Makefile.coq.conf:70: test] Error 2
- make[2]: *** [Makefile.coq.conf:66: post-all] Error 2
- make[1]: *** [Makefile.coq:319: all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0'
- make: *** [Makefile:2: all] Error 2
[ERROR] The compilation of coq-finger-tree failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j7".
#=== ERROR while compiling coq-finger-tree.8.8.0 ==============================#
# context 2.0.1 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code 2
# env-file ~/.opam/log/coq-finger-tree-18707-865888.env
# output-file ~/.opam/log/coq-finger-tree-18707-865888.out
### output ###
# [...]
# ocamlc -c -for-pack Fingertrees Modules.mli
# File "Decimal.ml", line 1:
# Error: Could not find the .cmi file for interface Decimal.mli.
# make[5]: *** [OCamlMakefile:966: Decimal.cmx] Error 2
# make[5]: *** Waiting for unfinished jobs....
# ocamlc -c -for-pack Fingertrees Specif.mli
# make[4]: *** [OCamlMakefile:744: native-code-library] Error 2
# make[3]: *** [Makefile.coq.conf:70: test] Error 2
# make[2]: *** [Makefile.coq.conf:66: post-all] Error 2
# make[1]: *** [Makefile.coq:319: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-finger-tree.8.8.0'
# make: *** [Makefile:2: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-finger-tree 8.8.0
+-
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-finger-tree.8.8.0 coq.8.8.0' failed.
No files were installed.
true