provers-detection-data.conf 15.4 KB
Newer Older
1 2 3
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
4
exec = "alt-ergo-2.2.0"
5
exec = "alt-ergo-2.1.0"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
6
exec = "alt-ergo-2.0.0"
7 8
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
9
version_ok  = "2.2.0"
10
version_ok  = "2.1.0"
11
version_ok  = "2.0.0"
12 13 14 15
version_bad = "1.30"
version_bad = "1.01"
version_bad = "0.99.1"
version_bad = "0.95.2"
16 17
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
18
driver = "alt_ergo"
19
editor = "altgr-ergo"
20
use_at_auto_level = 1
21

22
# CVC4 version >= 1.6, with counterexamples
23 24 25 26
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
27
exec = "cvc4-1.6"
28 29
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
30
version_ok  = "1.6"
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
driver = "cvc4_16_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"

# CVC4 version >= 1.6
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.6"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok  = "1.6"
driver = "cvc4_16"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1

# CVC4 version = 1.5, with counterexamples
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
60
version_ok  = "1.5"
61
driver = "cvc4_15_counterexample"
62 63 64 65 66
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"

67
# CVC4 version 1.5
68
[ATP cvc4]
69
name = "CVC4"
70
exec = "cvc4"
71
exec = "cvc4-1.5"
72 73
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
74
version_ok  = "1.5"
75
driver = "cvc4_15"
76 77
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
78
command = "%e --tlimit=%t000 --lang=smt2 %f"
79
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
MARCHE Claude's avatar
MARCHE Claude committed
80
use_at_auto_level = 1
81

82 83
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
84
name = "CVC4"
85 86 87 88
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
89
version_old  = "1.4"
90
driver = "cvc4_14"
91 92 93 94
# --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
95
command = "%e --tlimit=%t000 --lang=smt2 %f"
96
use_at_auto_level = 1
97

98
# CVC4 version 1.4, not using SMTLIB bitvectors
99 100
[ATP cvc4]
name = "CVC4"
101
alternative = "noBV"
102 103 104 105
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
106
version_old  = "1.4"
107
driver = "cvc4"
108
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
109 110
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
111
# cvc4 1.4 does not print steps used in --stats anyway
112
command = "%e --tlimit=%t000 --lang=smt2 %f"
113

114

115 116 117 118
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
119 120 121 122
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
123 124
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
125 126 127 128
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
version_old = "1.0"
129
driver = "cvc4"
130
command = "%e --lang=smt2 %f"
131

132 133 134 135 136 137 138 139
# 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"
140
driver = "psyche"
141
command = "%e -gplugin dpll_wl %f"
142

143
# CVC3 versions 2.4.x
144
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
145
name = "CVC3"
146
exec = "cvc3"
147
exec = "cvc3-2.4.1"
148
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
149 150
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
151 152
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
153
# the -timeout option is unreliable in CVC3 2.4.1
154
command = "%e -seed 42 %f"
155
driver = "cvc3"
Andrei Paskevich's avatar
Andrei Paskevich committed
156

157
# CVC3 versions 2.x
158
[ATP cvc3]
159
name = "CVC3"
160
exec = "cvc3"
161 162
exec = "cvc3-2.2"
exec = "cvc3-2.1"
163
version_switch = "-version"
164
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
165
version_old = "2.2"
166
version_old = "2.1"
167
command = "%e  -seed 42 -timeout %t %f"
168
driver = "cvc3"
169

170 171 172
[ATP yices]
name = "Yices"
exec = "yices"
173
exec = "yices-1.0.38"
174
version_switch = "--version"
175
version_regexp = "\\([^ \n]+\\)"
176 177 178
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
179 180
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
181
command = "%e"
182
driver = "yices"
183

184 185 186 187
[ATP yices-smt2]
name = "Yices"
exec = "yices-smt2"
exec = "yices-smt2-2.3.0"
Jean-Christophe's avatar
Jean-Christophe committed
188
version_switch = "--version"
189 190
version_regexp = "^Yices \\([^ \n]+\\)$"
version_ok = "2.3.0"
191
command = "%e"
192
driver = "yices-smt2"
Jean-Christophe's avatar
Jean-Christophe committed
193

