MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

provers-detection-data.conf.in 7.6 KB
Newer Older
1
[ATP alt-ergo]
2
3
4
5
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
6
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
7
version_ok = "0.95-dev"
8
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
9
driver = "drivers/alt_ergo_model.drv"
10
11
editor = "altgr-ergo"

12
13
[ATP alt-ergo]
name = "Alt-Ergo"
14
exec = "alt-ergo"
15
exec = "alt-ergo-0.94"
16
17
18
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
19
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
20
driver = "drivers/alt_ergo.drv"
21
editor = "altgr-ergo"
22
23
24
25

[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
26
27
exec = "alt-ergo-0.93.1"
exec = "alt-ergo-0.93"
MARCHE Claude's avatar
MARCHE Claude committed
28
version_switch = "-version"
29
version_regexp = "\\([0-9.]+\\)"
30
version_ok = "^0\.93\.[1-3]"
31
version_ok = "0.93"
32
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
33
driver = "drivers/alt_ergo_0.93.drv"
MARCHE Claude's avatar
MARCHE Claude committed
34

35
[ATP alt-ergo]
36
name = "Alt-Ergo"
37
exec = "alt-ergo"
38
39
40
41
exec = "alt-ergo-0.92.3"
exec = "alt-ergo-0.92.2"
exec = "alt-ergo-0.92.1"
exec = "alt-ergo-0.92"
42
exec = "alt-ergo-0.91"
43
44
45
exec = "alt-ergo-0.9"
exec = "alt-ergo-0.8"
exec = "ergo"
46
version_switch = "-version"
47
version_regexp = "\\([0-9.]+\\)"
48
version_old = "^0\.92\..+"
49
50
version_old = "0.92"
version_old = "0.91"
51
52
version_old = "0.9"
version_old = "0.8"
53
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
54
driver = "drivers/alt_ergo_bare.drv"
55

56
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
57
name = "CVC3"
58
exec = "cvc3"
59
exec = "cvc3-2.4.1"
60
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
61
62
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
63
64
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
65
# the -timeout option is unreliable in CVC3 2.4.1
66
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
67
68
driver = "drivers/cvc3.drv"

69
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
70
name = "CVC3"
71
exec = "cvc3"
72
73
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
74
version_switch = "-version"
75
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
76
version_ok  = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
77
version_old = "2.1"
78
# we pass time 0 to why3-cpulimit to avoid race
79
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
80
driver = "drivers/cvc3.drv"
81

82
83
84
85
86
[ATP yices]
name = "Yices"
exec = "yices"
version_switch = "--version"
version_regexp = "[Yices ]*\\([^ \n]+\\)"
87
88
89
90
version_ok = "^1\.0\.3[0-5]"
version_ok = "^1\.0\.2[5-9]"
version_old = "^1\.0\.2[0-4]"
version_old = "^1\.0\.1."
91
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e"
92
93
driver = "drivers/yices.drv"

94
95
96
[ATP eprover]
name = "Eprover"
exec = "eprover"
97
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
98
99
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.4"
100
# we pass time 0 to why3-cpulimit to avoid race
101
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
102
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
103
104
105

[ATP gappa]
name = "Gappa"
106
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
107
version_switch = "--version"
108
version_regexp = "Gappa \\([^ \n]*\\)"
109
110
111
version_ok = "^0.16.[0-1]"
version_ok = "^0\.1[4-5]\..+"
version_old = "^0\.1[1-2]\..+"
112
113
114
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

115
[ATP gappa]
MARCHE Claude's avatar
MARCHE Claude committed
116
117
118
119
120
121
122
123
name = "Gappa+dev"
exec = "gappa-0.16.0+dev"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.16.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

124
[ATP gappa]
125
126
127
128
129
130
131
132
name = "Gappa"
exec = "gappa-0.15.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.15.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"

133
[ATP gappa]
134
135
136
137
138
139
name = "Gappa"
exec = "gappa-0.14.1"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.14.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
140
driver = "drivers/gappa.drv"
MARCHE Claude's avatar
MARCHE Claude committed
141
142
143

[ATP simplify]
name = "Simplify"
144
145
146
147
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
148
version_switch = "-version"
149
version_regexp = "Simplify version \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
150
version_ok = "1.5.5"
151
version_ok = "1.5.4"
152
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
153
154
155
156
157
driver = "drivers/simplify.drv"

[ATP spass]
name = "Spass"
exec = "SPASS"
158
version_switch = "-TPTP || true"
159
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
160
version_ok = "3.7"
161
# we pass time 0 to why3-cpulimit to avoid race
162
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
163
driver = "drivers/tptp.drv"
MARCHE Claude's avatar
MARCHE Claude committed
164

MARCHE Claude's avatar
MARCHE Claude committed
165
166
167
168
169
[ATP vampire]
name = "Vampire"
exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
170
# we pass time 0 to why3-cpulimit to avoid race
171
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
172
driver = "drivers/vampire.drv"
173
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
174

175
176
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
177
exec = "veriT"
178
exec = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
179
180
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
181
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
182
183
driver = "drivers/verit.drv"

184
[ATP z3]
185
186
187
188
189
190
191
192
193
name = "Z3"
exec = "z3"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok  = "4.0"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"

194
[ATP z3]
195
name = "Z3"
196
exec = "z3"
197
exec = "z3-3.2"
198
199
exec = "z3-3.1"
exec = "z3-3.0"
200
201
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
202
version_ok  = "^3\..+"
203
204
205
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
206
# the -T is unreliable in Z3 3.2
207
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
208

209
[ATP z3]
François Bobot's avatar
François Bobot committed
210
211
name = "Z3"
exec = "z3"
212
213
214
215
exec = "z3-2.19"
exec = "z3-2.18"
exec = "z3-2.17"
exec = "z3-2.16"
François Bobot's avatar
François Bobot committed
216
217
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
218
219
version_old = "^2\.2.+"
version_old = "^2\.1[6-9]"
Andrei Paskevich's avatar
Andrei Paskevich committed
220
driver = "drivers/z3.drv"
221
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 \
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
PHASE_SELECTION=0 \
RESTART_STRATEGY=0 \
RESTART_FACTOR=1.5 \
QI_EAGER_THRESHOLD=100 \
ARITH_RANDOM_INITIAL_VALUE=true \
SORT_AND_OR=false \
CASE_SPLIT=3 \
DELAY_UNITS=true \
DELAY_UNITS_THRESHOLD=16 \
%f"
#Other Parameters given by Nikolaj Bjorner
#BV_REFLECT=true #arith?
#MODEL_PARTIAL=true
#MODEL_VALUE_COMPLETION=false
#MODEL_HIDE_UNUSED_PARTITIONS=false
#MODEL_V1=true
#ASYNC_COMMANDS=false
#NNF_SK_HACK=true

241
[ATP z3]
242
name = "Z3"
243
244
exec = "z3"
exec = "z3-2.2"
245
246
exec = "z3-2.1"
exec = "z3-1.3"
247
248
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
249
250
version_old = "^2\.1[0-5]"
version_old = "^2\.[0-9]"
251
version_old = "1.3"
252
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
253
driver = "drivers/z3_smtv1.drv"
254

MARCHE Claude's avatar
MARCHE Claude committed
255
256
[ITP coq]
name = "Coq"
257
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
258
version_switch = "-v"
259
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
260
version_ok = "8.3pl4"
261
version_ok = "8.3pl3"
262
263
version_ok = "8.3pl2"
version_ok = "8.3pl1"
MARCHE Claude's avatar
MARCHE Claude committed
264
version_ok = "8.3"
265
266
267
268
269
270
271
272
273
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"

[ITP coq]
name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
274
275
276
version_old = "8.2pl2"
version_old = "8.2pl1"
version_old = "8.2"
277
278
version_old = "8.1"
version_old = "8.0"
279
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
280
driver = "drivers/coq.drv"
281
editor = "coqide"
MARCHE Claude's avatar
MARCHE Claude committed
282

283
284
285
286
287
288
289
290
[ITP pvs]
name = "PVS"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "5.0"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
driver = "drivers/pvs.drv"
291
in_place = true
292
editor = "pvs"
293

294
295
296
[editor pvs]
name = "PVS"
command = "@LOCALBIN@why3-call-pvs %l %f"
297
298

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
299
name = "CoqIDE"
300
301
302
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
303
name = "Emacs/ProofGeneral/Coq"
304
command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
305
306

[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
307
name = "AltGr-Ergo"
308
command = "altgr-ergo %f"