(2021-10-27 02:59:51 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 dune 2.9.1 Fast, portable, and opinionated build system ocaml 4.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled 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: "https://flocq.gitlabpages.inria.fr/" dev-repo: "git+https://gitlab.inria.fr/flocq/flocq.git" bug-reports: "https://gitlab.inria.fr/flocq/flocq/issues" license: "LGPL-3.0-or-later" build: [ ["autoconf"] {dev} ["./configure"] ["./remake" "-j%{jobs}%"] ] install: ["./remake" "install"] depends: [ "coq" {(>= "8.7" & < "8.11~") | >= "8.12"} "conf-autoconf" {build & dev} ("conf-g++" {build} | "conf-clang" {build}) ] tags: [ "keyword:floating-point arithmetic" "logpath:Flocq" "date:2021-06-18" ] authors: [ "Sylvie Boldo <sylvie.boldo@inria.fr>" "Guillaume Melquiond <guillaume.melquiond@inria.fr>" ] synopsis: "A formalization of floating-point arithmetic for the Coq system" url { src: "https://flocq.gitlabpages.inria.fr/releases/flocq-3.4.1.tar.gz" checksum: "sha512=7d8d9ea86a95f006466329f9abf90ebd0bea16c40a90010b921f6dcd1dfd7cb791087f2f6f8f5e9f13286432ffface7e2a6aeaf80b32b21bf9eb9d60ffa87e24" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-flocq.3.4.1 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 4h opam install -y --deps-only coq-flocq.3.4.1 coq.dev
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-flocq.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-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 dune 2.9.1 Fast, portable, and opinionated build system ocaml 4.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled 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-flocq 3.4.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-flocq.3.4.1: http] [coq-flocq.3.4.1] downloaded from https://flocq.gitlabpages.inria.fr/releases/flocq-3.4.1.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.12.0/.opam-switch/build/coq-flocq.3.4.1) - checking for coqc... /home/bench/.opam/ocaml-base-compiler.4.12.0/bin/coqc - checking Coq version... 8.15 - checking for coqdep... /home/bench/.opam/ocaml-base-compiler.4.12.0/bin/coqdep - checking for coqdoc... /home/bench/.opam/ocaml-base-compiler.4.12.0/bin/coqdoc - 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 - configure: building remake... - /usr/bin/ld: /tmp/ccuxgrFm.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 - config.status: creating src/IEEE754/SpecFloatCompat.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.12.0/.opam-switch/build/coq-flocq.3.4.1) - 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/IEEE754/SpecFloatCompat.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 - Finished src/Version.vo - Building src/Prop/Sterbenz.vo - Building src/Prop/Round_odd.vo - Building src/Prop/Double_rounding.vo - Building src/IEEE754/PrimFloat.vo - Building src/IEEE754/BinarySingleNaN.vo - Building src/IEEE754/Binary.vo - Finished src/IEEE754/SpecFloatCompat.vo - Building src/IEEE754/Bits.vo - Building src/Pff/Pff.vo - Building src/Pff/Pff2FlocqAux.vo - Building src/Pff/Pff2Flocq.vo - Finished src/Core/Zaux.vo - File "./src/Pff/Pff.v", line 1088, characters 0-30: - Warning: - New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing - [INR] : nat >-> R. [ambiguous-paths,typechecker] - Finished src/Core/Raux.vo - File "./src/Pff/Pff.v", line 1293, characters 0-16: - Warning: - New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing - [INR] : nat >-> R. [ambiguous-paths,typechecker] - Finished src/Core/Digits.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/Div.vo - Finished src/Calc/Sqrt.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/Prop/Relative.vo - Finished src/Prop/Round_odd.vo - Finished src/Prop/Plus_error.vo - Finished src/Calc/Round.vo - Finished src/Prop/Mult_error.vo - Finished src/Prop/Double_rounding.vo - Finished src/IEEE754/BinarySingleNaN.vo - Finished src/IEEE754/Binary.vo - File "./src/IEEE754/PrimFloat.v", line 257, characters 2-6: - Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead - [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 284, characters 55-59: - Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead - [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 324, characters 14-18: - Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead - [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 509, characters 10-18: - Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. - [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 510, characters 51-55: - Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead - [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 515, characters 8-21: - Warning: Notation of_int63_spec is deprecated since 8.14. - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 515, characters 8-21: - Warning: Notation of_int63_spec is deprecated since 8.14. - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 515, characters 8-21: - Warning: Notation of_int63_spec is deprecated since 8.14. - Use of_uint63_spec instead. [deprecated-syntactic-definition,deprecated] - File "./src/IEEE754/PrimFloat.v", line 521, characters 6-7: - Error: Syntax error: [term] expected after '=' (in [term]). - - Failed to build src/IEEE754/PrimFloat.vo - Failed to build all - Finished src/Prop/Div_sqrt_error.vo - File "./src/IEEE754/Bits.v", line 183, characters 0-79: - Warning: - The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead. - [conversion_at_with,deprecated] - Finished src/IEEE754/Bits.vo - Finished src/Pff/Pff.vo - File "./src/Pff/Pff2FlocqAux.v", line 23, characters 0-24: - Warning: - New coercion path [BinInt.Z.of_nat; Rdefinitions.IZR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R is ambiguous with existing - [Raxioms.INR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R. - [ambiguous-paths,typechecker] - Finished src/Pff/Pff2FlocqAux.vo - File "./src/Pff/Pff2Flocq.v", line 23, characters 0-32: - Warning: - New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing - [INR] : nat >-> R. [ambiguous-paths,typechecker] - Finished src/Pff/Pff2Flocq.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.4.1 ====================================# # context 2.0.8 | linux/x86_64 | ocaml-base-compiler.4.12.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.12.0/.opam-switch/build/coq-flocq.3.4.1 # command ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j4 # exit-code 1 # env-file ~/.opam/log/coq-flocq-25691-2dea01.env # output-file ~/.opam/log/coq-flocq-25691-2dea01.out ### output ### # [...] # Finished src/Pff/Pff.vo # File "./src/Pff/Pff2FlocqAux.v", line 23, characters 0-24: # Warning: # New coercion path [BinInt.Z.of_nat; Rdefinitions.IZR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R is ambiguous with existing # [Raxioms.INR] : nat >-> Rdefinitions.RbaseSymbolsImpl.R. # [ambiguous-paths,typechecker] # Finished src/Pff/Pff2FlocqAux.vo # File "./src/Pff/Pff2Flocq.v", line 23, characters 0-32: # Warning: # New coercion path [Z.of_nat; IZR] : nat >-> R is ambiguous with existing # [INR] : nat >-> R. [ambiguous-paths,typechecker] # Finished src/Pff/Pff2Flocq.vo <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-flocq 3.4.1 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-flocq.3.4.1 coq.dev' failed.
No files were installed.
true