provers-detection-data.conf.in 2.76 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
[ATP alt-ergo]
name = "Alt-Ergo"
3
exec = "ergo"
4
exec = "alt-ergo"
MARCHE Claude's avatar
MARCHE Claude committed
5
exec = "alt-ergo-0.91"
MARCHE Claude's avatar
MARCHE Claude committed
6
version_switch = "-version"
7
version_regexp = ".*Ergo \\([^ \n]*\\)"
8
version_ok = "0.92.2"
MARCHE Claude's avatar
MARCHE Claude committed
9
version_ok = "0.92.1"
10
11
version_ok = "0.92"
version_ok = "0.91"
MARCHE Claude's avatar
MARCHE Claude committed
12
version_old = "0.9"
13
version_old = "0.8"
Andrei Paskevich's avatar
Andrei Paskevich committed
14
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
15
driver = "drivers/alt_ergo.drv"
MARCHE Claude's avatar
MARCHE Claude committed
16

17
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
18
name = "CVC3"
19
exec = "cvc3"
MARCHE Claude's avatar
MARCHE Claude committed
20
version_switch = "-version"
21
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
22
23
version_ok = "2.2"
version_old = "2.1"
Andrei Paskevich's avatar
Andrei Paskevich committed
24
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t -lang smt %f"
25
26
driver = "drivers/cvc3.drv"

27
28
29
30
31
32
33
34
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "1.0.27"
version_old = "1.0.17"
version_old = "1.0.24"
Andrei Paskevich's avatar
Andrei Paskevich committed
35
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt"
36
37
driver = "drivers/yices.drv"

38
39
40
[ATP eprover]
name = "Eprover"
exec = "eprover"
41
42
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
43
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
44
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
45
46
47

[ATP gappa]
name = "Gappa"
48
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
49
version_switch = "--version"
50
version_regexp = "Gappa \\([^ \n]*\\)"
MARCHE Claude's avatar
MARCHE Claude committed
51
52
version_ok = "0.13.0"
version_old = "0.12.3"
53
54
55
56
version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
Andrei Paskevich's avatar
Andrei Paskevich committed
57
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
58
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
59
60
61

[ATP simplify]
name = "Simplify"
62
63
64
65
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
66
version_switch = "-version"
67
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
68
version_ok = "1.5.5"
69
version_ok = "1.5.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
70
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
71
72
73
74
75
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
76
version_switch = "-TPTP || true"
77
version_regexp = "SPASS V \\([^ \n\t]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
78
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
79
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
80

81
82
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
83
exec = "veriT"
84
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
85
86
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
87
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
88
89
driver = "drivers/verit.drv"

MARCHE Claude's avatar
MARCHE Claude committed
90
91
[ATP z3]
name = "Z3"
92
93
exec = "z3"
exec = "z3-2.2"
MARCHE Claude's avatar
MARCHE Claude committed
94
version_switch = "-version"
95
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
96
97
98
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
Andrei Paskevich's avatar
Andrei Paskevich committed
99
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
100
driver = "drivers/z3.drv"
MARCHE Claude's avatar
MARCHE Claude committed
101
102
103

[ITP coq]
name = "Coq"
104
exec = "coqc"
MARCHE Claude's avatar
MARCHE Claude committed
105
version_switch = "-v"
106
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
107
version_ok = "8.3"
108
version_ok = "8.2pl2"
MARCHE Claude's avatar
MARCHE Claude committed
109
version_ok = "8.2pl1"
110
111
112
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
113
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
114
driver = "drivers/coq.drv"
MARCHE Claude's avatar
MARCHE Claude committed
115
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
116
117