1(* :mode=isabelle-options: *) 2 3section "Automatically tried tools" 4 5public option auto_time_start : real = 1.0 6 -- "initial delay for automatically tried tools (seconds)" 7 8public option auto_time_limit : real = 2.0 9 -- "time limit for automatically tried tools (seconds > 0)" 10 11public option auto_nitpick : bool = false 12 -- "run Nitpick automatically" 13 14public option auto_sledgehammer : bool = false 15 -- "run Sledgehammer automatically" 16 17public option auto_methods : bool = false 18 -- "try standard proof methods automatically" 19 20public option auto_quickcheck : bool = true 21 -- "run Quickcheck automatically" 22 23public option auto_solve_direct : bool = true 24 -- "run solve_direct automatically" 25 26 27section "Miscellaneous Tools" 28 29public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" 30 -- "provers for Sledgehammer (separated by blanks)" 31 32public option sledgehammer_timeout : int = 30 33 -- "provers will be interrupted after this time (in seconds)" 34 35public option vampire_noncommercial : string = "unknown" 36 -- "status of Vampire activation for noncommercial use (yes, no, unknown)" 37 38public option MaSh : string = "sml" 39 -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" 40