# 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.10.dev Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
# 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" "cd libvalidsdp && ./autogen.sh && ./configure"]
[make "-C" "libvalidsdp" "-j%{jobs}%"]
]
install: [make "-C" "libvalidsdp" "install"]
depends: [
"ocaml"
"coq" {>= "8.7" & < "8.11~"}
"coq-bignums"
"coq-flocq" {>= "3.1.0"}
"coq-coquelicot" {>= "3.0"}
"coq-interval" {>= "3.4.0" & < "4~"}
"coq-mathcomp-field" {>= "1.8" & < "1.10~"}
"ocamlfind" {build}
"conf-autoconf" {build}
]
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: "git+https://github.com/validsdp/validsdp.git#master"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-libvalidsdp.dev coq.8.10.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-libvalidsdp.dev coq.8.10.devopam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y coq-libvalidsdp.dev coq.8.10.dev# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-autoconf 0.1 Virtual package relying on autoconf installation conf-findutils 1 Virtual package relying on findutils conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++) conf-m4 1 Virtual package relying on m4 conf-which 1 Virtual package relying on which coq 8.10.dev Formal proof management system coq-bignums 8.10.0 Bignums, the Coq library of arbitrary large numbers coq-coquelicot 3.1.0 A Coq formalization of real analysis compatible with the standard library coq-flocq 3.3.1 A formalization of floating-point arithmetic for the Coq system coq-interval 3.4.2 A Coq tactic for proving bounds on real-valued expressions automatically coq-mathcomp-algebra 1.9.0 Mathematical Components Library on Algebra coq-mathcomp-field 1.9.0 Mathematical Components Library on Fields coq-mathcomp-fingroup 1.9.0 Mathematical Components Library on finite groups coq-mathcomp-solvable 1.9.0 Mathematical Components Library on finite groups (II) coq-mathcomp-ssreflect 1.9.0 Small Scale Reflection num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 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.10.dev). The following actions will be performed: - install coq-libvalidsdp dev <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-libvalidsdp.dev] synchronised from git+https://github.com/validsdp/validsdp.git#master <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ERROR] The compilation of coq-libvalidsdp failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build sh -c cd libvalidsdp && ./autogen.sh && ./configure". #=== ERROR while compiling coq-libvalidsdp.dev ================================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.09.1 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.4.09.1/.opam-switch/build/coq-libvalidsdp.dev # command ~/.opam/opam-init/hooks/sandbox.sh build sh -c cd libvalidsdp && ./autogen.sh && ./configure # exit-code 1 # env-file ~/.opam/log/coq-libvalidsdp-25301-e4db2f.env # output-file ~/.opam/log/coq-libvalidsdp-25301-e4db2f.out ### output ### # checking for ocamlc... ocamlc # checking for coqc... coqc # checking Coq version... 8.10.2 # configure: error: must be at least 8.11. <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-libvalidsdp dev +- - No changes have been performed # Run eval $(opam env) to update the current shell environment
No files were installed.
true