(2020-03-09 03:40:58 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.10.0 Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.0 Official release 4.09.0
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
name: "coq-mathcomp-finmap"
version: "1.2.0"
maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
homepage: "https://github.com/math-comp/finmap"
bug-reports: "https://github.com/math-comp/finmap/issues"
dev-repo: "git+https://github.com/math-comp/finmap.git"
license: "CeCILL-B"
build: [ make "-j" "%{jobs}%" ]
install: [ make "install" ]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/finmap'" ]
depends: [
"coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.9.0~") | (= "dev")}
"coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") }
]
tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"]
authors: [ "Cyril Cohen <cyril.cohen@inria.fr>" ]
synopsis: "Finite sets, finite maps, finitely supported functions, orders"
description: """
This library is an extension of mathematical component in order to
support finite sets and finite maps on choicetypes (rather that finite
types). This includes support for functions with finite support and
multisets. The library also contains a generic order and set libary,
which will be used to subsume notations for finite sets, eventually."""
url {
src: "https://github.com/math-comp/finmap/archive/1.2.0.tar.gz"
checksum: "sha256=fed84ffbb51701fa91705cac8473fc5138d50a8f9f556b4c96e0dcb45f5b54c7"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-mathcomp-finmap.1.2.0 coq.8.10.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 2h opam install -y --deps-only coq-mathcomp-finmap.1.2.0 coq.8.10.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-mathcomp-finmap.1.2.0 coq.8.10.0# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 coq 8.10.0 Formal proof management system coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning coq-mathcomp-ssreflect dev Small Scale Reflection num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.0 Official release 4.09.0 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.8.1 A library manager for OCaml [NOTE] Package coq is already installed (current version is 8.10.0). The following actions will be performed: - install coq-mathcomp-finmap 1.2.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-mathcomp-finmap.1.2.0: http] [coq-mathcomp-finmap.1.2.0] downloaded from https://github.com/math-comp/finmap/archive/1.2.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-mathcomp-finmap: make 4] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j" "4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-mathcomp-finmap.1.2.0) - /home/bench/.opam/ocaml-base-compiler.4.09.0/bin/coq_makefile -f _CoqProject -o Makefile.coq - make -f Makefile.coq - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-mathcomp-finmap.1.2.0' - COQDEP VFILES - COQC finmap.v - COQC order.v - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 21, characters 0-79: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./order.v", line 80, characters 0-33: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope order_scope.". [undeclared-scope,deprecated] - File "./order.v", line 365, characters 0-37: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope cpo_sort.". [undeclared-scope,deprecated] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 3, characters 0-72: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./finmap.v", line 158, characters 32-50: - Error: The reference sort_of_simpl_pred was not found in the current - environment. - - make[2]: *** [Makefile.coq:659: finmap.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - File "./order.v", line 1008, characters 0-157: - Warning: Notation "[ cblatticeType of _ for _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1010, characters 0-205: - Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in - scope form_scope. [notation-overridden,parsing] - File "./order.v", line 1013, characters 0-135: - Warning: Notation "[ cblatticeType of _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1015, characters 0-170: - Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1022, characters 0-12: - Warning: Notation "[ cblatticeType of _ for _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1022, characters 0-12: - Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in - scope form_scope. [notation-overridden,parsing] - File "./order.v", line 1022, characters 0-12: - Warning: Notation "[ cblatticeType of _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1022, characters 0-12: - Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1025, characters 0-26: - Warning: Notation "[ cblatticeType of _ for _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1025, characters 0-26: - Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in - scope form_scope. [notation-overridden,parsing] - File "./order.v", line 1025, characters 0-26: - Warning: Notation "[ cblatticeType of _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1025, characters 0-26: - Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 1653, characters 0-18: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 1656, characters 0-21: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 1671, characters 0-28: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 1824, characters 0-41: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2044, characters 0-25: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2113, characters 0-22: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2116, characters 0-25: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2153, characters 0-18: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2365, characters 0-23: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2476, characters 0-18: - Warning: Adding and removing hints in the core database implicitly is - deprecated. Please specify a hint database. - [implicit-core-hint-db,deprecated] - File "./order.v", line 2847, characters 0-25: - Warning: Notation "[ cblatticeType of _ for _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 2847, characters 0-25: - Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in - scope form_scope. [notation-overridden,parsing] - File "./order.v", line 2847, characters 0-25: - Warning: Notation "[ cblatticeType of _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 2847, characters 0-25: - Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 2849, characters 0-26: - Warning: Notation "[ cblatticeType of _ for _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 2849, characters 0-26: - Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in - scope form_scope. [notation-overridden,parsing] - File "./order.v", line 2849, characters 0-26: - Warning: Notation "[ cblatticeType of _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - File "./order.v", line 2849, characters 0-26: - Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope - form_scope. [notation-overridden,parsing] - make[1]: *** [Makefile.coq:321: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-mathcomp-finmap.1.2.0' - make: *** [Makefile.common:51: this-build] Error 2 [ERROR] The compilation of coq-mathcomp-finmap failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j 4". #=== ERROR while compiling coq-mathcomp-finmap.1.2.0 ==========================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-mathcomp-finmap.1.2.0 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j 4 # exit-code 2 # env-file ~/.opam/log/coq-mathcomp-finmap-3972-335865.env # output-file ~/.opam/log/coq-mathcomp-finmap-3972-335865.out ### output ### # [...] # File "./order.v", line 2849, characters 0-26: # Warning: Notation "[ cblatticeType of _ for _ with _ ]" was already used in # scope form_scope. [notation-overridden,parsing] # File "./order.v", line 2849, characters 0-26: # Warning: Notation "[ cblatticeType of _ ]" was already used in scope # form_scope. [notation-overridden,parsing] # File "./order.v", line 2849, characters 0-26: # Warning: Notation "[ cblatticeType of _ with _ ]" was already used in scope # form_scope. [notation-overridden,parsing] # make[1]: *** [Makefile.coq:321: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-mathcomp-finmap.1.2.0' # make: *** [Makefile.common:51: this-build] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-mathcomp-finmap 1.2.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-mathcomp-finmap.1.2.0 coq.8.10.0' failed.
No files were installed.
true