-
Notifications
You must be signed in to change notification settings - Fork 1.1k
/
opam
46 lines (41 loc) · 1.49 KB
/
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
opam-version: "2.0"
maintainer: "alt-ergo@ocamlpro.com"
authors: "Alt-Ergo developers"
license: "OCamlPro Non-Commercial License"
homepage: "http://alt-ergo.ocamlpro.com/"
bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
build:
[
["./configure" "-prefix" "%{prefix}%"]
[make "fm-simplex"]
]
install:
[
[make "install-fm-simplex" "MANDIR=%{man}%/man1"]
]
remove:
[
["rm" "%{prefix}%/lib/alt-ergo/plugins/fm-simplex-plugin.cmxs"]
]
depends: [
"ocaml"
"zarith"
"alt-ergo" {= "1.01"}
"conf-autoconf"
]
messages: [ "This release is too old. Please consider using version 1.30 that fixes many soundness bugs and brings a lot of improvements" ]
synopsis:
"Alt-Ergo, an SMT Solver for Software Verification: FM-Simplex Plugin"
description: """
Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.
This package provides the FM-Simplex plugin for Alt-Ergo: an alternative to Fourier-Motzkin elimination algorithm described in [this paper](https://hal.archives-ouvertes.fr/hal-00687640).
usage: alt-ergo -inequalities-plugin fm-simplex-plugin.cmxs [other-options] <file.why>"""
flags: light-uninstall
url {
src: "http://alt-ergo.ocamlpro.com/http/alt-ergo-1.01/alt-ergo-1.01.tar.gz"
checksum: [
"sha256=d51a9833acf265d475408cde04e9beb75f950355580b9c73292ffbfbebf280eb"
"md5=9fbf8e42bec2a171dc9422f9dcea9519"
]
}