194 195 196
[ATP eprover]
name = "Eprover"
exec = "eprover"
197 198 199
exec = "eprover-2.0"
exec = "eprover-1.9.1"
exec = "eprover-1.9"
MARCHE Claude's avatar
MARCHE Claude committed
200 201
exec = "eprover-1.8"
exec = "eprover-1.7"
202 203 204
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
205
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
206
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
207 208 209 210
version_ok  = "2.0"
version_old = "1.9.1-001"
version_old = "1.9"
version_old = "1.8-001"
211 212
version_old = "1.7"
version_old = "1.6"
213 214
version_old = "1.5"
version_old = "1.4"
215
command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
216
driver = "eprover"
217
use_at_auto_level = 2
218 219 220

[ATP gappa]
name = "Gappa"
221
exec = "gappa"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
222
exec = "gappa-1.3.2"
223 224
exec = "gappa-1.3.0"
exec = "gappa-1.2.2"
MARCHE Claude's avatar
MARCHE Claude committed
225
exec = "gappa-1.2.0"
226
exec = "gappa-1.1.1"
227
exec = "gappa-1.1.0"
228
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
229
exec = "gappa-0.16.1"
230
exec = "gappa-0.14.1"
231
version_switch = "--version"
232
version_regexp = "Gappa \\([^ \n]*\\)"
233
version_ok = "^1\.[0-3]\..+$"
234
version_old = "^0\.1[1-8]\..+$"
235
command = "%e -Eprecision=70"
236
driver = "gappa"
237

238 239 240
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
241
exec = "mathsat-5.2.2"
242 243 244
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
245
command = "%e -input=smt2 -model -random_seed=80"
246
driver = "mathsat"
247

248 249
[ATP simplify]
name = "Simplify"
250 251 252 253
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
254
version_switch = "-version"
255
version_regexp = "Simplify version \\([^ \n,]+\\)"
256 257
version_old = "1.5.5"
version_old = "1.5.4"
258
command = "%e %f"
259
driver = "simplify"
260

261 262 263 264 265 266
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
267
command = "%e --time-limit %t %f"
268
driver = "metis"
269 270 271 272

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
273 274
exec = "metit-2.4"
exec = "metit-2.2"
275 276
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
277 278
version_ok = "2.4"
version_old = "2.2"
279
command = "%e --time %t %f"
280
driver = "metitarski"
281

282 283 284 285 286 287 288
[ATP polypaver]
name = "PolyPaver"
exec = "polypaver"
exec = "polypaver-0.3"
version_switch = "--version"
version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
version_ok = "0.3"
289
command = "%e -d 2 -m 10 --time=%t %f"
290
driver = "polypaver"
291

292 293 294
[ATP spass]
name = "Spass"
exec = "SPASS"
295
exec = "SPASS-3.7"
296
version_switch = " | grep 'SPASS V'"
297
version_regexp = "SPASS V \\([^ \n\t]+\\)"
298
version_ok = "3.7"
299
command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
300
driver = "spass"
301
use_at_auto_level = 2
302

