author | wenzelm |
Sat, 02 Oct 2021 12:15:37 +0200 | |
changeset 74409 | 83d2208252d1 |
parent 74376 | 1cc630940147 |
child 74845 | 91ee232b4211 |
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 |
||
72988
52ba78df4088
disable auto_nitpick for now: spurious problems with non-termination e.g. in HOL-Hoare examples;
wenzelm
parents:
72299
diff
changeset
|
11 |
public option auto_nitpick : bool = false |
52639 | 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 |
|
74409
83d2208252d1
clarified sledgehammer_provers, following d8dc8fdc46fc;
wenzelm
parents:
74376
diff
changeset
|
29 |
public option sledgehammer_provers : string = "cvc4 vampire verit e spass z3 zipperposition" |
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 |
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
72988
diff
changeset
|
35 |
public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply" |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
72988
diff
changeset
|
36 |
-- "URL for SystemOnTPTP service" |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
72988
diff
changeset
|
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 |
|
72299 | 41 |
public option kodkod_scala : bool = true |
72196
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)" |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
46 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
47 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
48 |
section "Mirabelle" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
49 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
50 |
option mirabelle_timeout : real = 30 |
74077
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
73852
diff
changeset
|
51 |
-- "timeout in seconds for each action" |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
52 |
|
73797
f7ea394490f5
moved stride option from sledgehammer action to main mirabelle
desharna
parents:
73691
diff
changeset
|
53 |
option mirabelle_stride : int = 1 |
74077
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
73852
diff
changeset
|
54 |
-- "run actions on every nth goal (0: uniform distribution)" |
73797
f7ea394490f5
moved stride option from sledgehammer action to main mirabelle
desharna
parents:
73691
diff
changeset
|
55 |
|
73852
adb34395b622
added support for unbounded max calls to Mirabelle
desharna
parents:
73847
diff
changeset
|
56 |
option mirabelle_max_calls : int = 0 |
74077
b93d8c2ebab0
added automatic uniform stride option to Mirabelle
desharna
parents:
73852
diff
changeset
|
57 |
-- "max. no. of calls to each action (0: unbounded)" |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
58 |
|
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
59 |
option mirabelle_output_dir : string = "mirabelle" |
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
60 |
-- "output directory for log files and generated artefacts" |
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
74077
diff
changeset
|
61 |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
62 |
option mirabelle_actions : string = "" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
63 |
-- "Mirabelle actions (outer syntax, separated by semicolons)" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
64 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
65 |
option mirabelle_theories : string = "" |
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73418
diff
changeset
|
66 |
-- "Mirabelle theories (names with optional line range, separated by commas)" |