(2021-04-06 20:47: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-gmp 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "guillaume.melquiond@inria.fr" homepage: "http://coq-interval.gforge.inria.fr/" dev-repo: "git+https://gitlab.inria.fr/coqinterval/interval.git" bug-reports: "https://gitlab.inria.fr/coqinterval/interval/issues" license: "CeCILL-C" patches: [ "remake.patch" ] build: [ ["autoconf"] {dev} ["./configure"] ["./remake" "-j%{jobs}%"] ] install: ["./remake" "install"] depends: [ "coq" {>= "8.8"} "coq-bignums" "coq-flocq" {>= "3.1"} "coq-mathcomp-ssreflect" {>= "1.6"} "coq-coquelicot" {>= "3.0"} "conf-autoconf" {build & dev} ("conf-g++" {build} | "conf-clang" {build}) ] tags: [ "keyword:interval arithmetic" "keyword:decision procedure" "keyword:floating-point arithmetic" "keyword:reflexive tactic" "keyword:Taylor models" "category:Mathematics/Real Calculus and Topology" "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" "logpath:Interval" "date:2020-11-25" ] authors: [ "Guillaume Melquiond <guillaume.melquiond@inria.fr>" "Érik Martin-Dorel <erik.martin-dorel@irit.fr>" "Pierre Roux <pierre.roux@onera.fr>" "Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>" ] synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically" url { src: "https://gforge.inria.fr/frs/download.php/file/38379/interval-4.1.0.tar.gz" checksum: "sha512=74f94e1d5a1f9b6562a84e5e3addced7bb2a36fd38b2ed6bcbbd0493ba9c4d470bbb2b5d07e3b322d9a5736bc18358966b4101e0ab9b0b18c2cab4efbb7b8c08" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-interval.4.1.0 coq.dev
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-interval.4.1.0 coq.dev
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-interval.4.1.0 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-g++ 1.0 Virtual package relying on the g++ compiler (for C++) conf-gmp 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system coq-bignums dev Bignums, the Coq library of arbitrary large numbers coq-coquelicot dev A Coq formalization of real analysis compatible with the standard library. coq-flocq dev A floating-point formalization for the Coq system coq-mathcomp-ssreflect dev Small Scale Reflection num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 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-interval 4.1.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-interval.4.1.0: http] [coq-interval.4.1.0] downloaded from https://gforge.inria.fr/frs/download.php/file/38379/interval-4.1.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-interval: patch] Processing 1/2: [coq-interval: ./configure] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-interval.4.1.0) - checking for g++... g++ - checking whether the C++ compiler works... yes - checking for C++ compiler default output file name... a.out - checking for suffix of executables... - - checking whether we are cross compiling... no - checking for suffix of object files... o - checking whether we are using the GNU C++ compiler... yes - checking whether g++ accepts -g... yes - checking for coqc... /home/bench/.opam/ocaml-base-compiler.4.10.1/bin/coqc - checking Coq version... 8.14 - checking for coqdep... /home/bench/.opam/ocaml-base-compiler.4.10.1/bin/coqdep - checking for coqdoc... /home/bench/.opam/ocaml-base-compiler.4.10.1/bin/coqdoc - checking for Flocq... - yes - checking for primitive floats... - yes - checking for Ssreflect... yes - checking for Coquelicot... - yes - checking for Bignums... - yes - configure: building remake... - /usr/bin/ld: /tmp/ccagffi4.o: in function `main': - remake.cpp:(.text.startup+0xae0): warning: the use of `tempnam' is dangerous, better use `mkstemp' - configure: creating ./config.status - config.status: creating Remakefile Processing 1/2: [coq-interval: ./remake] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./remake" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-interval.4.1.0) - Building src/Tactic_float.v - Finished src/Tactic_float.v - Building src/Tactic.vo - Building src/Eval/Eval.vo - Building src/Eval/Prog.vo - Building src/Eval/Reify.vo - Building src/Eval/Tree.vo - Building src/Float/Basic.vo - Building src/Float/Generic.vo - Building src/Float/Generic_ops.vo - Building src/Float/Generic_proof.vo - Building src/Float/Specific_bigint.vo - Building src/Float/Specific_ops.vo - Building src/Float/Specific_sig.vo - Building src/Float/Specific_stdz.vo - Building src/Float/Sig.vo - Building src/Integral/Bertrand.vo - Building src/Integral/Integral.vo - Building src/Integral/Priority.vo - Building src/Integral/Refine.vo - Building src/Interval/Interval.vo - Building src/Interval/Interval_compl.vo - Building src/Interval/Float.vo - Building src/Interval/Float_full.vo - Building src/Interval/Transcend.vo - Building src/Interval/Univariate_sig.vo - Building src/Missing/Coquelicot.vo - Building src/Missing/MathComp.vo - Building src/Missing/Stdlib.vo - Building src/Poly/Basic_rec.vo - Building src/Poly/Bound.vo - Building src/Poly/Bound_quad.vo - Building src/Poly/Datatypes.vo - Building src/Poly/Taylor_model.vo - Building src/Poly/Taylor_model_sharp.vo - Building src/Poly/Taylor_poly.vo - Building src/Real/Taylor.vo - Building src/Real/Xreal.vo - Building src/Real/Xreal_derive.vo - Building src/Tactic_float.vo - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Missing/MathComp.v", line 24, characters 0-88: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Integral/Priority.v", line 21, characters 0-62: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - Building src/Float/Primitive_ops.vo - File "./src/Integral/Priority.v", line 527, characters 0-118: - Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] - Finished src/Missing/MathComp.vo - Finished src/Integral/Priority.vo - File "./src/Missing/Stdlib.v", line 833, characters 8-13: - Error: The reference omega was not found in the current environment. - - Failed to build src/Missing/Stdlib.vo - Failed to build src/Real/Taylor.vo - Failed to build src/Real/Xreal.vo - Failed to build src/Real/Xreal_derive.vo - Failed to build src/Poly/Taylor_model.vo - Failed to build src/Poly/Taylor_model_sharp.vo - Failed to build src/Float/Primitive_ops.vo - Failed to build src/Poly/Bound_quad.vo - Failed to build src/Poly/Datatypes.vo - Failed to build src/Tactic_float.vo - Failed to build src/Missing/Coquelicot.vo - Failed to build src/Poly/Bound.vo - Failed to build src/Interval/Transcend.vo - Failed to build src/Interval/Univariate_sig.vo - Failed to build src/Interval/Float.vo - Failed to build src/Interval/Float_full.vo - Failed to build src/Interval/Interval.vo - Failed to build src/Interval/Interval_compl.vo - Failed to build src/Integral/Bertrand.vo - Failed to build src/Integral/Refine.vo - Failed to build src/Float/Sig.vo - Failed to build src/Integral/Integral.vo - Failed to build src/Float/Generic.vo - Failed to build src/Float/Specific_ops.vo - Failed to build src/Float/Specific_sig.vo - Failed to build src/Float/Specific_stdz.vo - Failed to build src/Float/Generic_proof.vo - Failed to build src/Float/Specific_bigint.vo - Failed to build src/Float/Basic.vo - Failed to build src/Float/Generic_ops.vo - Failed to build src/Tactic.vo - Failed to build src/Eval/Reify.vo - Failed to build src/Eval/Eval.vo - Failed to build src/Eval/Tree.vo - Failed to build all - Failed to build src/Eval/Prog.vo - Failed to build src/Poly/Taylor_poly.vo - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 24, characters 0-102: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/Poly/Basic_rec.v", line 154, characters 0-10: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 154, characters 0-10: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 164, characters 2-62: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 164, characters 2-62: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 191, characters 2-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 191, characters 2-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 192, characters 2-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 192, characters 2-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 490, characters 0-10: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 490, characters 0-10: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 500, characters 2-35: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 500, characters 2-35: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 526, characters 2-54: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 526, characters 2-54: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 527, characters 2-54: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Poly/Basic_rec.v", line 527, characters 2-54: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - Finished src/Poly/Basic_rec.vo [ERROR] The compilation of coq-interval failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build ./remake -j4". #=== ERROR while compiling coq-interval.4.1.0 =================================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-interval.4.1.0 # command ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j4 # exit-code 1 # env-file ~/.opam/log/coq-interval-3722-d474c2.env # output-file ~/.opam/log/coq-interval-3722-d474c2.out ### output ### # [...] # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Poly/Basic_rec.v", line 526, characters 2-54: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Poly/Basic_rec.v", line 527, characters 2-54: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Poly/Basic_rec.v", line 527, characters 2-54: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # Finished src/Poly/Basic_rec.vo <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-interval 4.1.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-interval.4.1.0 coq.dev' failed.
No files were installed.
true