(2020-04-14 10:21:03 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.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.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-flocq.3.2.0 coq.devopam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-flocq.3.2.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-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.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 dev). 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/cc2IzpzT.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/Relative.vo - Building src/Prop/Plus_error.vo - Building src/Prop/Sterbenz.vo - Building src/Prop/Round_odd.vo - Building src/Prop/Double_rounding.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 - Finished src/Version.vo - Finished src/Core/Zaux.vo - 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/Pff2FlocqAux.vo - Failed to build src/Pff/Pff2Flocq.vo - Failed to build all - Finished src/Core/Digits.vo - Finished src/Core/Raux.vo - Finished src/Core/Defs.vo - Finished src/Core/Float_prop.vo - Finished src/Core/Round_pred.vo - Finished src/Calc/Operations.vo - Finished src/Calc/Bracket.vo - Finished src/Core/Generic_fmt.vo - Finished src/Prop/Sterbenz.vo - Finished src/Calc/Sqrt.vo - Finished src/Calc/Div.vo - Finished src/Core/Ulp.vo - Finished src/Core/Round_NE.vo - Finished src/Core/FIX.vo - Finished src/Core/FLX.vo - Finished src/Core/FTZ.vo - Finished src/Core/FLT.vo - Finished src/Core/Core.vo - Finished src/Calc/Round.vo - Finished src/Prop/Relative.vo - Finished src/Prop/Round_odd.vo - Finished src/Prop/Plus_error.vo - Finished src/Prop/Mult_error.vo - Finished src/Prop/Div_sqrt_error.vo - Finished src/IEEE754/Binary.vo - Finished src/IEEE754/Bits.vo - 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-7130-2dea01.env # output-file ~/.opam/log/coq-flocq-7130-2dea01.out ### output ### # [...] # Finished src/Core/FTZ.vo # Finished src/Core/FLT.vo # Finished src/Core/Core.vo # Finished src/Calc/Round.vo # Finished src/Prop/Relative.vo # Finished src/Prop/Round_odd.vo # Finished src/Prop/Plus_error.vo # Finished src/Prop/Mult_error.vo # Finished src/Prop/Div_sqrt_error.vo # Finished src/IEEE754/Binary.vo # Finished src/IEEE754/Bits.vo # 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.dev' failed.
No files were installed.
true