(2020-08-26 04:03:56 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.12.0 Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.10.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.0 Official release 4.10.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://flocq.gforge.inria.fr/"
dev-repo: "git+https://gitlab.inria.fr/flocq/flocq.git"
bug-reports: "https://gitlab.inria.fr/flocq/flocq/issues"
license: "LGPL 3"
build: [
["./configure"]
["./remake" "-j%{jobs}%"]
]
install: ["./remake" "install"]
depends: [
"coq" {>= "8.7"}
]
tags: [ "keyword:floating point arithmetic" ]
authors: [ "Sylvie Boldo <sylvie.boldo@inria.fr>" "Guillaume Melquiond <guillaume.melquiond@inria.fr>" ]
synopsis: "A floating-point formalization for the Coq system"
url {
src: "https://gforge.inria.fr/frs/download.php/file/38103/flocq-3.2.0.tar.gz"
checksum: "sha512=de737c9dab61115cb8f0e145f6e8d7e0ec8c1de97afec77079a30fb3948eec2afa0e5b0568bd5a3f82939a2c18befa62073adfbbdcac31ab7775d8cc874f026a"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-flocq.3.2.0 coq.8.12.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-flocq.3.2.0 coq.8.12.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-flocq.3.2.0 coq.8.12.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.12.0 Formal proof management system num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.0 Official release 4.10.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.12.0). The following actions will be performed: - install coq-flocq 3.2.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-flocq.3.2.0: http] [coq-flocq.3.2.0] downloaded from https://gforge.inria.fr/frs/download.php/file/38103/flocq-3.2.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-flocq: ./configure] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-flocq.3.2.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.0/bin/coqc - checking for coqdep... /home/bench/.opam/ocaml-base-compiler.4.10.0/bin/coqdep - checking for coqdoc... /home/bench/.opam/ocaml-base-compiler.4.10.0/bin/coqdoc - configure: building remake... - /usr/bin/ld: /tmp/ccHl7re6.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 - config.status: creating src/Version.v Processing 1/2: [coq-flocq: ./remake] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./remake" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-flocq.3.2.0) - Building src/Version.vo - Building src/Core/Raux.vo - Building src/Core/Zaux.vo - Building src/Core/Defs.vo - Building src/Core/Digits.vo - Building src/Core/Float_prop.vo - Building src/Core/FIX.vo - Building src/Core/FLT.vo - Building src/Core/Generic_fmt.vo - Building src/Core/FLX.vo - Building src/Core/Round_pred.vo - Building src/Core/Round_NE.vo - Building src/Core/Ulp.vo - Building src/Core/FTZ.vo - Building src/Core/Core.vo - Building src/Calc/Bracket.vo - Building src/Calc/Div.vo - Building src/Calc/Operations.vo - Building src/Calc/Round.vo - Building src/Calc/Sqrt.vo - Building src/Prop/Div_sqrt_error.vo - Building src/Prop/Mult_error.vo - Building src/Prop/Plus_error.vo - Building src/Prop/Relative.vo - Building src/Prop/Sterbenz.vo - Building src/Prop/Round_odd.vo - Building src/Prop/Double_rounding.vo - Finished src/Version.vo - Building src/IEEE754/Binary.vo - Building src/IEEE754/Bits.vo - Building src/Pff/Pff.vo - Building src/Pff/Pff2FlocqAux.vo - Building src/Pff/Pff2Flocq.vo - File "./src/Core/Zaux.v", line 265, characters 0-18: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Zaux.v", line 285, characters 0-17: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Zaux.v", line 305, characters 16-22: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Zaux.v", line 423, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Zaux.v", line 440, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - Finished src/Core/Zaux.vo - File "./src/Core/Digits.v", line 44, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 46, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 188, characters 0-31: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Pff/Pff.v", line 843, characters 0-41: - Error: No such goal. - - Failed to build src/Pff/Pff.vo - Failed to build src/Pff/Pff2Flocq.vo - Failed to build all - Failed to build src/Pff/Pff2FlocqAux.vo - File "./src/Core/Digits.v", line 194, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 194, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 206, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 230, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 230, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 452, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 495, characters 0-29: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 506, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 535, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 592, characters 0-13: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 593, characters 0-39: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 597, characters 0-13: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 601, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 627, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 629, characters 0-27: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 634, characters 0-32: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 649, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 669, characters 0-30: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 688, characters 0-40: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 688, characters 0-40: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 692, characters 0-30: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 696, characters 0-40: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 716, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Raux.v", line 1308, characters 11-17: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Raux.v", line 1310, characters 14-20: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Raux.v", line 1457, characters 0-32: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 791, characters 0-18: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Raux.v", line 1759, characters 0-25: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 931, characters 0-13: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 941, characters 42-48: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 954, characters 0-19: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 964, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Core/Digits.v", line 985, characters 0-6: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecate [...] truncated E754/Bits.v", line 248, characters 7-55: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 248, characters 7-55: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 248, characters 7-55: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 256, characters 18-30: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 266, characters 0-21: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 272, characters 0-25: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 273, characters 28-42: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 285, characters 0-14: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 290, characters 0-14: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 308, characters 2-25: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 316, characters 2-25: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 324, characters 6-23: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 328, characters 6-50: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 328, characters 6-50: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 330, characters 6-20: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 332, characters 6-30: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 334, characters 6-44: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 336, characters 6-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 336, characters 6-51: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 339, characters 6-23: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4215, characters 6-123: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 373, characters 2-21: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 392, characters 0-20: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 400, characters 18-39: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 402, characters 0-19: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4228, characters 4-50: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4236, characters 4-33: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 409, characters 0-60: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 413, characters 28-34: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 455, characters 0-29: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 474, characters 0-29: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 479, characters 0-19: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 506, characters 18-32: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 512, characters 18-32: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4382, characters 0-30: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4383, characters 0-47: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4428, characters 2-8: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 525, characters 0-14: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 530, characters 0-19: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4433, characters 2-8: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 537, characters 0-22: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 550, characters 0-22: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4438, characters 2-8: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 591, characters 8-20: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 596, characters 0-21: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/IEEE754/Bits.v", line 604, characters 0-28: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4443, characters 2-8: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4448, characters 2-8: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - Finished src/IEEE754/Bits.vo - File "./src/Prop/Double_rounding.v", line 4494, characters 2-94: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4497, characters 2-188: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4502, characters 2-196: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4507, characters 2-188: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - File "./src/Prop/Double_rounding.v", line 4512, characters 2-188: - Warning: omega is deprecated since 8.12; use “lia” instead. - [omega-is-deprecated,deprecated] - Finished src/Prop/Double_rounding.vo [ERROR] The compilation of coq-flocq failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build ./remake -j4". #=== ERROR while compiling coq-flocq.3.2.0 ====================================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.10.0/.opam-switch/build/coq-flocq.3.2.0 # command ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j4 # exit-code 1 # env-file ~/.opam/log/coq-flocq-20199-2dea01.env # output-file ~/.opam/log/coq-flocq-20199-2dea01.out ### output ### # [...] # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Prop/Double_rounding.v", line 4502, characters 2-196: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Prop/Double_rounding.v", line 4507, characters 2-188: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # File "./src/Prop/Double_rounding.v", line 4512, characters 2-188: # Warning: omega is deprecated since 8.12; use “lia” instead. # [omega-is-deprecated,deprecated] # Finished src/Prop/Double_rounding.vo <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-flocq 3.2.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-flocq.3.2.0 coq.8.12.0' failed. The middle of the output is truncated (maximum 20000 characters)
No files were installed.
true