src/HOL/Tools/etc/options

moved stride option from sledgehammer action to main mirabelle

(* :mode=isabelle-options: *)

section "Automatically tried tools"

public option auto_time_start : real = 1.0
  -- "initial delay for automatically tried tools (seconds)"

public option auto_time_limit : real = 2.0
  -- "time limit for automatically tried tools (seconds > 0)"

public option auto_nitpick : bool = false
  -- "run Nitpick automatically"

public option auto_sledgehammer : bool = false
  -- "run Sledgehammer automatically"

public option auto_methods : bool = false
  -- "try standard proof methods automatically"

public option auto_quickcheck : bool = true
  -- "run Quickcheck automatically"

public option auto_solve_direct : bool = true
  -- "run solve_direct automatically"


section "Miscellaneous Tools"

public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
  -- "provers for Sledgehammer (separated by blanks)"

public option sledgehammer_timeout : int = 30
  -- "provers will be interrupted after this time (in seconds)"

public option vampire_noncommercial : string = "unknown"
  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"

public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
  -- "URL for SystemOnTPTP service"

public option MaSh : string = "sml"
  -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"

public option kodkod_scala : bool = true
  -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"

public option kodkod_max_threads : int = 0
  -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)"


section "Mirabelle"

option mirabelle_timeout : real = 30
  -- "default timeout for Mirabelle actions"

option mirabelle_stride : int = 1
  -- "default stride for running Mirabelle actions on every nth goal"

option mirabelle_actions : string = ""
  -- "Mirabelle actions (outer syntax, separated by semicolons)"

option mirabelle_theories : string = ""
  -- "Mirabelle theories (names with optional line range, separated by commas)"