-
Notifications
You must be signed in to change notification settings - Fork 1
/
coq-libvalidsdp.opam
57 lines (53 loc) · 1.89 KB
/
coq-libvalidsdp.opam
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
opam-version: "2.0"
version: "dev"
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" "cd libvalidsdp && ./autogen.sh"] {dev}
["sh" "-c" "cd libvalidsdp && ./configure"]
[make "-C" "libvalidsdp" "-j%{jobs}%"]
]
install: [make "-C" "libvalidsdp" "install"]
depends: [
"coq" {((>= "8.16" & < "8.20~") | (= "dev"))}
"coq-bignums"
"coq-flocq" {>= "3.3.0"}
"coq-coquelicot" {>= "3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {(>= "2.0" & < "2.3~") | (= "dev")}
"coq-mathcomp-analysis" {>= "1.0.0"}
"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/v0.8.0/libvalidsdp-0.8.0.tar.gz
# checksum: "sha256=TODO curl -L archive | sha256sum"
#}