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

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

[ATP eprover]
name = "Eprover"
exec = "eprover"
26
27
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
28
29
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
30
31
32

[ATP gappa]
name = "Gappa"
33
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
34
version_switch = "--version"
35
version_regexp = "Gappa \\([^ \n]*\\)"
MARCHE Claude's avatar
MARCHE Claude committed
36
37
38
39
40
41
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"
42
43
command = "why3-cpulimit %t %m %e %f 2>&1"
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
44
45
46

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

[ATP spass]
name = "Spass"
exec = "SPASS"
61
62
version_switch = " || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
63
64
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
65
66
67

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

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