# 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 4 Virtual package relying on a GMP lib system installation
coq 8.16.0 Formal proof management system
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.13.1 Official release 4.13.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.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}%"]
]
run-test: [make "-j%{jobs}%" "test"]
install: [make "install"]
depends: [
"ocaml"
"coq" {>= "8.14" & < "8.17~"}
"coq-bignums" {< "9~"}
"coq-flocq" {>= "3.3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {>= "1.13" & < "1.16~"}
"coq-mathcomp-analysis" {>= "0.3.5" & < "0.5.4~"}
"coq-libvalidsdp" {= "1.0.1"}
"coq-mathcomp-multinomials" {>= "1.2"}
"coq-coqeal" {>= "1.1.0"}
"coq-paramcoq" {>= "1.1.0"}
"osdp" {>= "1.0"}
"ocamlfind" {build}
"conf-autoconf" {build & dev}
]
synopsis: "ValidSDP"
description: """
ValidSDP is a library for the Coq formal proof assistant. It provides
reflexive tactics to prove multivariate inequalities involving
real-valued variables and rational constants, using SDP solvers as
untrusted back-ends and verified checkers based on libValidSDP.
Once installed, you can import the following modules:
From Coq Require Import Reals.
From ValidSDP Require Import validsdp.
"""
tags: [
"keyword:libValidSDP"
"keyword:ValidSDP"
"keyword:floating-point arithmetic"
"keyword:Cholesky decomposition"
"category:Miscellaneous/Coq Extensions"
"logpath:ValidSDP"
]
authors: [
"Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
"Pierre Roux <pierre.roux@onera.fr>"
]
url {
src: "https://github.com/validsdp/validsdp/releases/download/v1.0.1/validsdp-1.0.1.tar.gz"
checksum: "sha512=7857ceb8e7e04c2771f4264f6612e63f753bfca92a13a38bb058e817fc3dec60a6357992a74318a5bf617231c30beec3f2ea15c45243bc0b8186ccca043f8f82"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-validsdp.1.0.1 coq.8.16.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-validsdp.1.0.1 coq.8.16.0opam list; echo; timeout 4h opam install -y -v coq-validsdp.1.0.1 coq.8.16.0# Packages matching: installed # Name # Installed # Synopsis atd 2.15.0 Parser for the ATD data format description language atdgen 2.15.0 Generates efficient JSON serializers, deserializers and validators atdgen-runtime 2.15.0 Runtime library for code generated by atdgen atdts 2.15.0 TypeScript code generation for ATD APIs base-bigarray base base-threads base base-unix base biniou 1.2.2 Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve camlp-streams 5.0.1 The Stream and Genlex libraries for use with Camlp4 and Camlp5 cmdliner 1.2.0 Declarative definition of command line interfaces for OCaml conf-autoconf 0.1 Virtual package relying on autoconf installation conf-csdp 1 Virtual package relying on a CSDP binary system installation conf-findutils 1 Virtual package relying on findutils conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++) conf-gmp 4 Virtual package relying on a GMP lib system installation conf-which 1 Virtual package relying on which coq 8.16.0 Formal proof management system coq-bignums 8.16.0 Bignums, the Coq library of arbitrary large numbers coq-coqeal 1.1.3 CoqEAL - The Coq Effective Algebra Library coq-coquelicot 3.4.1 A Coq formalization of real analysis compatible with the standard library coq-elpi 1.16.0 Elpi extension language for Coq coq-flocq 4.1.3 A formalization of floating-point arithmetic for the Coq system coq-hierarchy-builder 1.6.0 High level commands to declare and evolve a hierarchy based on packed classes coq-interval 4.9.0 A Coq tactic for proving bounds on real-valued expressions automatically coq-libvalidsdp 1.0.1 LibValidSDP coq-mathcomp-algebra 1.15.0 Mathematical Components Library on Algebra coq-mathcomp-analysis 0.5.3 An analysis library for mathematical components coq-mathcomp-bigenough 1.0.1 A small library to do epsilon - N reasoning coq-mathcomp-field 1.15.0 Mathematical Components Library on Fields coq-mathcomp-fingroup 1.15.0 Mathematical Components Library on finite groups coq-mathcomp-finmap 1.5.2 Finite sets, finite maps, finitely supported functions coq-mathcomp-multinomials 1.6.0 A Multivariate polynomial Library for the Mathematical Components Library coq-mathcomp-real-closed 1.1.4 Mathematical Components Library on real closed fields coq-mathcomp-solvable 1.15.0 Mathematical Components Library on finite groups (II) coq-mathcomp-ssreflect 1.15.0 Small Scale Reflection coq-paramcoq 1.1.3+coq8.16 Plugin for generating parametricity statements to perform refinement proofs cppo 1.6.9 Code preprocessor like cpp for OCaml dune 3.13.0 Fast, portable, and opinionated build system easy-format 1.3.4 High-level and functional interface to the Format module of the OCaml standard library elpi 1.16.10 ELPI - Embeddable λProlog Interpreter menhir 20231231 An LR(1) parser generator menhirCST 20231231 Runtime support library for parsers generated by Menhir menhirLib 20231231 Runtime support library for parsers generated by Menhir menhirSdk 20231231 Compile-time library for auxiliary tools related to Menhir num 1.5 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.13.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.13.1 Official release 4.13.1 ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlbuild 0.14.3 OCamlbuild is a build system with builtin rules to easily build most OCaml projects ocamlfind 1.9.6 A library manager for OCaml ocplib-simplex 0.4 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions osdp 1.1.0 OCaml Interface to SDP solvers ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppxlib 0.31.0 Standard infrastructure for ppx rewriters re 1.11.0 RE is a regular expression library for OCaml result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib0 v0.16.0 Library containing the definition of S-expressions and some base converters stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler yojson 2.1.2 Yojson is an optimized parsing and printing library for the JSON format zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is 8.16.0). The following actions will be performed: - install coq-validsdp 1.0.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-validsdp.1.0.1: http] [coq-validsdp.1.0.1] downloaded from https://github.com/validsdp/validsdp/releases/download/v1.0.1/validsdp-1.0.1.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-validsdp: sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "sh" "-c" "./configure" (CWD=/home/bench/.opam/ocaml-base-compiler.4.13.1/.opam-switch/build/coq-validsdp.1.0.1) - checking for ocamlc... ocamlc - checking for coqc... coqc - checking Coq version... 8.16.0 - checking for ocamlfind... ocamlfind - checking for Ltac2... yes - checking for Mathcomp... - yes - checking for Mathcomp Analysis... - yes - checking for Flocq... - yes - checking for Coq-interval... - yes - checking for Multinomials... File "./conftest.v", line 1, characters 47-95: - Error: Cannot find a physical path bound to logical path - mpoly with prefix SsrMultinomials. - - no - configure: error: *** Unable to find library Multinomials >= 1.0 (https://github.com/math-comp/multinomials/) [ERROR] The compilation of coq-validsdp failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build sh -c ./configure". #=== ERROR while compiling coq-validsdp.1.0.1 =================================# # context 2.0.10 | linux/x86_64 | ocaml-base-compiler.4.13.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.13.1/.opam-switch/build/coq-validsdp.1.0.1 # command ~/.opam/opam-init/hooks/sandbox.sh build sh -c ./configure # exit-code 1 # env-file ~/.opam/log/coq-validsdp-14686-335865.env # output-file ~/.opam/log/coq-validsdp-14686-335865.out ### output ### # [...] # checking for ocamlfind... ocamlfind # checking for Ltac2... yes # checking for Mathcomp... yes # checking for Mathcomp Analysis... yes # checking for Flocq... yes # checking for Coq-interval... yes # checking for Multinomials... File "./conftest.v", line 1, characters 47-95: # Error: Cannot find a physical path bound to logical path # mpoly with prefix SsrMultinomials. # # no # configure: error: *** Unable to find library Multinomials >= 1.0 (https://github.com/math-comp/multinomials/) <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-validsdp 1.0.1 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-validsdp.1.0.1 coq.8.16.0' failed.
No files were installed.
true