provers-detection-data.conf 14.7 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-1.30"
6 7 8
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
9 10
version_ok  = "2.0.0"
version_old  = "1.30"
11
version_old = "1.01"
12 13
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
14
driver = "alt_ergo"
15
editor = "altgr-ergo"
16
use_at_auto_level = 1
17

18 19 20 21 22 23 24
[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.]+\\)$"
25 26
version_old = "0.99.1"
version_old = "0.95.2"
27 28
command = "%e -no-rm-eq-existential -timelimit %t %f"
command_steps = "%e -no-rm-eq-existential -steps-bound %S %f"
29
driver = "alt_ergo"
30 31
editor = "altgr-ergo"

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
[ATP alt-ergo-prv]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_old = "1.20.prv"
version_old = "1.10.prv"
version_old = "1.00.prv"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"

MARCHE Claude's avatar
MARCHE Claude committed
48 49
# CVC4 version 1.5
[ATP cvc4-15]
50
name = "CVC4"
51
exec = "cvc4"
52
exec = "cvc4-1.5"
53 54
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
55
version_ok  = "1.5"
56
driver = "cvc4_15"
57 58
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
59 60
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
MARCHE Claude's avatar
MARCHE Claude committed
61
use_at_auto_level = 1
62

63 64
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
65
name = "CVC4"
66 67 68 69
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
70
version_old  = "1.4"
71
driver = "cvc4_14"
72 73 74 75
# --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
76
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
77
use_at_auto_level = 1
78

79
# CVC4 version 1.4, not using SMTLIB bitvectors
80 81
[ATP cvc4]
name = "CVC4"
82
alternative = "noBV"
83 84 85 86
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
87
version_old  = "1.4"
88
driver = "cvc4"
89
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
90 91
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
92
# cvc4 1.4 does not print steps used in --stats anyway
93
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
94

95

96 97 98 99
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
100 101 102 103
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
104 105
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
106 107 108 109
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
version_old = "1.0"
110
driver = "cvc4"
111
command = "%e --lang=smt2 %f"
112

113 114 115 116 117 118 119 120
# 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"
121
driver = "psyche"
122
command = "%e -gplugin dpll_wl %f"
123

124
# CVC3 versions 2.4.x
125
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
126
name = "CVC3"
127
exec = "cvc3"
128
exec = "cvc3-2.4.1"
129
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
130 131
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
132 133
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
134
# the -timeout option is unreliable in CVC3 2.4.1
135
command = "%e -seed 42 %f"
136
driver = "cvc3"
Andrei Paskevich's avatar
Andrei Paskevich committed
137

138
# CVC3 versions 2.x
139
[ATP cvc3]
140
name = "CVC3"
141
exec = "cvc3"
142 143
exec = "cvc3-2.2"
exec = "cvc3-2.1"
144
version_switch = "-version"
145
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
146
version_old = "2.2"
147
version_old = "2.1"
148
command = "%e  -seed 42 -timeout %t %f"
149
driver = "cvc3"
150

151 152 153
[ATP yices]
name = "Yices"
exec = "yices"
154
exec = "yices-1.0.38"
155
version_switch = "--version"
156
version_regexp = "\\([^ \n]+\\)"
157 158 159
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
160 161
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
162
command = "%e"
163
driver = "yices"
164

165 166 167 168
[ATP yices-smt2]
name = "Yices"
exec = "yices-smt2"
exec = "yices-smt2-2.3.0"
Jean-Christophe's avatar
Jean-Christophe committed
169
version_switch = "--version"
170 171
version_regexp = "^Yices \\([^ \n]+\\)$"
version_ok = "2.3.0"
172
command = "%e"
173
driver = "yices-smt2"
Jean-Christophe's avatar
Jean-Christophe committed
174

175 176 177
[ATP eprover]
name = "Eprover"
exec = "eprover"
178 179 180
exec = "eprover-2.0"
exec = "eprover-1.9.1"
exec = "eprover-1.9"
MARCHE Claude's avatar
MARCHE Claude committed
181 182
exec = "eprover-1.8"
exec = "eprover-1.7"
183 184 185
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
186
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
187
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
188 189 190 191
version_ok  = "2.0"
version_old = "1.9.1-001"
version_old = "1.9"
version_old = "1.8-001"
192 193
version_old = "1.7"
version_old = "1.6"
194 195
version_old = "1.5"
version_old = "1.4"
196
command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
197
driver = "eprover"
198
use_at_auto_level = 2
199 200 201

[ATP gappa]
name = "Gappa"
202
exec = "gappa"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
203
exec = "gappa-1.3.2"
204 205
exec = "gappa-1.3.0"
exec = "gappa-1.2.2"
MARCHE Claude's avatar
MARCHE Claude committed
206
exec = "gappa-1.2.0"
207
exec = "gappa-1.1.1"
208
exec = "gappa-1.1.0"
209
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
210
exec = "gappa-0.16.1"
211
exec = "gappa-0.14.1"
212
version_switch = "--version"
213
version_regexp = "Gappa \\([^ \n]*\\)"
214
version_ok = "^1\.[0-3]\..+$"
215
version_old = "^0\.1[1-8]\..+$"
216
command = "%e -Eprecision=70"
217
driver = "gappa"
218

