provers-detection-data.conf 15.9 KB
Newer Older
1 2 3
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
MARCHE Claude's avatar
MARCHE Claude committed
4
exec = "alt-ergo-1.30"
5
exec = "alt-ergo-1.20.prv"
6
exec = "alt-ergo-1.10.prv"
7 8
exec = "alt-ergo-1.01"
exec = "alt-ergo-1.00.prv"
9
version_switch = "-version"
MARCHE Claude's avatar
MARCHE Claude committed
10
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
MARCHE Claude's avatar
MARCHE Claude committed
11
version_ok  = "1.30"
12
version_ok  = "1.20.prv"
13
version_ok  = "1.10.prv"
14
version_ok  = "1.01"
MARCHE Claude's avatar
MARCHE Claude committed
15
version_ok  = "1.00.prv"
16 17 18 19
# %T means timelimit+1
command = "%l/why3-cpulimit %T %m -s %e -timelimit %t %f"
# %U means 2*timelimit+1
command_steps = "%l/why3-cpulimit %U %m -s %e -steps-bound %S %f"
20 21 22
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"

23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.99.1"
exec = "alt-ergo-0.95.2"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok  = "0.99.1"
version_ok  = "0.95.2"
# %T means timelimit+1
command = "%l/why3-cpulimit %T %m -s %e -no-rm-eq-existential -timelimit %t %f"
# %U means 2*timelimit+1
command_steps = "%l/why3-cpulimit %U %m -s %e -no-rm-eq-existential -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"

39
# CVC4 version 1.5-prerelease
40
[ATP cvc4]
41
name = "CVC4"
42
exec = "cvc4"
43
exec = "cvc4-1.5-prerelease"
David Hauzar's avatar
David Hauzar committed
44
exec = "cvc4-1.5"
45 46 47
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok  = "1.5-prerelease"
48
version_ok  = "1.5"
49
driver = "drivers/cvc4_15.drv"
50 51
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
52
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
53
command_steps = "%l/why3-cpulimit %U %m -s %e --stats --rlimit=%S --lang=smt2 %f"
54

55 56
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
57
name = "CVC4"
58 59 60 61 62
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok  = "1.4"
63
driver = "drivers/cvc4_14.drv"
64 65 66 67 68 69
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"

70
# CVC4 version 1.4, not using SMTLIB bitvectors
71 72
[ATP cvc4]
name = "CVC4"
73
alternative = "noBV"
74 75 76 77
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
78
version_ok  = "1.4"
79
driver = "drivers/cvc4.drv"
80
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
81 82 83
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 .14 does not print steps used in --stats anyway
84 85
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"

David Hauzar's avatar
David Hauzar committed
86

87 88 89 90
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
91 92 93 94
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
95 96
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
97 98 99 100
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
version_old = "1.0"
101
driver = "drivers/cvc4.drv"
102
command = "%l/why3-cpulimit %t %m -s %e --lang=smt2 %f"
103

104 105 106 107 108 109 110 111 112 113 114
# Psyche version 2.x
[ATP psyche]
name = "Psyche"
exec = "psyche"
exec = "psyche-2.02"
version_switch = "-version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok  = "2.0"
driver = "drivers/psyche.drv"
command = "%l/why3-cpulimit %t %m -s %e -gplugin dpll_wl %f"

115
# CVC3 versions 2.4.x
116
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
117
name = "CVC3"
118
exec = "cvc3"
119
exec = "cvc3-2.4.1"
120
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
121 122
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
123 124
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
125
# the -timeout option is unreliable in CVC3 2.4.1
126
command = "%l/why3-cpulimit %t %m -s %e -seed 42 %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
127 128
driver = "drivers/cvc3.drv"

129
# CVC3 versions 2.x
130
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
131
name = "CVC3"
132
exec = "cvc3"
133 134
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
135
version_switch = "-version"
136
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
137
version_old = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
138
version_old = "2.1"
139
command = "%l/why3-cpulimit %T %m -s %e  -seed 42 -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
140
driver = "drivers/cvc3.drv"
141

