| author | wenzelm |
| Wed, 04 Oct 2017 12:00:53 +0200 | |
| changeset 66787 | 64b47495676d |
| parent 60594 | c1a6c23f70a5 |
| child 68563 | 05fb05f94686 |
| permissions | -rw-r--r-- |
| 52639 | 1 |
(* :mode=isabelle-options: *) |
2 |
||
| 59753 | 3 |
section "Automatically tried tools" |
| 52651 | 4 |
|
5 |
public option auto_time_start : real = 1.0 |
|
6 |
-- "initial delay for automatically tried tools (seconds)" |
|
| 52639 | 7 |
|
| 52645 | 8 |
public option auto_time_limit : real = 2.0 |
| 52639 | 9 |
-- "time limit for automatically tried tools (seconds > 0)" |
10 |
||
11 |
public option auto_nitpick : bool = false |
|
12 |
-- "run Nitpick automatically" |
|
13 |
||
14 |
public option auto_sledgehammer : bool = false |
|
15 |
-- "run Sledgehammer automatically" |
|
16 |
||
|
52717
da7bf8b3d24a
clarified option name, with improved sort order wrt. "time" options;
wenzelm
parents:
52651
diff
changeset
|
17 |
public option auto_methods : bool = false |
| 52639 | 18 |
-- "try standard proof methods automatically" |
19 |
||
| 52645 | 20 |
public option auto_quickcheck : bool = true |
| 52639 | 21 |
-- "run Quickcheck automatically" |
22 |
||
| 52645 | 23 |
public option auto_solve_direct : bool = true |
| 52639 | 24 |
-- "run solve_direct automatically" |
25 |
||
|
53057
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
52717
diff
changeset
|
26 |
|
|
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
52717
diff
changeset
|
27 |
section "Miscellaneous Tools" |
|
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
52717
diff
changeset
|
28 |
|
| 60594 | 29 |
public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" |
|
60071
323feed18a92
clarified sledgehammer options to approximate old-style diagnostic command;
wenzelm
parents:
59960
diff
changeset
|
30 |
-- "provers for Sledgehammer (separated by blanks)" |
|
56623
4675df68450e
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents:
55007
diff
changeset
|
31 |
|
|
53057
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
52717
diff
changeset
|
32 |
public option sledgehammer_timeout : int = 30 |
|
60071
323feed18a92
clarified sledgehammer options to approximate old-style diagnostic command;
wenzelm
parents:
59960
diff
changeset
|
33 |
-- "provers will be interrupted after this time (in seconds)" |
|
53057
e18a028b345c
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
wenzelm
parents:
52717
diff
changeset
|
34 |
|
|
57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57566
diff
changeset
|
35 |
public option MaSh : string = "sml" |
| 57532 | 36 |
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" |