src/HOL/Tools/etc/options
author desharna
Sat, 12 Jun 2021 15:37:25 +0200
changeset 73852 adb34395b622
parent 73847 58f6b41efe88
child 74077 b93d8c2ebab0
permissions -rw-r--r--
added support for unbounded max calls to Mirabelle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
     1
(* :mode=isabelle-options: *)
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
     2
59753
wenzelm
parents: 57659
diff changeset
     3
section "Automatically tried tools"
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52645
diff changeset
     4
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52645
diff changeset
     5
public option auto_time_start : real = 1.0
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52645
diff changeset
     6
  -- "initial delay for automatically tried tools (seconds)"
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
     7
52645
e8c1c5612677 clarified some default options;
wenzelm
parents: 52639
diff changeset
     8
public option auto_time_limit : real = 2.0
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
     9
  -- "time limit for automatically tried tools (seconds > 0)"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    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
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    12
  -- "run Nitpick automatically"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    13
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    14
public option auto_sledgehammer : bool = false
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    15
  -- "run Sledgehammer automatically"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    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
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    18
  -- "try standard proof methods automatically"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    19
52645
e8c1c5612677 clarified some default options;
wenzelm
parents: 52639
diff changeset
    20
public option auto_quickcheck : bool = true
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    21
  -- "run Quickcheck automatically"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    22
52645
e8c1c5612677 clarified some default options;
wenzelm
parents: 52639
diff changeset
    23
public option auto_solve_direct : bool = true
52639
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    24
  -- "run solve_direct automatically"
df830310e550 system options for Isabelle/HOL proof tools;
wenzelm
parents:
diff changeset
    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
c1a6c23f70a5 adapted to a9b71c82647b;
wenzelm
parents: 60071
diff changeset
    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
05fb05f94686 added option for noncommercial Vampire
blanchet
parents: 60594
diff changeset
    35
public option vampire_noncommercial : string = "unknown"
05fb05f94686 added option for noncommercial Vampire
blanchet
parents: 60594
diff changeset
    36
  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
05fb05f94686 added option for noncommercial Vampire
blanchet
parents: 60594
diff changeset
    37
73418
7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents: 72988
diff changeset
    38
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
    39
  -- "URL for SystemOnTPTP service"
7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents: 72988
diff changeset
    40
57659
b246943b3aa3 reenabled MaSh for Isabelle2014 release (hopefully)
blanchet
parents: 57566
diff changeset
    41
public option MaSh : string = "sml"
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57462
diff changeset
    42
  -- "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
    43
72299
0c7a74a1c6d9 clarified defaults for nitpick;
wenzelm
parents: 72200
diff changeset
    44
public option kodkod_scala : bool = true
72196
6dba090358d2 invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
wenzelm
parents: 68563
diff changeset
    45
  -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
72200
edaed30360cc more flexible default for max_threads;
wenzelm
parents: 72196
diff changeset
    46
edaed30360cc more flexible default for max_threads;
wenzelm
parents: 72196
diff changeset
    47
public option kodkod_max_threads : int = 0
edaed30360cc more flexible default for max_threads;
wenzelm
parents: 72196
diff changeset
    48
  -- "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
    49
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    50
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    51
section "Mirabelle"
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    52
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    53
option mirabelle_timeout : real = 30
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    54
  -- "default timeout for Mirabelle actions"
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents: 73418
diff changeset
    55
73797
f7ea394490f5 moved stride option from sledgehammer action to main mirabelle
desharna
parents: 73691
diff changeset
    56
option mirabelle_stride : int = 1
f7ea394490f5 moved stride option from sledgehammer action to main mirabelle
desharna
parents: 73691
diff changeset
    57
  -- "default stride for running Mirabelle actions on every nth goal"
f7ea394490f5 moved stride option from sledgehammer action to main mirabelle
desharna
parents: 73691
diff changeset
    58
73852
adb34395b622 added support for unbounded max calls to Mirabelle
desharna
parents: 73847
diff changeset
    59
option mirabelle_max_calls : int = 0
adb34395b622 added support for unbounded max calls to Mirabelle
desharna
parents: 73847
diff changeset
    60
  -- "default max. no. of calls to each Mirabelle action (0: unbounded)"
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73797
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)"