1(* :mode=isabelle-options: *)
2
3section "Automatically tried tools"
4
5public option auto_time_start : real = 1.0
6  -- "initial delay for automatically tried tools (seconds)"
7
8public option auto_time_limit : real = 2.0
9  -- "time limit for automatically tried tools (seconds > 0)"
10
11public option auto_nitpick : bool = false
12  -- "run Nitpick automatically"
13
14public option auto_sledgehammer : bool = false
15  -- "run Sledgehammer automatically"
16
17public option auto_methods : bool = false
18  -- "try standard proof methods automatically"
19
20public option auto_quickcheck : bool = true
21  -- "run Quickcheck automatically"
22
23public option auto_solve_direct : bool = true
24  -- "run solve_direct automatically"
25
26
27section "Miscellaneous Tools"
28
29public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
30  -- "provers for Sledgehammer (separated by blanks)"
31
32public option sledgehammer_timeout : int = 30
33  -- "provers will be interrupted after this time (in seconds)"
34
35public option vampire_noncommercial : string = "unknown"
36  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
37
38public option MaSh : string = "sml"
39  -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
40