This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to github.com/coq/opam-coq-archive. The list of black-listed packages is in black_list.rb.
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.13.1 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: [
"Pierre Roux <pierre.roux@onera.fr>"
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
]
homepage: "https://sourcesup.renater.fr/validsdp/"
dev-repo: "git+https://github.com/validsdp/validsdp.git"
bug-reports: "https://github.com/validsdp/validsdp/issues"
license: "LGPL-2.1-or-later"
build: [
["sh" "-c" "./configure"]
[make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
"coq" {>= "8.12" & < "8.16~"}
"coq-bignums"
"coq-flocq" {>= "3.3.0"}
"coq-coquelicot" {>= "3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {>= "1.12" & < "1.15~"}
"coq-mathcomp-analysis" {>= "0.3.4" & < "0.4~"}
"ocamlfind" {build}
"conf-autoconf" {build & dev}
]
synopsis: "LibValidSDP"
description: """
LibValidSDP is a library for the Coq formal proof assistant. It provides
results mostly about rounding errors in the Cholesky decomposition algorithm
used in the ValidSDP library which itself implements Coq tactics to prove
multivariate inequalities using SDP solvers.
Once installed, the following modules can be imported :
From libValidSDP Require Import Rstruct.v misc.v real_matrix.v bounded.v float_spec.v fsum.v fcmsum.v binary64.v cholesky.v float_infnan_spec.v binary64_infnan.v cholesky_infnan.v flx64.v zulp.v coqinterval_infnan.v.
"""
tags: [
"keyword:libValidSDP"
"keyword:ValidSDP"
"keyword:floating-point arithmetic"
"keyword:Cholesky decomposition"
"category:libValidSDP"
"category:Miscellaneous/Coq Extensions"
"logpath:libValidSDP"
]
authors: [
"Pierre Roux <pierre.roux@onera.fr>"
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
]
url {
src: "https://github.com/validsdp/validsdp/releases/download/v1.0.0/libvalidsdp-1.0.0.tar.gz"
checksum: "sha512=911a7f3dce7984d54ca8b33dac9532e52000273c8e7928e02010e14e44caa1b4f3903fe6cc3f1b33e0e5a25394e20872a7a88091585fd8b02ad25e7a55d3c71f"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-libvalidsdp.1.0.0 coq.8.13.1Dry 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 4h opam install -y --deps-only coq-libvalidsdp.1.0.0 coq.8.13.1# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.13.1 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
The following actions will be performed:
- install conf-perl 2
- install conf-g++ 1.0
- downgrade ocamlfind 1.9.5 to 1.9.1
- install ocaml-secondary-compiler 4.08.1-1
- install camlp5 7.14
- recompile zarith 1.12 [uses ocamlfind]
- install ocamlfind-secondary 1.9.1
- install dune 3.4.1
- install stdlib-shims 0.3.0
- install sexplib0 v0.15.0
- install seq 0.3.1
- install result 1.5
- install ppx_derivers 1.2.1
- install ocaml-compiler-libs v0.12.4
- install cppo 1.6.9
- install re 1.10.4
- install ppxlib 0.27.0
- install ppx_deriving 5.2.1
- install elpi 1.13.8
===== 17 to install | 1 to recompile | 1 to downgrade =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[cppo.1.6.9] downloaded from cache at https://opam.ocaml.org/cache
[camlp5.7.14] downloaded from cache at https://opam.ocaml.org/cache
[dune.3.4.1] downloaded from cache at https://opam.ocaml.org/cache
[elpi.1.13.8] downloaded from cache at https://opam.ocaml.org/cache
[ocaml-compiler-libs.v0.12.4] downloaded from cache at https://opam.ocaml.org/cache
[ocamlfind.1.9.1] downloaded from cache at https://opam.ocaml.org/cache
[ocaml-secondary-compiler.4.08.1-1] downloaded from cache at https://opam.ocaml.org/cache
[ppx_derivers.1.2.1] downloaded from cache at https://opam.ocaml.org/cache
[ocamlfind-secondary.1.9.1] downloaded from cache at https://opam.ocaml.org/cache
[ocaml-secondary-compiler.4.08.1-1/alt-signal-stack.patch] downloaded from https://opam.ocaml.org/cache
[ppx_deriving.5.2.1] downloaded from cache at https://opam.ocaml.org/cache
[result.1.5] downloaded from cache at https://opam.ocaml.org/cache
[ppxlib.0.27.0] downloaded from cache at https://opam.ocaml.org/cache
[re.1.10.4] downloaded from cache at https://opam.ocaml.org/cache
[seq.0.3.1] downloaded from cache at https://opam.ocaml.org/cache
[zarith.1.12] found in cache
[sexplib0.v0.15.0] downloaded from cache at https://opam.ocaml.org/cache
[stdlib-shims.0.3.0] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed conf-g++.1.0
-> installed conf-perl.2
[WARNING] While removing zarith.1.12: not removing files that changed since:
- lib/zarith/zarith_top.cma
- lib/zarith/zarith.h
- lib/zarith/zarith.cmxs
- lib/zarith/zarith.cmxa
- lib/zarith/zarith.cma
- lib/zarith/zarith.a
- lib/zarith/z.mli
- lib/zarith/z.cmx
- lib/zarith/z.cmti
- lib/zarith/z.cmi
- lib/zarith/q.mli
- lib/zarith/q.cmx
- lib/zarith/q.cmti
- lib/zarith/q.cmi
- lib/zarith/libzarith.a
- lib/zarith/big_int_Z.mli
- lib/zarith/big_int_Z.cmx
- lib/zarith/big_int_Z.cmti
- lib/zarith/big_int_Z.cmi
- lib/zarith/META
- lib/stublibs/dllzarith.so.owner
- lib/stublibs/dllzarith.so
[NOTE] While removing zarith.1.12: not removing non-empty directories:
- lib/zarith
-> removed zarith.1.12
[WARNING] While removing ocamlfind.1.9.5: not removing files that changed since:
- man/man5/site-lib.5
- man/man5/findlib.conf.5
- man/man5/META.5
- man/man1/ocamlfind.1
- lib/unix/META
- lib/toplevel/topfind
- lib/threads/META
- lib/str/META
- lib/stdlib/META
- lib/raw_spacetime/META
- lib/ocamldoc/META
- lib/ocaml/topfind
- lib/num/META
- lib/num-top/num_top_printers.cmi
- lib/num-top/num_top.cmi
- lib/num-top/num_top.cma
- lib/num-top/META
- lib/graphics/META
- lib/findlib/topfind.mli
- lib/findlib/topfind.cmi
- lib/findlib/ocaml_args.cmi
- lib/findlib/fl_topo.cmi
- lib/findlib/fl_split.cmi
- lib/findlib/fl_package_base.mli
- lib/findlib/fl_package_base.cmi
- lib/findlib/fl_metatoken.cmi
- lib/findlib/fl_metascanner.mli
- lib/findlib/fl_metascanner.cmi
- lib/findlib/fl_meta.cmi
- lib/findlib/fl_lint.cmi
- lib/findlib/fl_dynload.mli
- lib/findlib/fl_dynload.cmi
- lib/findlib/fl_args.cmi
- lib/findlib/findlib_top.cmxs
- lib/findlib/findlib_top.cmxa
- lib/findlib/findlib_top.cma
- lib/findlib/findlib_top.a
- lib/findlib/findlib_dynload.cmxs
- lib/findlib/findlib_dynload.cmxa
- lib/findlib/findlib_dynload.cma
- lib/findlib/findlib_dynload.a
- lib/findlib/findlib_config.ml
- lib/findlib/findlib_config.cmi
- lib/findlib/findlib.mli
- lib/findlib/findlib.cmxs
- lib/findlib/findlib.cmxa
- lib/findlib/findlib.cmi
- lib/findlib/findlib.cma
- lib/findlib/findlib.a
- lib/findlib/Makefile.packages
- lib/findlib/Makefile.config
- lib/findlib/META
- lib/findlib.conf
- lib/dynlink/META
- lib/compiler-libs/META
- lib/bytes/META
- lib/bigarray/META
[NOTE] While removing ocamlfind.1.9.5: not removing non-empty directories:
- lib/unix
- lib/threads
- lib/str
- lib/stdlib
- lib/raw_spacetime
- lib/ocamldoc
- lib/num-top
- lib/graphics
- lib/findlib
- lib/dynlink
- lib/compiler-libs
- lib/bytes
- lib/bigarray
-> removed ocamlfind.1.9.5
-> installed ocamlfind.1.9.1
[ERROR] The installation of zarith failed at "make install".
-> installed camlp5.7.14
-> installed ocaml-secondary-compiler.4.08.1-1
-> installed ocamlfind-secondary.1.9.1
-> installed dune.3.4.1
-> installed ocaml-compiler-libs.v0.12.4
-> installed ppx_derivers.1.2.1
-> installed result.1.5
-> installed seq.0.3.1
-> installed cppo.1.6.9
-> installed sexplib0.v0.15.0
-> installed stdlib-shims.0.3.0
-> installed re.1.10.4
-> installed ppxlib.0.27.0
-> installed ppx_deriving.5.2.1
-> installed elpi.1.13.8
#=== ERROR while installing zarith.1.12 =======================================#
# context 2.0.1 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://opam.ocaml.org#d079370f
# path ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/zarith.1.12
# command ~/.opam/opam-init/hooks/sandbox.sh install make install
# exit-code 2
# env-file ~/.opam/log/zarith-26050-6c557a.env
# output-file ~/.opam/log/zarith-26050-6c557a.out
### output ###
# ocamlfind install -destdir "/home/bench/.opam/ocaml-base-compiler.4.05.0/lib" zarith META zarith.cma libzarith.a z.cmi q.cmi big_int_Z.cmi zarith_top.cma z.mli zarith.cmxa z.cmx q.cmx big_int_Z.cmx zarith.cmxs zarith.h q.mli big_int_Z.mli zarith.a z.cmti q.cmti big_int_Z.cmti -optional dllzarith.so
# ocamlfind: Package zarith is already installed
# - (file /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/zarith/META already exists)
# make: *** [project.mak:115: install] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - install zarith 1.12
+-
+- The following changes have been performed
| - remove zarith 1.12
| - downgrade ocamlfind 1.9.5 to 1.9.1
| - install camlp5 7.14
| - install conf-g++ 1.0
| - install conf-perl 2
| - install cppo 1.6.9
| - install dune 3.4.1
| - install elpi 1.13.8
| - install ocaml-compiler-libs v0.12.4
| - install ocaml-secondary-compiler 4.08.1-1
| - install ocamlfind-secondary 1.9.1
| - install ppx_derivers 1.2.1
| - install ppx_deriving 5.2.1
| - install ppxlib 0.27.0
| - install re 1.10.4
| - install result 1.5
| - install seq 0.3.1
| - install sexplib0 v0.15.0
| - install stdlib-shims 0.3.0
+-
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
opam switch import "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/backup/state-20220926162619.export"
trueNo files were installed.
true