why3ide-doc.conf 1.55 KB
Newer Older
1
[editor coqide]
2
command = "true %f"
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
name = "CoqIDE"

[ide]
allow_source_editing = true
current_tab = 0
default_editor = "editor %f"
default_prover = ""
error_color = "orange"
font_size = 11
goal_color = "gold"
iconset = "fatcow"
intro_premises = true
max_boxes = 16
neg_premise_color = "pink"
premise_color = "chartreuse"
print_coercions = true
19
print_attributes = false
20 21 22 23
print_locs = false
print_time_limit = false
saving_policy = 2
show_full_context = false
24
task_height = 220
25 26 27 28 29 30
tree_width = 384
verbose = 0
window_height = 768
window_width = 1024

[main]
31
loadpath = "/home/cmarche/why3.master/share/stdlib"
32 33 34 35 36 37
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5

[prover]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38
command = "coqtop -batch -R %l/coq Why3 -l %f"
39 40 41 42 43 44
driver = "coq"
editor = "coqide"
in_place = false
interactive = true
name = "Coq"
shortcut = "coq"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
45
version = "8.7.2"
46 47 48

[prover]
command = "alt-ergo -timelimit %t %f"
49
command_steps = "alt-ergo-2.2.0 -steps-bound %S %f"
50 51 52 53 54
driver = "alt_ergo"
in_place = false
interactive = false
name = "Alt-Ergo"
shortcut = "alt-ergo"
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
version = "2.2.0"

[prover]
alternative = "counterexamples"
command = "cvc4-1.6 --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
driver = "cvc4_16_counterexample"
editor = ""
in_place = false
interactive = false
name = "CVC4"
shortcut = "cvc4-ce"
version = "1.6"

[prover]
command = "cvc4-1.6 --tlimit=%t000 --lang=smt2 %f"
command_steps = "cvc4-1.6 --stats --rlimit=%S --lang=smt2 %f"
driver = "cvc4_16"
editor = ""
in_place = false
interactive = false
name = "CVC4"
shortcut = "cvc4"
version = "1.6"