142 143 144
[ATP yices]
name = "Yices"
exec = "yices"
145
exec = "yices-1.0.38"
146
version_switch = "--version"
147
version_regexp = "\\([^ \n]+\\)"
148 149 150
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
151 152
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
153
command = "%l/why3-cpulimit %t %m -s %e"
154 155
driver = "drivers/yices.drv"

156 157 158 159
[ATP yices-smt2]
name = "Yices"
exec = "yices-smt2"
exec = "yices-smt2-2.3.0"
160
version_switch = "--version"
161 162
version_regexp = "^Yices \\([^ \n]+\\)$"
version_ok = "2.3.0"
163
command = "%l/why3-cpulimit %t %m -s %e"
164
driver = "drivers/yices-smt2.drv"
165

166 167 168
[ATP eprover]
name = "Eprover"
exec = "eprover"
MARCHE Claude's avatar
MARCHE Claude committed
169 170
exec = "eprover-1.8"
exec = "eprover-1.7"
171 172 173
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
174
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
175
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
MARCHE Claude's avatar
MARCHE Claude committed
176
version_ok  = "1.8-001"
177 178
version_old = "1.7"
version_old = "1.6"
179 180
version_old = "1.5"
version_old = "1.4"
181
command = "%l/why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
MARCHE Claude's avatar
MARCHE Claude committed
182
driver = "drivers/eprover.drv"
MARCHE Claude's avatar
MARCHE Claude committed
183 184 185

[ATP gappa]
name = "Gappa"
186
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
187
exec = "gappa-1.2.0"
188
exec = "gappa-1.1.1"
189
exec = "gappa-1.1.0"
190
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
191
exec = "gappa-0.16.1"
192
exec = "gappa-0.14.1"
MARCHE Claude's avatar
MARCHE Claude committed
193
version_switch = "--version"
194
version_regexp = "Gappa \\([^ \n]*\\)"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
195
version_ok = "^1\.[0-2]\..+$"
196
version_old = "^0\.1[1-8]\..+$"
197
command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
198 199
driver = "drivers/gappa.drv"

200 201 202
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
203
exec = "mathsat-5.2.2"
204 205 206
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
207
command = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f"
208 209
driver = "drivers/mathsat.drv"

MARCHE Claude's avatar
MARCHE Claude committed
210 211
[ATP simplify]
name = "Simplify"
212 213 214 215
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
216
version_switch = "-version"
217
version_regexp = "Simplify version \\([^ \n,]+\\)"
218 219
version_old = "1.5.5"
version_old = "1.5.4"
220
command = "%l/why3-cpulimit %t %m -s %e %f"
221 222
driver = "drivers/simplify.drv"

223 224 225 226 227 228
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
229 230 231 232
# %U means 2*timelimit+1. Required because Metis tends to
# react very slowly to the time limit given, hence answers
# oscillate between Timeout and Unknown
command = "%l/why3-cpulimit %U %m -s %e --time-limit %t %f"
233 234 235 236 237
driver = "drivers/metis.drv"

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
MARCHE Claude's avatar
MARCHE Claude committed
238 239
exec = "metit-2.4"
exec = "metit-2.2"
240 241
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
242 243
version_ok = "2.4"
version_old = "2.2"
244
command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
245 246
driver = "drivers/metitarski.drv"

247 248 249 250 251 252 253 254 255 256
[ATP polypaver]
name = "PolyPaver"
exec = "polypaver"
exec = "polypaver-0.3"
version_switch = "--version"
version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
version_ok = "0.3"
command = "%l/why3-cpulimit %T %m -s %e -d 2 -m 10 --time=%t %f"
driver = "drivers/polypaver.drv"

257 258 259
[ATP spass]
name = "Spass"
exec = "SPASS"
260
exec = "SPASS-3.7"
261
version_switch = " | grep 'SPASS V'"
262
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
263
version_ok = "3.7"
264
command = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
MARCHE Claude's avatar
MARCHE Claude committed
265
driver = "drivers/spass.drv"
MARCHE Claude's avatar
MARCHE Claude committed
266

267 268 269 270 271 272 273
[ATP spass]
name = "Spass"
exec = "SPASS"
exec = "SPASS-3.8ds"
version_switch = " | grep 'SPASS[^ \\n\\t]* V'"
version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)"
version_ok = "3.8ds"
274
command = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
275 276
driver = "drivers/spass_types.drv"

