provers-detection-data.conf 2.22 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
6
exec = "alt-ergo-0.91"
exec = "alt-ergo-0.92.1"
MARCHE Claude's avatar
MARCHE Claude committed
7
version_switch = "-version"
8
version_regexp = ".*Ergo \\([^ \n]*\\)"
MARCHE Claude's avatar
MARCHE Claude committed
9
version_ok = "0.91"
MARCHE Claude's avatar
MARCHE Claude committed
10
version_ok = "0.92"
MARCHE Claude's avatar
MARCHE Claude committed
11
version_ok = "0.92.1"
MARCHE Claude's avatar
MARCHE Claude committed
12
13
version_old = "0.8"
version_old = "0.9"
14
15
command = "why3-cpulimit %t %m %e %f"
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"
24
25
26
27
28
29
command = "why3-cpulimit 0 %m %e -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"

[ATP eprover]
name = "Eprover"
exec = "eprover"
30
31
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
32
33
command = "why3-cpulimit 0 %m %e -s --print-statistics -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
34
35
36

[ATP gappa]
name = "Gappa"
37
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
38
version_switch = "--version"
39
version_regexp = "Gappa \\([^ \n]*\\)"
MARCHE Claude's avatar
MARCHE Claude committed
40
41
42
43
44
45
version_ok = "0.13.0"
version_old = "0.11.2"
version_old = "0.12.0"
version_old = "0.12.1"
version_old = "0.12.2"
version_old = "0.12.3"
46
47
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
48
49
50

[ATP simplify]
name = "Simplify"
51
52
53
54
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
55
version_switch = "-version"
56
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
57
58
version_ok = "1.5.4"
version_ok = "1.5.5"
59
60
61
62
63
64
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
65
version_switch = "-TPTP || true"
66
version_regexp = "SPASS V \\([^ \n\t]+\\)"
67
68
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
69
70
71

[ATP z3]
name = "Z3"
72
73
exec = "z3"
exec = "z3-2.2"
MARCHE Claude's avatar
MARCHE Claude committed
74
version_switch = "-version"
75
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
76
77
78
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
79
80
command = "why3-cpulimit %t %m %e -smt %f 2>&1"
driver = "drivers/z3.drv"
MARCHE Claude's avatar
MARCHE Claude committed
81
82
83

[ITP coq]
name = "Coq"
84
exec = "coqc"
MARCHE Claude's avatar
MARCHE Claude committed
85
version_switch = "-v"
86
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
87
88
89
90
version_ok = "8.0"
version_ok = "8.1"
version_ok = "8.2"
version_ok = "8.2pl1"
MARCHE Claude's avatar
MARCHE Claude committed
91
version_old = "7.4"
92
93
command = "%e %f"
driver = "drivers/coq.drv"
MARCHE Claude's avatar
MARCHE Claude committed
94
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
95
96