303 304 305 306 307 308 309
[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"
310
command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
311
driver = "spass_types"
312
use_at_auto_level = 2
313

MARCHE Claude's avatar
MARCHE Claude committed
314 315 316
[ATP vampire]
name = "Vampire"
exec = "vampire"
317
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
318 319
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
320
command = "%e -t %t"
321
driver = "vampire"
322
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
323

324 325 326
[ATP princess]
name = "Princess"
exec = "princess"
327
exec = "princess-2015-12-07"
328
# version_switch = "-h"
329 330
# version_regexp = "(CASC version \\([0-9-]+\\))"
version_regexp = "(release \\([0-9-]+\\))"
331
command = "%e -timeout=%t %f"
332
driver = "princess"
333 334
# version_ok = "2013-05-13"
version_ok = "2015-12-07"
335 336 337 338 339 340 341

[ATP beagle]
name = "Beagle"
exec = "beagle"
exec = "beagle-0.4.1"
# version_switch = "-h"
version_regexp = "version \\([0-9.]+\\)"
342
command = "%e %f"
343
driver = "beagle"
344
version_ok = "0.4.1"
345

MARCHE Claude's avatar
MARCHE Claude committed
346 347 348 349 350 351
[ATP verit]
name = "veriT"
exec = "veriT"
exec = "veriT-201410"
version_switch = "--version"
version_regexp = "version \\([^ \n\r]+\\)"
352
command = "%e --disable-print-success %f"
353
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
354 355
version_ok = "201410"

356 357
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
358
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
359 360
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
361
version_regexp = "version \\([^ \n\r]+\\)"
362
command = "%e --disable-print-success --enable-simp \
363
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
364
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
365
version_old = "201310"
366

367
# Z3 >= 4.6.0, with counterexamples and incremental usage
368 369 370 371
[ATP z3-ce]
name = "Z3"
alternative = "counterexamples"
exec = "z3"
MARCHE Claude's avatar
MARCHE Claude committed
372
exec = "z3-4.7.1"
373 374 375 376 377 378
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
379
version_ok  = "4.7.1"
380 381 382 383
version_ok  = "4.6.0"
version_ok  = "4.5.0"
version_old  = "4.4.1"
version_old  = "4.4.0"
384
driver = "z3_440_counterexample"
385
# -t sets the time limit per query
386 387 388
command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"

389
# Z3 >= 4.4.0, with BV support
390
[ATP z3]
391
name = "Z3"
392
exec = "z3"
MARCHE Claude's avatar
MARCHE Claude committed
393
exec = "z3-4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
394
exec = "z3-4.6.0"
395
exec = "z3-4.5.0"
396
exec = "z3-4.4.1"
397 398 399
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
400
version_ok  = "4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
401
version_ok  = "4.6.0"
402
version_ok  = "4.5.0"
MARCHE Claude's avatar
MARCHE Claude committed
403 404
version_old  = "4.4.1"
version_old  = "4.4.0"
405
driver = "z3_440"
406
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
407
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
408
use_at_auto_level = 1
409

410
# Z3 >= 4.4.0, without BV support
411
[ATP z3-nobv]
412 413 414
name = "Z3"
alternative = "noBV"
exec = "z3"
MARCHE Claude's avatar
MARCHE Claude committed
415
exec = "z3-4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
416
exec = "z3-4.6.0"
417
exec = "z3-4.5.0"
418
exec = "z3-4.4.1"
419 420 421
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
422
version_ok  = "4.7.1"
MARCHE Claude's avatar
MARCHE Claude committed
423
version_ok  = "4.6.0"
424
version_ok  = "4.5.0"
MARCHE Claude's avatar
MARCHE Claude committed
425 426
version_old  = "4.4.1"
version_old  = "4.4.0"
427
driver = "z3_432"
428
command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
429
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
430

MARCHE Claude's avatar
MARCHE Claude committed
431 432
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
433
# Z3 4.3.2 supports Datatypes
MARCHE Claude's avatar
MARCHE Claude committed
434 435 436 437 438
[ATP z3]
name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
439
version_old  = "4.3.2"
440
driver = "z3_432"
441 442
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%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
443

444
[ATP z3]
Jean-Christophe's avatar
Jean-Christophe committed
445 446
name = "Z3"
exec = "z3"
447 448
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
449
exec = "z3-4.2"
450 451
exec = "z3-4.1.2"
exec = "z3-4.1.1"
Jean-Christophe's avatar
Jean-Christophe committed
452 453 454
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
455
version_old = "4.3.1"
456 457 458 459 460
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
461
driver = "z3"
462
command = "%e -smt2 -rs:42 %f"
Jean-Christophe's avatar
Jean-Christophe committed
463

464
[ATP z3]
465
name = "Z3"
466
exec = "z3"
467
exec = "z3-3.2"
468 469
exec = "z3-3.1"
exec = "z3-3.0"
470 471
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
472
version_old = "3.2"
473 474
version_old = "3.1"
version_old = "3.0"
475
driver = "z3"
Andrei Paskevich's avatar
Andrei Paskevich committed
476
# the -T is unreliable in Z3 3.2
477
command = "%e -smt2 -rs:42 %f"
478

479
[ATP z3]
François Bobot's avatar
François Bobot committed
480 481
name = "Z3"
exec = "z3"
482 483 484 485
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
486 487
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
488 489
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
490
driver = "z3"
491
command = "%e -smt2 -rs:42 \
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510
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

511
[ATP z3]
512
name = "Z3"
513 514
exec = "z3"
exec = "z3-2.2"
515 516
exec = "z3-2.1"
exec = "z3-1.3"
517 518
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
519 520
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
521
version_old = "1.3"
522
command = "%e -smt %f"
523
driver = "z3_smtv1"
524

525 526 527
[ATP zenon]
name = "Zenon"
exec = "zenon"
528
exec = "zenon-0.8.0"
529 530 531
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
532
version_ok = "0.8.0"
533
version_ok = "0.7.1"
534
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
535
driver = "zenon"
536

537 538 539 540 541
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
542
version_ok = "0.4.1"
543
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
544
driver = "zenon_modulo"
545

546 547 548
[ATP iprover]
name = "iProver"
exec = "iprover"
549
exec = "iprover-0.8.1"
550 551 552
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
553
command = "%e --fof true --out_options none \
554 555
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
556
driver = "iprover"
557

558 559 560 561 562
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
563
version_ok = "9.0"
564 565
version_ok = "8.0"
version_ok = "7.0"
566
command = "%e -noprompt"
567
driver = "mathematica"
568

569 570
[ITP coq]
name = "Coq"
571
support_library = "%l/coq/version"
572
exec = "coqtop"
573 574
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
575
version_ok = "^8\.8\.[0-2]$"
576
version_ok = "^8\.7\.[0-2]$"
MARCHE Claude's avatar
MARCHE Claude committed
577
version_ok = "8.6.1"
578
version_ok = "8.6"
MARCHE Claude's avatar
MARCHE Claude committed
579 580
version_old = "^8\.5pl[1-3]$"
version_old = "8.5"
581
command = "%e -batch -R %l/coq Why3 -l %f"
582
driver = "coq"
583 584
editor = "coqide"

585 586
[ITP pvs]
name = "PVS"
587
support_library = "%l/pvs/version"
588 589 590
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
591
version_ok = "6.0"
592
version_bad = "^[0-5]\..+$"
593
command = "%l/why3-call-pvs %l/pvs proveit -f %f"
594
driver = "pvs"
595
in_place = true
596
editor = "pvs"
597

598 599 600 601
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
602
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
603
version_ok = "2018"
604
version_bad = "2017"
605
version_bad = "2016-1"
606
command = "%e why3 -b %f"
607
driver = "isabelle2018"
608
in_place = true
609
editor = "isabelle-jedit"
610 611 612 613 614 615

[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
616
version_ok = "2017"
617
version_bad = "2018"
618
version_bad = "2016-1"
619
command = "%e why3 -b %f"
620
driver = "isabelle2017"
621
in_place = true
622
editor = "isabelle-jedit"
623

624 625
[editor pvs]
name = "PVS"
626
command = "%l/why3-call-pvs %l pvs %f"
627 628

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
629
name = "CoqIDE"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
630
command = "coqide -R %l/coq Why3 %f"
631 632

[editor proofgeneral-coq]
MARCHE Claude's avatar
MARCHE Claude committed
633
name = "Emacs/ProofGeneral/Coq"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
634
command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
635

636 637
[editor isabelle-jedit]
name = "Isabelle/jEdit"
638
command = "isabelle why3 -i %f"
639

640
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
641
name = "AltGr-Ergo"
642
command = "altgr-ergo %f"
643 644 645 646

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