MARCHE Claude's avatar
MARCHE Claude committed
277 278 279
[ATP vampire]
name = "Vampire"
exec = "vampire"
280
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
281 282
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
283
command = "%l/why3-cpulimit %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
284
driver = "drivers/vampire.drv"
285
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
286

287 288 289 290
[ATP princess]
name = "Princess"
exec = "princess"
# version_switch = "-h"
291
version_regexp = "(CASC version \\([0-9-]+\\))"
292
command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f"
293
driver = "drivers/princess.drv"
294 295 296 297 298 299 300 301
version_ok = "2013-05-13"

[ATP beagle]
name = "Beagle"
exec = "beagle"
exec = "beagle-0.4.1"
# version_switch = "-h"
version_regexp = "version \\([0-9.]+\\)"
302
command = "%l/why3-cpulimit %t 0 -s %e %f"
303 304
driver = "drivers/beagle.drv"
version_ok = "0.4.1"
305

MARCHE Claude's avatar
MARCHE Claude committed
306 307 308 309 310 311 312 313 314 315
[ATP verit]
name = "veriT"
exec = "veriT"
exec = "veriT-201410"
version_switch = "--version"
version_regexp = "version \\([^ \n\r]+\\)"
command = "%l/why3-cpulimit %t %m -s %e --disable-print-success %f"
driver = "drivers/verit.drv"
version_ok = "201410"

316 317
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
318
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
319 320
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
321
version_regexp = "version \\([^ \n\r]+\\)"
322 323
command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
324
driver = "drivers/verit.drv"
MARCHE Claude's avatar
MARCHE Claude committed
325
version_old = "201310"
326

327
# Z3 >= 4.4.0, with BV support
328
[ATP z3]
329
name = "Z3"
330
exec = "z3"
331
exec = "z3-4.4.1"
332 333 334
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
335
version_ok  = "4.4.1"
336 337 338 339 340
version_ok  = "4.4.0"
driver = "drivers/z3_440.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"

341 342 343 344 345
# Z3 >= 4.4.0, without BV support
[ATP z3]
name = "Z3"
alternative = "noBV"
exec = "z3"
346
exec = "z3-4.4.1"
347 348 349
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
350
version_ok  = "4.4.1"
351 352 353 354 355
version_ok  = "4.4.0"
driver = "drivers/z3_432.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"

MARCHE Claude's avatar
MARCHE Claude committed
356 357
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
358
# Z3 4.3.2 supports Datatypes
MARCHE Claude's avatar
MARCHE Claude committed
359 360 361 362 363
[ATP z3]
name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
364
version_ok  = "4.3.2"
365
driver = "drivers/z3_432.drv"
MARCHE Claude's avatar
MARCHE Claude committed
366
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
367
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
MARCHE Claude's avatar
MARCHE Claude committed
368

369
[ATP z3]
370 371
name = "Z3"
exec = "z3"
372 373
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
374
exec = "z3-4.2"
375 376
exec = "z3-4.1.2"
exec = "z3-4.1.1"
377 378 379
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
380
version_old = "4.3.1"
381 382 383 384 385
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
386
driver = "drivers/z3.drv"
387
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
388

389
[ATP z3]
390
name = "Z3"
391
exec = "z3"
392
exec = "z3-3.2"
393 394
exec = "z3-3.1"
exec = "z3-3.0"
395 396
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
397
version_old = "3.2"
398 399 400
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
401
# the -T is unreliable in Z3 3.2
402
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
403

404
[ATP z3]
François Bobot's avatar
François Bobot committed
405 406
name = "Z3"
exec = "z3"
407 408 409 410
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
411 412
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
413 414
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
Andrei Paskevich's avatar
Andrei Paskevich committed
415
driver = "drivers/z3.drv"
416
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 \
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
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

436
[ATP z3]
437
name = "Z3"
438 439
exec = "z3"
exec = "z3-2.2"
440 441
exec = "z3-2.1"
exec = "z3-1.3"
442 443
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
444 445
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
446
version_old = "1.3"
447
command = "%l/why3-cpulimit %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
448
driver = "drivers/z3_smtv1.drv"
449

