Merge pull request #3337 from proux01/validsdp104

Add validsdp 1.0.4

Author: proux01

released/packages/coq-libvalidsdp/coq-libvalidsdp.1.0.4/opam

@@ -0,0 +1,53 @@
+opam-version: "2.0"
+maintainer: [
+  "Pierre Roux <[email protected]>"
+  "Érik Martin-Dorel <[email protected]>"
+]
+
+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: [
+  [make "-C" "libvalidsdp" "-j%{jobs}%"]
+]
+install: [make "-C" "libvalidsdp" "install"]
+depends: [
+  "coq" {>= "8.18" & < "8.21~"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.3.0"}
+  "coq-coquelicot" {>= "3.0"}
+  "coq-interval" {>= "4.0.0" & < "5~"}
+  "coq-mathcomp-field" {>= "2.1" & < "2.4~"}
+  ("coq-mathcomp-analysis" {>= "1.0.0" & < "1.7~"}
+  | "coq-mathcomp-reals-stdlib" {>= "1.8.0"})
+]
+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 <[email protected]>"
+  "Érik Martin-Dorel <[email protected]>"
+]
+url {
+  src: "https://github.com/validsdp/validsdp/releases/download/v1.0.4/validsdp-1.0.4.tar.gz"
+  checksum: "sha512=47f9c3b0f67cc41bec5dc97d7df4dcfec05443b2b799320b34efe0cc843f24ae11c1b6340c8c6103789338fccb5dc657729ff96e56d6d8c840d7f0dce4bf0cbd"
+}

released/packages/coq-validsdp/coq-validsdp.1.0.4/opam

@@ -0,0 +1,63 @@
+opam-version: "2.0"
+maintainer: [
+  "Érik Martin-Dorel <[email protected]>"
+  "Pierre Roux <[email protected]>"
+]
+
+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.18" & < "8.21~"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.3.0"}
+  "coq-interval" {>= "4.0.0" & < "5~"}
+  "coq-mathcomp-field" {>= "2.1" & < "2.4~"}
+  ("coq-mathcomp-analysis" {>= "1.0.0" & < "1.7~"}
+  | "coq-mathcomp-reals-stdlib" {>= "1.8.0"})
+  "coq-libvalidsdp" {= version}
+  "coq-mathcomp-multinomials" {>= "2.0"}
+  "coq-coqeal" {>= "2.0.2"}
+  "osdp" {>= "1.1.1"}
+  "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"
+  "category:ValidSDP"
+  "logpath:ValidSDP"
+]
+authors: [
+  "Érik Martin-Dorel <[email protected]>"
+  "Pierre Roux <[email protected]>"
+]
+url {
+  src: "https://github.com/validsdp/validsdp/releases/download/v1.0.4/validsdp-1.0.4.tar.gz"
+  checksum: "sha512=47f9c3b0f67cc41bec5dc97d7df4dcfec05443b2b799320b34efe0cc843f24ae11c1b6340c8c6103789338fccb5dc657729ff96e56d6d8c840d7f0dce4bf0cbd"
+}