author | wenzelm |
Mon, 24 Aug 2020 17:58:04 +0200 | |
changeset 72200 | edaed30360cc |
parent 72196 | 6dba090358d2 |
child 72299 | 0c7a74a1c6d9 |
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 |
|
68563 | 35 |
public option vampire_noncommercial : string = "unknown" |
36 |
-- "status of Vampire activation for noncommercial use (yes, no, unknown)" |
|
37 |
||
57659
b246943b3aa3
reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents:
57566
diff
changeset
|
38 |
public option MaSh : string = "sml" |
57532 | 39 |
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" |
72196
6dba090358d2
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
wenzelm
parents:
68563
diff
changeset
|
40 |
|
6dba090358d2
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
wenzelm
parents:
68563
diff
changeset
|
41 |
public option kodkod_scala : bool = false |
6dba090358d2
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
wenzelm
parents:
68563
diff
changeset
|
42 |
-- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" |
72200 | 43 |
|
44 |
public option kodkod_max_threads : int = 0 |
|
45 |
-- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" |