-
Notifications
You must be signed in to change notification settings - Fork 1
/
coq-validsdp.opam
65 lines (60 loc) · 1.82 KB
/
coq-validsdp.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
58
59
60
61
62
63
64
65
opam-version: "2.0"
version: "dev"
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" "./autogen.sh"] {dev}
["sh" "-c" "./configure"]
[make "-j%{jobs}%"]
]
run-test: [make "-j%{jobs}%" "test"]
install: [make "install"]
depends: [
"ocaml"
"coq" {((>= "8.16" & < "8.20~") | (= "dev"))}
"coq-bignums"
"coq-flocq" {>= "3.3.0"}
"coq-interval" {>= "4.0.0" & < "5~"}
"coq-mathcomp-field" {(>= "2.0" & < "2.3~") | (= "dev")}
"coq-mathcomp-analysis" {>= "1.0.0"}
"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:ValidSDP"
"category:Miscellaneous/Coq Extensions"
"logpath:ValidSDP"
]
authors: [
"Érik Martin-Dorel <[email protected]>"
"Pierre Roux <[email protected]>"
]
#url {
# src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz"
# checksum: "sha256=TODO curl -L archive | sha256sum"
#}