this repo has no description
anil.recoil.org
1opam-version: "2.0"
2
3maintainer: "alt-ergo@ocamlpro.com"
4authors: "Alt-Ergo developers"
5license: ["OCamlPro Non-Commercial License" "Apache-1.0+"]
6homepage: "http://alt-ergo.ocamlpro.com/"
7bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
8dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
9build:
10[
11 ["autoconf"]
12 ["./configure" "-prefix" "%{prefix}%"]
13 [make]
14]
15
16install:
17[
18 [make "install" "MANDIR=%{man}%"]
19]
20
21remove: [
22 ["autoconf"]
23 ["./configure" "-prefix" "%{prefix}%"]
24 [make "uninstall" "MANDIR=%{man}%"]
25]
26
27depends: [
28 "ocaml" {>= "4.04.0"}
29 "num"
30 "zarith"
31 "camlzip" {< "1.08"}
32 "ocplib-simplex" {>= "0.4" & < "0.5"}
33 "menhir" {< "20211215"}
34 "conf-autoconf" {build}
35]
36depopts: [
37 "lablgtk"
38 "conf-gtksourceview"
39]
40
41conflicts: [
42 "alt-ergo" {< "2.0.0" }
43 "altgr-ergo" {< "2.0.0" }
44 "satML-plugin" {< "2.0.0" }
45 "profiler-plugin" {< "2.0.0" }
46 "fm-simplex-plugin" {< "2.0.0" }
47]
48
49patches:[
50 "makefile.user_replace_echo_by_printf.patch"
51 "patch_for_changes_in_num_library.patch"
52]
53synopsis: "Alt-Ergo, an SMT Solver for Software Verification"
54description: """
55Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.
56
57Since Alt-Ergo 2.0.0, this package provides the binaries (command-line
58and GUI), the plugins and the preludes of Alt-Ergo.
59
60Usage of the command-line:
61
62```alt-ergo [options] <file.why>```
63
64Usage of the GUI:
65
66```altgr-ergo [options] <file.why>```
67
68Usage of the satML plugin; an alternative SAT solver based on miniSAT:
69
70```alt-ergo -sat-plugin satML-plugin.cmxs [other-options] <file.why>```
71
72Usage of the FM-Simplex plugin, an alternative to Fourier-Motzkin algorithm for linear integer arithmetic
73
74```alt-ergo -inequalities-plugin fm-simplex-plugin.cmxs [other-options] <file.why>```
75
76Usage of the command-line with FPA reasoning:
77
78```alt-ergo -use-fpa -prelude fpa-theory-2017-01-04-16h00.why [other-options] <file.why>```"""
79url {
80 src:
81 "http://alt-ergo.ocamlpro.com/http/alt-ergo-2.0.0/alt-ergo-2.0.0.tar.gz"
82 checksum: [
83 "sha256=5fe64c7db492eac1404a82eeb6f83341df3f3793ddb604e575e90d24a3de64dc"
84 "md5=eb8467734d97c4b1a25beb431f064e4f"
85 ]
86}
87extra-source "patch_for_changes_in_num_library.patch" {
88 src:
89 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/alt-ergo/patch_for_changes_in_num_library.patch"
90 checksum: [
91 "sha256=a4ef9e003b0a14478df1d3e5d50035557d41e788be3e00961fc3a91178efe4ac"
92 "md5=ebb6d9ec5f99895f2b2b32dfbe56b9d3"
93 ]
94}
95extra-source "makefile.user_replace_echo_by_printf.patch" {
96 src:
97 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/alt-ergo/makefile.user_replace_echo_by_printf.patch"
98 checksum: [
99 "sha256=3221500ff3e9196325ba729521f13bfcbdec5fcc5297e9e3b9654b26f26850ca"
100 "md5=e2243201666098c1c2fc8a844ff53266"
101 ]
102}