/
opam
93 lines (76 loc) · 2.31 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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
opam-version: "2.0"
maintainer: "alt-ergo@ocamlpro.com"
authors: "Alt-Ergo developers"
license: ["OCamlPro Non-Commercial License" "Apache-1.0+"]
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:
[
["autoconf"]
["./configure" "-prefix" "%{prefix}%"]
[make]
]
install:
[
[make "install" "MANDIR=%{man}%"]
]
remove: [
["autoconf"]
["./configure" "-prefix" "%{prefix}%"]
[make "uninstall" "MANDIR=%{man}%"]
]
depends: [
"ocaml" {>= "4.04.0"}
"num"
"zarith"
"camlzip" {< "1.08"}
"ocplib-simplex" {>= "0.4" & < "0.5"}
"menhir" {< "20211215"}
"conf-autoconf" {build}
]
depopts: [
"lablgtk"
"conf-gtksourceview"
]
conflicts: [
"alt-ergo" {< "2.0.0" }
"altgr-ergo" {< "2.0.0" }
"satML-plugin" {< "2.0.0" }
"profiler-plugin" {< "2.0.0" }
"fm-simplex-plugin" {< "2.0.0" }
]
patches:[
"makefile.user_replace_echo_by_printf.patch"
"patch_for_changes_in_num_library.patch"
]
synopsis: "Alt-Ergo, an SMT Solver for Software Verification"
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.
Since Alt-Ergo 2.0.0, this package provides the binaries (command-line
and GUI), the plugins and the preludes of Alt-Ergo.
Usage of the command-line:
```alt-ergo [options] <file.why>```
Usage of the GUI:
```altgr-ergo [options] <file.why>```
Usage of the satML plugin; an alternative SAT solver based on miniSAT:
```alt-ergo -sat-plugin satML-plugin.cmxs [other-options] <file.why>```
Usage of the FM-Simplex plugin, an alternative to Fourier-Motzkin algorithm for linear integer arithmetic
```alt-ergo -inequalities-plugin fm-simplex-plugin.cmxs [other-options] <file.why>```
Usage of the command-line with FPA reasoning:
```alt-ergo -use-fpa -prelude fpa-theory-2017-01-04-16h00.why [other-options] <file.why>```"""
extra-files: [
[
"patch_for_changes_in_num_library.patch"
"md5=ebb6d9ec5f99895f2b2b32dfbe56b9d3"
]
[
"makefile.user_replace_echo_by_printf.patch"
"md5=e2243201666098c1c2fc8a844ff53266"
]
]
url {
src:
"http://alt-ergo.ocamlpro.com/http/alt-ergo-2.0.0/alt-ergo-2.0.0.tar.gz"
checksum: "md5=eb8467734d97c4b1a25beb431f064e4f"
}