Merge pull request #3283 from proux01/validsdp103

Add validsdp 1.0.3

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

@@ -0,0 +1,55 @@
+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: [
+  ["sh" "-c" "./configure"]
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.18" & < "8.20~"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.3.0"}
+  "coq-coquelicot" {>= "3.0"}
+  "coq-interval" {>= "4.0.0" & < "5~"}
+  "coq-mathcomp-field" {>= "2.1" & < "2.3~"}
+  "coq-mathcomp-analysis" {>= "1.0.0" & < "1.7~"}
+  "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 <[email protected]>"
+  "Érik Martin-Dorel <[email protected]>"
+]
+url {
+  src: "https://github.com/validsdp/validsdp/releases/download/v1.0.3/libvalidsdp-1.0.3.tar.gz"
+  checksum: "sha512=f378fb97889323fb8ef4531f2ca04e829e1d9fd486027967cfa5abae3bf213677f22b5bb056c40e30c5912ce6d1e8e025602024cbe91c8f024a579f2c2bd6d8f"
+}

released/packages/coq-validsdp/coq-validsdp.1.0.3/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.20~"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.3.0"}
+  "coq-interval" {>= "4.0.0" & < "5~"}
+  "coq-mathcomp-field" {>= "2.1" & < "2.3~"}
+  "coq-mathcomp-analysis" {>= "1.0.0" & < "1.7~"}
+  "coq-libvalidsdp" {= version}
+  "coq-mathcomp-multinomials" {>= "2.0"}
+  "coq-coqeal" {>= "2.0.2"}
+  "coq-paramcoq" {>= "1.1.0"}
+  "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.3/validsdp-1.0.3.tar.gz"
+  checksum: "sha512=c24db26f6457e5e5e17f8a5674f1885488661e031ec27c167690344c00f23f5bd534081814f364911217998a3c3ded672f8b785665f4f82ff3d3b6daa84e3388"
+}