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 13.6 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.00.prv"
5
version_switch = "-version"
MARCHE Claude's avatar
MARCHE Claude committed
6
7
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok  = "1.00.prv"
8
9
10
11
# %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"
12
13
14
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"

15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
[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"

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

# CVC4 version 1.4
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
54
version_ok  = "1.4"
55
driver = "drivers/cvc4_14.drv"
56
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
57
58
59
# 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
60
61
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"

David Hauzar's avatar
David Hauzar committed
62

63
64
65
66
# CVC4 version 1.0 to 1.3
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
67
68
69
70
exec = "cvc4-1.3"
exec = "cvc4-1.2"
exec = "cvc4-1.1"
exec = "cvc4-1.0"
71
72
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
73
74
75
76
version_old = "1.3"
version_old = "1.2"
version_old = "1.1"
version_old = "1.0"
77
driver = "drivers/cvc4.drv"
78
command = "%l/why3-cpulimit %t %m -s %e --lang=smt2 %f"
79

80
81
82
83
84
85
86
87
88
89
90
# 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"

91
# CVC3 versions 2.4.x
92
[ATP cvc3]
Andrei Paskevich's avatar
Andrei Paskevich committed
93
name = "CVC3"
94
exec = "cvc3"
95
exec = "cvc3-2.4.1"
96
exec = "cvc3-2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
97
98
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
99
100
version_ok  = "2.4.1"
version_old = "2.4"
Andrei Paskevich's avatar
Andrei Paskevich committed
101
# the -timeout option is unreliable in CVC3 2.4.1
102
command = "%l/why3-cpulimit %t %m -s %e -seed 42 %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
103
104
driver = "drivers/cvc3.drv"

105
# CVC3 versions 2.x
106
[ATP cvc3]
MARCHE Claude's avatar
MARCHE Claude committed
107
name = "CVC3"
108
exec = "cvc3"
109
110
exec = "cvc3-2.2"
exec = "cvc3-2.1"
MARCHE Claude's avatar
MARCHE Claude committed
111
version_switch = "-version"
112
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
113
version_old = "2.2"
MARCHE Claude's avatar
MARCHE Claude committed
114
version_old = "2.1"
115
command = "%l/why3-cpulimit %T %m -s %e  -seed 42 -timeout %t %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
116
driver = "drivers/cvc3.drv"
117

118
119
120
[ATP yices]
name = "Yices"
exec = "yices"
121
exec = "yices-1.0.38"
122
version_switch = "--version"
123
version_regexp = "\\([^ \n]+\\)"
124
125
126
version_ok = "1.0.38"
version_old = "^1\.0\.3[0-7]$"
version_old = "^1\.0\.2[5-9]$"
127
128
version_old = "^1\.0\.2[0-4]$"
version_old = "^1\.0\.1\.*$"
129
command = "%l/why3-cpulimit %t %m -s %e"
130
131
driver = "drivers/yices.drv"

132
133
134
135
[ATP yices-smt2]
name = "Yices"
exec = "yices-smt2"
exec = "yices-smt2-2.3.0"
136
version_switch = "--version"
137
138
version_regexp = "^Yices \\([^ \n]+\\)$"
version_ok = "2.3.0"
139
command = "%l/why3-cpulimit %t %m -s %e"
140
driver = "drivers/yices-smt2.drv"
141

142
143
144
[ATP eprover]
name = "Eprover"
exec = "eprover"
MARCHE Claude's avatar
MARCHE Claude committed
145
146
exec = "eprover-1.8"
exec = "eprover-1.7"
147
148
149
exec = "eprover-1.6"
exec = "eprover-1.5"
exec = "eprover-1.4"
150
version_switch = "--version"
Andrei Paskevich's avatar
Andrei Paskevich committed
151
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
MARCHE Claude's avatar
MARCHE Claude committed
152
version_ok  = "1.8-001"
153
154
version_old = "1.7"
version_old = "1.6"
155
156
version_old = "1.5"
version_old = "1.4"
157
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
158
driver = "drivers/eprover.drv"
MARCHE Claude's avatar
MARCHE Claude committed
159
160
161

[ATP gappa]
name = "Gappa"
162
exec = "gappa"
MARCHE Claude's avatar
MARCHE Claude committed
163
exec = "gappa-1.2.0"
164
exec = "gappa-1.1.1"
165
exec = "gappa-1.1.0"
166
exec = "gappa-1.0.0"
MARCHE Claude's avatar
MARCHE Claude committed
167
exec = "gappa-0.16.1"
168
exec = "gappa-0.14.1"
MARCHE Claude's avatar
MARCHE Claude committed
169
version_switch = "--version"
170
version_regexp = "Gappa \\([^ \n]*\\)"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
171
version_ok = "^1\.[0-2]\..+$"
172
version_old = "^0\.1[1-8]\..+$"
173
command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
174
175
driver = "drivers/gappa.drv"

176
177
178
[ATP mathsat]
name = "MathSAT5"
exec = "mathsat"
179
exec = "mathsat-5.2.2"
180
181
182
version_switch = "-version"
version_regexp = "MathSAT5 version \\([^ \n]+\\)"
version_ok  = "5.2.2"
183
command = "%l/why3-cpulimit %t %m -s %e -input=smt2 -model -random_seed=80 %f"
184
185
driver = "drivers/mathsat.drv"

MARCHE Claude's avatar
MARCHE Claude committed
186
187
[ATP simplify]
name = "Simplify"
188
189
190
191
exec = "Simplify"
exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
MARCHE Claude's avatar
MARCHE Claude committed
192
version_switch = "-version"
193
version_regexp = "Simplify version \\([^ \n,]+\\)"
194
195
version_old = "1.5.5"
version_old = "1.5.4"
196
command = "%l/why3-cpulimit %t %m -s %e %f"
197
198
driver = "drivers/simplify.drv"

199
200
201
202
203
204
[ATP metis]
name = "Metis"
exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
205
206
207
208
# %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"
209
210
211
212
213
driver = "drivers/metis.drv"

[ATP metitarski]
name = "MetiTarski"
exec = "metit"
MARCHE Claude's avatar
MARCHE Claude committed
214
215
exec = "metit-2.4"
exec = "metit-2.2"
216
217
version_switch = "-v"
version_regexp = "MetiTarski \\([^ \n,]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
218
219
version_ok = "2.4"
version_old = "2.2"
220
command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
221
222
driver = "drivers/metitarski.drv"

223
224
225
[ATP spass]
name = "Spass"
exec = "SPASS"
226
exec = "SPASS-3.7"
227
version_switch = " | grep 'SPASS V'"
228
version_regexp = "SPASS V \\([^ \n\t]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
229
version_ok = "3.7"
230
command = "%l/why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
MARCHE Claude's avatar
MARCHE Claude committed
231
driver = "drivers/spass.drv"
MARCHE Claude's avatar
MARCHE Claude committed
232

233
234
235
236
237
238
239
[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"
240
command = "%l/why3-cpulimit %T %m -s %e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
241
242
driver = "drivers/spass_types.drv"

MARCHE Claude's avatar
MARCHE Claude committed
243
244
245
[ATP vampire]
name = "Vampire"
exec = "vampire"
246
exec = "vampire-0.6"
MARCHE Claude's avatar
MARCHE Claude committed
247
248
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
249
command = "%l/why3-cpulimit %T %m -s %e -t %t"
MARCHE Claude's avatar
MARCHE Claude committed
250
driver = "drivers/vampire.drv"
251
version_ok = "0.6"
MARCHE Claude's avatar
MARCHE Claude committed
252

253
254
255
256
[ATP princess]
name = "Princess"
exec = "princess"
# version_switch = "-h"
257
version_regexp = "(CASC version \\([0-9-]+\\))"
258
command = "%l/why3-cpulimit %T 0 -s %e -timeout=%t %f"
259
driver = "drivers/princess.drv"
260
261
262
263
264
265
266
267
version_ok = "2013-05-13"

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

MARCHE Claude's avatar
MARCHE Claude committed
272
273
274
275
276
277
278
279
280
281
[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"

282
283
[ATP verit]
name = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
284
exec = "veriT"
MARCHE Claude's avatar
MARCHE Claude committed
285
286
exec = "veriT-201310"
version_switch = "--version"
MARCHE Claude's avatar
MARCHE Claude committed
287
version_regexp = "version \\([^ \n\r]+\\)"
288
289
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"
290
driver = "drivers/verit.drv"
MARCHE Claude's avatar
MARCHE Claude committed
291
version_old = "201310"
292

MARCHE Claude's avatar
MARCHE Claude committed
293
294
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
295
# Z3 4.3.2 supports Datatypes
MARCHE Claude's avatar
MARCHE Claude committed
296
297
298
[ATP z3]
name = "Z3"
exec = "z3"
Andrei Paskevich's avatar
Andrei Paskevich committed
299
exec = "z3-4.3.3"
MARCHE Claude's avatar
MARCHE Claude committed
300
301
302
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
303
version_ok  = "4.3.3"
304
version_ok = "4.3.2"
305
driver = "drivers/z3_432.drv"
MARCHE Claude's avatar
MARCHE Claude committed
306
307
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"

308
[ATP z3]
309
310
name = "Z3"
exec = "z3"
311
312
exec = "z3-4.3.1"
exec = "z3-4.3.0"
MARCHE Claude's avatar
MARCHE Claude committed
313
exec = "z3-4.2"
314
315
exec = "z3-4.1.2"
exec = "z3-4.1.1"
316
317
318
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
Andrei Paskevich's avatar
Andrei Paskevich committed
319
version_old = "4.3.1"
320
321
322
323
324
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
325
driver = "drivers/z3.drv"
326
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
327

328
[ATP z3]
329
name = "Z3"
330
exec = "z3"
331
exec = "z3-3.2"
332
333
exec = "z3-3.1"
exec = "z3-3.0"
334
335
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
336
version_old = "3.2"
337
338
339
version_old = "3.1"
version_old = "3.0"
driver = "drivers/z3.drv"
Andrei Paskevich's avatar
Andrei Paskevich committed
340
# the -T is unreliable in Z3 3.2
341
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
342

343
[ATP z3]
François Bobot's avatar
François Bobot committed
344
345
name = "Z3"
exec = "z3"
346
347
348
349
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
350
351
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
352
353
version_old = "^2\.2.+$"
version_old = "^2\.1[6-9]$"
Andrei Paskevich's avatar
Andrei Paskevich committed
354
driver = "drivers/z3.drv"
355
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 \
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
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

375
[ATP z3]
376
name = "Z3"
377
378
exec = "z3"
exec = "z3-2.2"
379
380
exec = "z3-2.1"
exec = "z3-1.3"
381
382
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
383
384
version_old = "^2\.1[0-5]$"
version_old = "^2\.[0-9]$"
385
version_old = "1.3"
386
command = "%l/why3-cpulimit %t %m -s %e -smt %f"
Andrei Paskevich's avatar
Andrei Paskevich committed
387
driver = "drivers/z3_smtv1.drv"
388

389
390
391
[ATP zenon]
name = "Zenon"
exec = "zenon"
392
exec = "zenon-0.8.0"
393
394
395
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
396
version_ok = "0.8.0"
397
version_ok = "0.7.1"
398
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
399
400
driver = "drivers/zenon.drv"

401
402
403
404
405
[ATP zenon_modulo]
name = "Zenon Modulo"
exec = "zenon_modulo"
version_switch = "-v"
version_regexp = "zenon_modulo version \\([0-9.]+\\)"
406
version_ok = "0.4.1"
407
408
409
command = "%l/why3-cpulimit %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon_modulo.drv"

410
411
412
[ATP iprover]
name = "iProver"
exec = "iprover"
413
exec = "iprover-0.8.1"
414
415
416
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
417
command = "%l/why3-cpulimit %T %m -s %e --fof true --out_options none \
418
419
--time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \
\"eprover --cnf --tstp-format \" %f"
420
421
driver = "drivers/iprover.drv"

Daisuke Ishii's avatar
Daisuke Ishii committed
422
423
424
425
426
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
427
version_ok = "9.0"
Daisuke Ishii's avatar
Daisuke Ishii committed
428
429
version_ok = "8.0"
version_ok = "7.0"
430
command = "%l/why3-cpulimit %t %m -s %e -noprompt"
Daisuke Ishii's avatar
Daisuke Ishii committed
431
432
driver = "drivers/mathematica.drv"

433
434
435
436
437
438
439
440
441
[ATP safeprover]
name = "SafeProver"
exec = "safeprover"
version_switch = "-version"
version_regexp = "The safe prover, version \\([^ \n\t]+\\)"
version_ok = "0.0.0"
command = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/safeprover.drv"

MARCHE Claude's avatar
MARCHE Claude committed
442
443
[ITP coq]
name = "Coq"
444
compile_time_support = true
445
exec = "coqtop -batch"
MARCHE Claude's avatar
MARCHE Claude committed
446
version_switch = "-v"
447
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
MARCHE Claude's avatar
MARCHE Claude committed
448
version_ok = "8.4pl6"
MARCHE Claude's avatar
MARCHE Claude committed
449
version_ok = "8.4pl5"
450
version_ok = "8.4pl4"
Andrei Paskevich's avatar
Andrei Paskevich committed
451
version_ok = "8.4pl3"
452
version_ok = "8.4pl2"
MARCHE Claude's avatar
MARCHE Claude committed
453
version_ok = "8.4pl1"
454
version_ok = "8.4"
455
command = "%l/why3-cpulimit 0 %m -s %e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
456
457
458
driver = "drivers/coq.drv"
editor = "coqide"

459
460
[ITP pvs]
name = "PVS"
461
compile_time_support = true
462
463
464
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
465
version_ok = "6.0"
466
version_bad = "^[0-5]\..+$"
467
468
# 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"
469
driver = "drivers/pvs.drv"
470
in_place = true
471
editor = "pvs"
472

473
474
475
476
[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
Stefan Berghofer's avatar
Stefan Berghofer committed
477
478
479
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
version_ok = "2015"
version_bad = "2014"
480
481
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
482
483
driver = "drivers/isabelle2015.drv"
in_place = true
484
editor = "isabelle2015-jedit"
485
486
487
488
489
490
491
492
493
494
495

[ITP isabelle]
name = "Isabelle"
exec = "isabelle"
version_switch = "version"
version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
version_ok = "2014"
version_bad = "2015"
# not why3-cpulimit 0 %m because isabelle needs more memory at start-up
command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
driver = "drivers/isabelle2014.drv"
496
in_place = true
497
editor = "isabelle2014-jedit"
498

499
500
[editor pvs]
name = "PVS"
501
command = "%l/why3-call-pvs %l pvs %f"
502
503

[editor coqide]
MARCHE Claude's avatar
MARCHE Claude committed
504
name = "CoqIDE"
MARCHE Claude's avatar
MARCHE Claude committed
505
command = "coqide -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
506
507

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

512
513
[editor isabelle2015-jedit]
name = "Isabelle2015/jEdit"
Stefan Berghofer's avatar
Stefan Berghofer committed
514
command = "isabelle why3 -i %f"
515

516
517
518
519
520
521
522
523
[editor isabelle2014-jedit]
name = "Isabelle2014/jEdit"
command = "isabelle why3 -i jedit %f"

[editor isabelle2014-proofgeneral]
name = "Isabelle2014/Emacs/ProofGeneral"
command = "isabelle why3 -i emacs %f"

524
[editor altgr-ergo]
MARCHE Claude's avatar
MARCHE Claude committed
525
name = "AltGr-Ergo"
526
command = "altgr-ergo %f"
527
528
529
530

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