« Up

libvalidsdp dev Error 🔥

Context

# 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.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1      Official release 4.08.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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-libvalidsdp.dev coq.8.10.dev
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-libvalidsdp.dev coq.8.10.dev
Return code
0
Duration
34 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y coq-libvalidsdp.dev coq.8.10.dev
Return code
7936
Duration
1 m 0 s
Output
# 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.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler    4.08.1      Official release 4.08.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.5 | linux/x86_64 | ocaml-base-compiler.4.08.1 | file:///home/bench/run/opam-coq-archive/extra-dev
# path                 ~/.opam/ocaml-base-compiler.4.08.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-16064-e4db2f.env
# output-file          ~/.opam/log/coq-libvalidsdp-16064-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

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none