450 451 452
[ATP zenon]
name = "Zenon"
exec = "zenon"
453
exec = "zenon-0.8.0"
454 455 456
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
457
version_ok = "0.8.0"
458
version_ok = "0.7.1"
459
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
460 461
driver = "drivers/zenon.drv"

462 463 464 465 466
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
467
version_ok = "0.4.1"
468 469 470
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon_modulo.drv"

471 472 473
[ATP iprover]
name = "iProver"
exec = "iprover"
474
exec = "iprover-0.8.1"
475 476 477
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
478
command = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \
479 480
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
481 482
driver = "drivers/iprover.drv"

Daisuke Ishii's avatar
Daisuke Ishii committed
483 484 485 486 487
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
488
version_ok = "9.0"
Daisuke Ishii's avatar
Daisuke Ishii committed
489 490
version_ok = "8.0"
version_ok = "7.0"
491
command = "%l/why3-cpulimit %t %m -s %e -noprompt"
Daisuke Ishii's avatar
Daisuke Ishii committed
492 493
driver = "drivers/mathematica.drv"

Guillaume Melquiond's avatar
Guillaume Melquiond committed
494 495 496 497 498 499 500 501 502 503 504 505
# Coq 8.6: do not limit memory
[ITP coq]
name = "Coq"
compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.6"
command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"

506 507 508 509 510 511 512
# Coq 8.5: do not limit memory
[ITP coq]
name = "Coq"
compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
513 514
version_ok = "8.5pl3"
version_ok = "8.5pl2"
515
version_ok = "8.5pl1"
516 517 518 519 520
version_ok = "8.5"
command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"

MARCHE Claude's avatar
MARCHE Claude committed
521 522
[ITP coq]
name = "Coq"
523
compile_time_support = true
524
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
525
version_switch = "-v"
526
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
527
version_ok = "^8\.4pl[1-6]$"
528
version_ok = "8.4"
529
command = "%l/why3-cpulimit 0 %m -s %e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
530 531 532
driver = "drivers/coq.drv"
editor = "coqide"

533 534
[ITP pvs]
name = "PVS"
535
compile_time_support = true
536 537 538
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
539
version_ok = "6.0"
540
version_bad = "^[0-5]\..+$"
541 542
# not why3-cpulimit 0 %m because 'proveit' allocates 8Gb at start-up
command = "%l/why3-cpulimit 0 0 -s %l/why3-call-pvs %l proveit -f %f"
543
driver = "drivers/pvs.drv"
544
in_place = true
545
editor = "pvs"
546

547 548 549 550
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
Stefan Berghofer's avatar
Stefan Berghofer committed
551
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
Stefan Berghofer's avatar
Stefan Berghofer committed
552 553
version_ok = "2016"
version_bad = "2015"
554 555
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
Stefan Berghofer's avatar
Stefan Berghofer committed
556
driver = "drivers/isabelle2016.drv"
557
in_place = true
Stefan Berghofer's avatar
Stefan Berghofer committed
558
editor = "isabelle-jedit"
559 560 561 562 563 564

[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
Stefan Berghofer's avatar
Stefan Berghofer committed
565 566
version_ok = "2015"
version_bad = "2016"
567 568
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
Stefan Berghofer's avatar
Stefan Berghofer committed
569
driver = "drivers/isabelle2015.drv"
570
in_place = true
Stefan Berghofer's avatar
Stefan Berghofer committed
571
editor = "isabelle-jedit"
572

573 574
[editor pvs]
name = "PVS"
575
command = "%l/why3-call-pvs %l pvs %f"
576 577

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
578
name = "CoqIDE"
MARCHE Claude's avatar
MARCHE Claude committed
579
command = "coqide -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
580 581

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
582
name = "Emacs/ProofGeneral/Coq"
583
command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq-tactic\\\" \\\"Why3\\\") \
584
(\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
585

Stefan Berghofer's avatar
Stefan Berghofer committed
586 587
[editor isabelle-jedit]
name = "Isabelle/jEdit"
Stefan Berghofer's avatar
Stefan Berghofer committed
588
command = "isabelle why3 -i %f"
589

590
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
591
name = "AltGr-Ergo"
592
command = "altgr-ergo %f"
593 594 595 596

[shortcut shortcut1]
name="Alt-Ergo"
shortcut="altergo"