219 220 221
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
222
exec = "mathsat-5.2.2"
223 224 225
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
226
command = "%e -input=smt2 -model -random_seed=80"
227
driver = "mathsat"
228

229 230
[ATP simplify]
name = "Simplify"
231 232 233 234
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
235
version_switch = "-version"
236
version_regexp = "Simplify version \\([^ \n,]+\\)"
237 238
version_old = "1.5.5"
version_old = "1.5.4"
239
command = "%e %f"
240
driver = "simplify"
241

242 243 244 245 246 247
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
248
command = "%e --time-limit %t %f"
249
driver = "metis"
250 251 252 253

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
254 255
exec = "metit-2.4"
exec = "metit-2.2"
256 257
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
258 259
version_ok = "2.4"
version_old = "2.2"
260
command = "%e --time %t %f"
261
driver = "metitarski"
262

263 264 265 266 267 268 269
[ATP polypaver]
name = "PolyPaver"
exec = "polypaver"
exec = "polypaver-0.3"
version_switch = "--version"
version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
version_ok = "0.3"
270
command = "%e -d 2 -m 10 --time=%t %f"
271
driver = "polypaver"
272

273 274 275
[ATP spass]
name = "Spass"
exec = "SPASS"
276
exec = "SPASS-3.7"
277
version_switch = " | grep 'SPASS V'"
278
version_regexp = "SPASS V \\([^ \n\t]+\\)"
279
version_ok = "3.7"
280
command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
281
driver = "spass"
282
use_at_auto_level = 2
283

