(2019-11-30 21:22:11 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 dev 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"
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"
build: [
["./configure"]
["./remake" "-j%{jobs}%"]
]
install: ["./remake" "install"]
depends: [
"coq" {>= "8.7"}
"coq-bignums"
"coq-flocq" {>= "3.0"}
"coq-mathcomp-ssreflect" {>= "1.6"}
"coq-coquelicot" {>= "3.0"}
]
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" ]
authors: [ "Guillaume Melquiond <guillaume.melquiond@inria.fr>" ]
synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically"
url {
src: "https://gforge.inria.fr/frs/download.php/file/38104/interval-3.4.1.tar.gz"
checksum: "sha512=676fd6f7d9f0ce949f30ebb00fd911353181ae29f9381ed786b9a105a26fa277c9b049dbe86f198f8e30b4a799546762becfc156f0868037a3c2f31efdb27a63"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-interval.3.4.1 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 2h opam install -y --deps-only coq-interval.3.4.1 coq.devopam list; echo; ulimit -Sv 4000000; timeout 1h opam install -y -v coq-interval.3.4.1 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-m4 1 Virtual package relying on m4 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 dune 2.0.0 Fast, portable, and opinionated build 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 [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-interval 3.4.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-interval.3.4.1: http] [coq-interval.3.4.1] downloaded from https://gforge.inria.fr/frs/download.php/file/38104/interval-3.4.1.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-interval: ./configure] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-interval.3.4.1) - 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.09.0/bin/coqc - checking for coqdep... /home/bench/.opam/ocaml-base-compiler.4.09.0/bin/coqdep - checking for Flocq... - yes - checking for Ssreflect... yes - checking for Coquelicot... - yes - checking for Bignums... - yes - configure: building remake... - /tmp/ccxD2qXv.o: In function `main': - remake.cpp:(.text.startup+0x890): 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.09.0/.opam-switch/build/coq-interval.3.4.1) - Building src/Interval_bigint_carrier.vo - Building src/Interval_bisect.vo - Building src/Interval_definitions.vo - Building src/Interval_float_sig.vo - Building src/Interval_xreal.vo - Building src/Interval_generic.vo - Building src/Interval_missing.vo - Building src/Interval_interval.vo - Building src/Interval_taylor_model.vo - Building src/Interval_xreal_derive.vo - Building src/coqapprox/coquelicot_compl.vo - Building src/Interval_generic_proof.vo - Building src/Interval_univariate.vo - Building src/coqapprox/Rstruct.vo - Building src/coqapprox/poly_datatypes.vo - Building src/coqapprox/interval_compl.vo - Building src/coqapprox/basic_rec.vo - Building src/coqapprox/taylor_thm.vo - Building src/coqapprox/seq_compl.vo - Building src/coqapprox/xreal_ssr_compat.vo - Building src/coqapprox/poly_bound.vo - Building src/coqapprox/poly_bound_quad.vo - Building src/coqapprox/taylor_model_int_sharp.vo - Building src/coqapprox/integral_pol.vo - Building src/coqapprox/taylor_poly.vo - Building src/Interval_specific_sig.vo - Building src/Interval_generic_ops.vo - Building src/Interval_integral.vo - Building src/Interval_interval_float.vo - Building src/Interval_interval_float_full.vo - Building src/Interval_transcend.vo - Building src/Interval_specific_ops.vo - Building src/Interval_stdz_carrier.vo - Building src/Interval_tactic.vo - Building src/bertrand.vo - Building src/various_integrals.vo - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/seq_compl.v", line 23, characters 0-197: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/Rstruct.v", line 24, characters 0-197: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - Finished src/coqapprox/Rstruct.vo - Finished src/coqapprox/seq_compl.vo - File "./src/Interval_missing.v", line 737, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_missing.v", line 740, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_missing.v", line 742, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_missing.v", line 764, characters 0-15: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/basic_rec.v", line 26, characters 0-249: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - Finished src/Interval_missing.vo - Finished src/coqapprox/basic_rec.vo - Finished src/Interval_xreal.vo - Finished src/coqapprox/taylor_thm.vo - Finished src/Interval_definitions.vo - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 24, characters 0-122: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 25, characters 0-32: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/xreal_ssr_compat.v", line 34, characters 0-33: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope ring_scope.". [undeclared-scope,deprecated] - File "./src/coqapprox/xreal_ssr_compat.v", line 35, characters 0-31: - Warning: Declaring a scope implicitly is deprecated; use in advance an - explicit "Declare Scope XR_scope.". [undeclared-scope,deprecated] - Finished src/coqapprox/xreal_ssr_compat.vo - Finished src/Interval_generic.vo - Finished src/Interval_interval.vo - Finished src/Interval_xreal_derive.vo - Finished src/Interval_float_sig.vo - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/Interval_generic_proof.v", line 29, characters 0-15: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 24, characters 0-174: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/interval_compl.v", line 26, characters 0-32: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - Finished src/Interval_univariate.vo - Finished src/coqapprox/interval_compl.vo - File "./src/Interval_generic_proof.v", line 1039, characters 8-33: - Error: - In environment - beta : radix - mode : rounding_mode - b : bool - p, n1 : positive - bP : (2 <= beta)%Z - H : (Z.pos n1 < Zdigits beta (Z.pos p))%Z - q := (Z.pos p / Z.pos (Z.to_pos beta ^ n1))%Z : Z - r := (Z.pos p mod Z.pos (Z.to_pos beta ^ n1))%Z : Z - U1 : (beta ^ (Zdigits beta (Z.pos p) - 1) <= Z.abs (Z.pos p))%Z - U2 : (Z.abs (Z.pos p) < beta ^ Zdigits beta (Z.pos p))%Z - Unable to unify "(?M3375 ?= Z.abs (Z.pos p))%Z = Gt -> False" with - "(0 ?= Z.pos (Z.to_pos beta ^ n1))%Z = Lt". - - Failed to build src/Interval_generic_proof.vo - Failed to build src/Interval_specific_ops.vo - Failed to build src/Interval_stdz_carrier.vo - Failed to build src/Interval_generic_ops.vo - Failed to build src/Interval_tactic.vo - Failed to build src/Interval_bigint_carrier.vo - Failed to build src/Interval_specific_sig.vo - Failed to build all - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope - fun_scope. [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ + _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ - _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ >= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ > _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ < _ <= _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ <= _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ < _ < _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ * _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 25, characters 0-96: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 26, characters 0-31: - Warning: Notation "_ ^ _" was already used in scope nat_scope. - [notation-overridden,parsing] - File "./src/coqapprox/poly_datatypes.v", line 257, characters 33-35: - Error: - In environment - u : U - The term "id" has type "R -> R" while it is expected to have type - "C.T -> C.T" (cannot unify "C.T" and "R"). - - Failed to build src/coqapprox/poly_datatypes.vo - Failed to build src/coqapprox/taylor_model_int_sharp.vo - Failed to build src/coqapprox/integral_pol.vo - Failed to build src/coqapprox/taylor_poly.vo - Failed to build src/coqapprox/coquelicot_compl.vo - Failed to build src/coqapprox/poly_bound.vo - Failed to build src/coqapprox/poly_bound_quad.vo - Failed to build src/Interval_integral.vo - Failed to build src/bertrand.vo - Failed to build src/various_integrals.vo - Failed to build src/Interval_bisect.vo - Failed to build src/Interval_taylor_model.vo - Finished src/Interval_interval_float.vo - File "./src/Interval_transcend.v", line 791, characters 50-65: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_transcend.v", line 798, characters 15-30: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_transcend.v", line 805, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_transcend.v", line 813, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - File "./src/Interval_transcend.v", line 819, characters 2-17: - Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. - [deprecated-tactic,deprecated] - Finished src/Interval_transcend.vo - Finished src/Interval_interval_float_full.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.3.4.1 =================================# # 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-interval.3.4.1 # command ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j4 # exit-code 1 # env-file ~/.opam/log/coq-interval-12050-2dea01.env # output-file ~/.opam/log/coq-interval-12050-2dea01.out ### output ### # [...] # [deprecated-tactic,deprecated] # File "./src/Interval_transcend.v", line 805, characters 2-17: # Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. # [deprecated-tactic,deprecated] # File "./src/Interval_transcend.v", line 813, characters 2-17: # Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. # [deprecated-tactic,deprecated] # File "./src/Interval_transcend.v", line 819, characters 2-17: # Warning: Tactic Fourier.fourier is deprecated since 8.9.0. Use lra instead. # [deprecated-tactic,deprecated] # Finished src/Interval_transcend.vo # Finished src/Interval_interval_float_full.vo <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-interval 3.4.1 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-interval.3.4.1 coq.dev' failed.
No files were installed.
true