284 285 286 287 288 289 290
[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"
291
command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
292
driver = "spass_types"
293
use_at_auto_level = 2
294

MARCHE Claude's avatar
MARCHE Claude committed
295 296 297
[ATP vampire]
name = "Vampire"
exec = "vampire"
298
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
299 300
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
301
command = "%e -t %t"
302
driver = "vampire"
303
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
304

305 306 307
[ATP princess]
name = "Princess"
exec = "princess"
308
exec = "princess-2015-12-07"
309
# version_switch = "-h"
310 311
# version_regexp = "(CASC version \\([0-9-]+\\))"
version_regexp = "(release \\([0-9-]+\\))"
312
command = "%e -timeout=%t %f"
313
driver = "princess"
314 315
# version_ok = "2013-05-13"
version_ok = "2015-12-07"
316 317 318 319 320 321 322

[ATP beagle]
name = "Beagle"
exec = "beagle"
exec = "beagle-0.4.1"
# version_switch = "-h"
version_regexp = "version \\([0-9.]+\\)"
323
command = "%e %f"
324
driver = "beagle"
325
version_ok = "0.4.1"
326

MARCHE Claude's avatar
MARCHE Claude committed
327 328 329 330 331 332
[ATP verit]
name = "veriT"
exec = "veriT"
exec = "veriT-201410"
version_switch = "--version"
version_regexp = "version \\([^ \n\r]+\\)"
333
command = "%e --disable-print-success %f"
334
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
335 336
version_ok = "201410"

337 338
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
339
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
340 341
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
342
version_regexp = "version \\([^ \n\r]+\\)"
343
command = "%e --disable-print-success --enable-simp \
344
--enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
345
driver = "verit"
MARCHE Claude's avatar
MARCHE Claude committed
346
version_old = "201310"
347

348
# Z3 >= 4.4.0, with BV support
349
[ATP z3]
350
name = "Z3"
351
exec = "z3"
MARCHE Claude's avatar
MARCHE Claude committed
352
exec = "z3-4.6.0"
353
exec = "z3-4.5.0"
354
exec = "z3-4.4.1"
355 356 357
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
358
version_ok  = "4.6.0"
359
version_ok  = "4.5.0"
MARCHE Claude's avatar
MARCHE Claude committed
360 361
version_old  = "4.4.1"
version_old  = "4.4.0"
362
driver = "z3_440"
363 364
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"
365
use_at_auto_level = 1
366

367 368 369 370 371
# Z3 >= 4.4.0, without BV support
[ATP z3]
name = "Z3"
alternative = "noBV"
exec = "z3"
MARCHE Claude's avatar
MARCHE Claude committed
372
exec = "z3-4.6.0"
373
exec = "z3-4.5.0"
374
exec = "z3-4.4.1"
375 376 377
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
378
version_ok  = "4.6.0"
379
version_ok  = "4.5.0"
MARCHE Claude's avatar
MARCHE Claude committed
380 381
version_old  = "4.4.1"
version_old  = "4.4.0"
382
driver = "z3_432"
383 384
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"
385

MARCHE Claude's avatar
MARCHE Claude committed
386 387
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
388
# Z3 4.3.2 supports Datatypes
MARCHE Claude's avatar
MARCHE Claude committed
389 390 391 392 393
[ATP z3]
name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
394
version_ok  = "4.3.2"
395
driver = "z3_432"
396 397
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
398

399
[ATP z3]
Jean-Christophe's avatar
Jean-Christophe committed
400 401
name = "Z3"
exec = "z3"
402 403
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
404
exec = "z3-4.2"
405 406
exec = "z3-4.1.2"
exec = "z3-4.1.1"
Jean-Christophe's avatar
Jean-Christophe committed
407 408 409
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
410
version_old = "4.3.1"
411 412 413 414 415
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
416
driver = "z3"
417
command = "%e -smt2 -rs:42 %f"
Jean-Christophe's avatar
Jean-Christophe committed
418

419
[ATP z3]
420
name = "Z3"
421
exec = "z3"
422
exec = "z3-3.2"
423 424
exec = "z3-3.1"
exec = "z3-3.0"
425 426
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
427
version_old = "3.2"
428 429
version_old = "3.1"
version_old = "3.0"
430
driver = "z3"
Andrei Paskevich's avatar
Andrei Paskevich committed
431
# the -T is unreliable in Z3 3.2
432
command = "%e -smt2 -rs:42 %f"
433

434
[ATP z3]
François Bobot's avatar
François Bobot committed
435 436
name = "Z3"
exec = "z3"
437 438 439 440
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
441 442
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
443 444
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
445
driver = "z3"
446
command = "%e -smt2 -rs:42 \
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
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

466
[ATP z3]
467
name = "Z3"
468 469
exec = "z3"
exec = "z3-2.2"
470 471
exec = "z3-2.1"
exec = "z3-1.3"
472 473
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
474 475
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
476
version_old = "1.3"
477
command = "%e -smt %f"
478
driver = "z3_smtv1"
479

480 481 482
[ATP zenon]
name = "Zenon"
exec = "zenon"
483
exec = "zenon-0.8.0"
484 485 486
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
487
version_ok = "0.8.0"
488
version_ok = "0.7.1"
489
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
490
driver = "zenon"
491

492 493 494 495 496
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
497
version_ok = "0.4.1"
498
command = "%e -p0 -itptp -max-size %mM -max-time %ts %f"
499
driver = "zenon_modulo"
500

501 502 503
[ATP iprover]
name = "iProver"
exec = "iprover"
504
exec = "iprover-0.8.1"
505 506 507
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
508
command = "%e --fof true --out_options none \
509 510
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
511
driver = "iprover"
512

513 514 515 516 517
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
518
version_ok = "9.0"
519 520
version_ok = "8.0"
version_ok = "7.0"
521
command = "%e -noprompt"
522
driver = "mathematica"
523

524 525 526 527 528 529 530
# 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]+\\)"
531
version_ok = "8.7.1"
532
version_ok = "8.7.0"
MARCHE Claude's avatar
MARCHE Claude committed
533
version_ok = "8.6.1"
534
version_ok = "8.6"
535
command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
536
driver = "coq"
537 538
editor = "coqide"

539 540 541 542 543 544 545
# 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]+\\)"
546 547
version_ok = "8.5pl3"
version_ok = "8.5pl2"
548
version_ok = "8.5pl1"
549 550
version_ok = "8.5"
command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
551
driver = "coq"
552 553
editor = "coqide"

554 555
[ITP coq]
name = "Coq"
556
compile_time_support = true
557
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
558
version_switch = "-v"
559
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
560
version_ok = "^8\.4pl[1-6]$"
561
version_ok = "8.4"
562
command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
563
driver = "coq"
564 565
editor = "coqide"

566 567
[ITP pvs]
name = "PVS"
568
compile_time_support = true
569 570 571
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
572
version_ok = "6.0"
573
version_bad = "^[0-5]\..+$"
574
command = "%l/why3-call-pvs %l proveit -f %f"
575
driver = "pvs"
576
in_place = true
577
editor = "pvs"
578

579 580 581 582
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
583
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
584
version_ok = "2016-1"
585
version_bad = "2017"
586
version_bad = "2016"
587
command = "%e why3 -b %f"
588
driver = "isabelle2016-1"
589
in_place = true
590
editor = "isabelle-jedit"
591 592 593 594 595 596

[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
597
version_ok = "2017"
598
version_bad = "2016-1"
599
version_bad = "2016"
600
command = "%e why3 -b %f"
601
driver = "isabelle2017"
602
in_place = true
603
editor = "isabelle-jedit"
604

605 606
[editor pvs]
name = "PVS"
607
command = "%l/why3-call-pvs %l pvs %f"
608 609

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
610
name = "CoqIDE"
611
command = "coqide -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
612 613

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

618 619
[editor isabelle-jedit]
name = "Isabelle/jEdit"
620
command = "isabelle why3 -i %f"
621

622
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
623
name = "AltGr-Ergo"
624
command = "altgr-ergo %f"
625 626 627 628

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