diff --git a/src/HOL/Mirabelle.thy b/src/HOL/Mirabelle.thy --- a/src/HOL/Mirabelle.thy +++ b/src/HOL/Mirabelle.thy @@ -1,28 +1,29 @@ (* Title: HOL/Mirabelle.thy Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken *) theory Mirabelle imports Sledgehammer Predicate_Compile Presburger begin +ML_file \Tools/Mirabelle/mirabelle_util.ML\ ML_file \Tools/Mirabelle/mirabelle.ML\ ML \ signature MIRABELLE_ACTION = sig val make_action : Mirabelle.action_context -> string * Mirabelle.action end \ ML_file \Tools/Mirabelle/mirabelle_arith.ML\ ML_file \Tools/Mirabelle/mirabelle_metis.ML\ ML_file \Tools/Mirabelle/mirabelle_presburger.ML\ ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ ML_file \Tools/Mirabelle/mirabelle_sledgehammer.ML\ ML_file \Tools/Mirabelle/mirabelle_try0.ML\ end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.ML b/src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML @@ -1,348 +1,353 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich *) signature MIRABELLE = sig (*core*) type action_context = {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T} type command = {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} type action = {run_action: command -> string, finalize: unit -> string} val register_action: string -> (action_context -> string * action) -> unit (*utility functions*) val print_exn: exn -> string val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list val theorems_of_sucessful_proof: Toplevel.state -> thm list val get_argument : (string * string) list -> string * string -> string val get_int_argument : (string * string) list -> string * int -> int val get_bool_argument : (string * string) list -> string * bool -> bool val cpu_time : ('a -> 'b) -> 'a -> 'b * int end structure Mirabelle : MIRABELLE = struct (** Mirabelle core **) (* concrete syntax *) fun read_actions str = let val thy = \<^theory>; val ctxt = Proof_Context.init_global thy val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords thy) fun read_actions () = Parse.read_embedded ctxt keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) (Input.string str) fun split_name_label (name, args) labels = (case String.tokens (fn c => c = #".") name of [name] => (("", name, args), labels) | [label, name] => (if Symtab.defined labels label then error ("Action label '" ^ label ^ "' already defined.") else (); ((label, name, args), Symtab.insert_set label labels)) | _ => error "Cannot parse action") in try read_actions () |> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty)) end (* actions *) type command = {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; type action_context = {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T}; type action = {run_action: command -> string, finalize: unit -> string}; local val actions = Synchronized.var "Mirabelle.actions" (Symtab.empty : (action_context -> string * action) Symtab.table); in fun register_action name make_action = (if name = "" then error "Registering unnamed Mirabelle action" else (); Synchronized.change actions (Symtab.map_default (name, make_action) (fn f => (warning ("Redefining Mirabelle action: " ^ quote name); f)))); fun get_action name = Symtab.lookup (Synchronized.value actions) name; end (* apply actions *) fun print_exn exn = (case exn of Timeout.TIMEOUT _ => "timeout" | ERROR msg => "error: " ^ msg | exn => "exception: " ^ General.exnMessage exn); fun run_action_function f = f () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else print_exn exn; fun make_action_path ({index, label, name, ...} : action_context) = Path.basic (if label = "" then string_of_int index ^ "." ^ name else label); fun initialize_action (make_action : action_context -> string * action) context = let val (s, action) = make_action context val action_path = make_action_path context; val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "initialize"); val () = if s <> "" then Export.export \<^theory> export_name [XML.Text s] else () in action end fun finalize_action ({finalize, ...} : action) context = let val s = run_action_function finalize; val action_path = make_action_path context; val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); in if s <> "" then Export.export \<^theory> export_name [XML.Text s] else () end fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) = let val thy = Proof.theory_of pre; val action_path = make_action_path context; val goal_name_path = Path.basic (#name command) val line_path = Path.basic (string_of_int (the (Position.line_of pos))); val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + line_path + offset_path); val s = run_action_function (fn () => run_action command); in if s <> "" then Export.export thy export_name [XML.Text s] else () end; (* theory line range *) local val theory_name = Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) >> Symbol_Pos.content; val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); val end_line = Symbol_Pos.$$ ":" |-- line; val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; in fun read_theory_range str = (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of SOME res => res | NONE => error ("Malformed specification of theory line range: " ^ quote str)); end; fun check_theories strs = let fun theory_import_name s = #theory_name (Resources.import_name (Session.get_name ()) Path.current s); val theories = map read_theory_range strs |> map (apfst theory_import_name); fun get_theory name = if null theories then SOME NONE else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; fun check_line NONE _ = false | check_line _ NONE = true | check_line (SOME NONE) _ = true | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; fun check_pos range = check_line range o Position.line_of; in check_pos o get_theory end; (* presentation hook *) val whitelist = ["apply", "by", "proof"]; val _ = Build.add_hook (fn qualifier => fn loaded_theories => let val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; val actions = (case read_actions mirabelle_actions of SOME actions => actions | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); in if null actions then () else let val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; + val mirabelle_randomize = Options.default_int \<^system_option>\mirabelle_randomize\; val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; val mirabelle_output_dir = Options.default_string \<^system_option>\mirabelle_output_dir\; val check_theory = check_theories (space_explode "," mirabelle_theories); fun make_commands (thy_index, (thy, segments)) = let val thy_long_name = Context.theory_long_name thy; val check_thy = check_theory thy_long_name; fun make_command {command = tr, prev_state = st, state = st', ...} = let val name = Toplevel.name_of tr; val pos = Toplevel.pos_of tr; in if Context.proper_subthy (\<^theory>, thy) andalso can (Proof.assert_backward o Toplevel.proof_of) st andalso member (op =) whitelist name andalso check_thy pos then SOME {theory_index = thy_index, name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} else NONE end; in if Resources.theory_qualifier thy_long_name = qualifier then map_filter make_command segments else [] end; (* initialize actions *) val contexts = actions |> map_index (fn (n, (label, name, args)) => let val make_action = (case get_action name of SOME f => f | NONE => error "Unknown action"); val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label; val output_dir = Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir); val context = {index = n, label = label, name = name, arguments = args, timeout = mirabelle_timeout, output_dir = output_dir}; in (initialize_action make_action context, context) end); in (* run actions on all relevant goals *) loaded_theories |> map_index I |> maps make_commands + |> (if mirabelle_randomize <= 0 then + I + else + fst o MLCG.shuffle (MLCG.initialize mirabelle_randomize)) |> (fn xs => fold_map (fn x => fn i => ((i, x), i + 1)) xs 0) |> (fn (indexed_commands, commands_length) => let val stride = if mirabelle_stride <= 0 then Integer.max 1 (commands_length div mirabelle_max_calls) else mirabelle_stride in maps (fn (n, command) => let val (m, k) = Integer.div_mod (n + 1) stride in if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then map (fn context => (context, command)) contexts else [] end) indexed_commands end) |> Par_List.map (fn ((action, context), command) => apply_action action context command); (* finalize actions *) List.app (uncurry finalize_action) contexts end end); (* Mirabelle utility functions *) fun can_apply time tac st = let val {context = ctxt, facts, goal} = Proof.goal st; val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); in (case try (Timeout.apply time (Seq.pull o full_tac)) goal of SOME (SOME _) => true | _ => false) end; local fun fold_body_thms f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = Proofterm.thm_node_name thm_node; val prop = Proofterm.thm_node_prop thm_node; val body = Future.join (Proofterm.thm_node_body thm_node); val (x', seen') = app (n + (if name = "" then 0 else 1)) body (x, Inttab.update (i, ()) seen); in (x' |> n = 0 ? f (name, prop, body), seen') end); in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; in fun theorems_in_proof_term thy thm = let val all_thms = Global_Theory.all_thms_of thy true; fun collect (s, _, _) = if s <> "" then insert (op =) s else I; fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; fun resolve_thms names = map_filter (member_of names) all_thms; in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; end; fun theorems_of_sucessful_proof st = (case try Toplevel.proof_of st of NONE => [] | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); fun get_argument arguments (key, default) = the_default default (AList.lookup (op =) arguments key); fun get_int_argument arguments (key, default) = (case Option.map Int.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun get_bool_argument arguments (key, default) = (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun cpu_time f x = let val ({cpu, ...}, y) = Timing.timing f x in (y, Time.toMilliseconds cpu) end; end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.scala b/src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala @@ -1,237 +1,240 @@ /* Title: HOL/Tools/Mirabelle/mirabelle.scala Author: Makarius Isabelle/Scala front-end for Mirabelle. */ package isabelle.mirabelle import isabelle._ object Mirabelle { /* actions and options */ def action_names(): List[String] = { val Pattern = """Mirabelle action: "(\w+)".*""".r (for { file <- File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, pred = _.getName.endsWith(".ML")) line <- split_lines(File.read(file)) name <- line match { case Pattern(a) => Some(a) case _ => None } } yield name).sorted } def sledgehammer_options(): List[String] = { val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) } /* main mirabelle */ def mirabelle( options: Options, actions: List[String], output_dir: Path, theories: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, progress: Progress = new Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, verbose: Boolean = false): Build.Results = { require(!selection.requirements) Isabelle_System.make_directory(output_dir) progress.echo("Building required heaps ...") val build_results0 = Build.build(options, build_heap = true, selection = selection.copy(requirements = true), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) if (build_results0.ok) { val build_options = options + "timeout_build=false" + ("mirabelle_actions=" + actions.mkString(";")) + ("mirabelle_theories=" + theories.mkString(",")) + ("mirabelle_output_dir=" + output_dir.implode) progress.echo("Running Mirabelle ...") val store = Sessions.store(build_options) def session_setup(session_name: String, session: Session): Unit = { session.all_messages += Session.Consumer[Prover.Message]("mirabelle_export") { case msg: Prover.Protocol_Output => msg.properties match { case Protocol.Export(args) if args.name.startsWith("mirabelle/") => if (verbose) { progress.echo( "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")") } val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = store.cache) val lines = Pretty.string_of(yxml).trim() val prefix = Export.explode_name(args.name) match { case List("mirabelle", action, "initialize") => action + " initialize " case List("mirabelle", action, "finalize") => action + " finalize " case List("mirabelle", action, "goal", goal_name, line, offset) => action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " + line + ":" + offset + " " case _ => "" } val body = Library.prefix_lines(prefix, lines) + "\n" val log_file = output_dir + Path.basic("mirabelle.log") File.append(log_file, body) case _ => } case _ => } } Build.build(build_options, clean_build = true, selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose, session_setup = session_setup) } else build_results0 } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", Scala_Project.here, args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var options = Options.init(opts = build_options) val mirabelle_max_calls = options.check_name("mirabelle_max_calls") + val mirabelle_randomize = options.check_name("mirabelle_randomize") val mirabelle_stride = options.check_name("mirabelle_stride") val mirabelle_timeout = options.check_name("mirabelle_timeout") val mirabelle_output_dir = options.check_name("mirabelle_output_dir") var actions: List[String] = Nil var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var output_dir = Path.explode(mirabelle_output_dir.default_value) var theories: List[String] = Nil var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var max_jobs = 1 var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] Options are: -A ACTION add to list of actions -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -O DIR """ + mirabelle_output_dir.description + " (default: " + mirabelle_output_dir.default_value + """) -T THEORY theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE] -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -m INT """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -r INT """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """) -s INT """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """) -t SECONDS """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """) -v verbose -x NAME exclude session NAME and all descendants Apply the given ACTIONs at all theories and proof steps of the specified sessions. The absence of theory restrictions (option -T) means to check all theories fully. Otherwise only the named theories are checked. Each ACTION is either of the form NAME or NAME [OPTION, ...] following Isabelle/Isar outer syntax. Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ For the ACTION "sledgehammer", the usual sledgehammer as well as the following mirabelle-specific OPTIONs are available:""" + sledgehammer_options().mkString("\n ", "\n ", "\n"), "A:" -> (arg => actions = actions ::: List(arg)), "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "O:" -> (arg => output_dir = Path.explode(arg)), "T:" -> (arg => theories = theories ::: List(arg)), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)), "o:" -> (arg => options = options + arg), + "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)), "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)), "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) if (actions.isEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo("Started at " + Build_Log.print_date(start_date)) } val results = progress.interrupt_handler { mirabelle(options, actions, output_dir.absolute, theories = theories, selection = Sessions.Selection( all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, verbose = verbose) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) } diff --git a/src/HOL/Tools/Mirabelle/mirabelle_util.ML b/src/HOL/Tools/Mirabelle/mirabelle_util.ML new file mode 100644 --- /dev/null +++ b/src/HOL/Tools/Mirabelle/mirabelle_util.ML @@ -0,0 +1,54 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_util.ML + Author: Martin Desharnais, MPI-INF Saarbruecken +*) + +(* Pseudorandom number generator *) +signature PRNG = sig + type state + val initialize : int -> state + val next : state -> int * state +end + +(* Pseudorandom algorithms *) +signature PRNG_ALGORITHMS = sig + include PRNG + val shuffle : state -> 'a list -> 'a list * state +end + +functor PRNG_Algorithms(PRNG : PRNG) : PRNG_ALGORITHMS = struct + +open PRNG + +fun shuffle prng_state xs = + fold_map (fn x => fn prng_state => + let + val (n, prng_state') = next prng_state + in ((n, x), prng_state') end) xs prng_state + |> apfst (sort (int_ord o apply2 fst)) + |> apfst (map snd) + +end + +(* multiplicative linear congruential generator *) +structure MLCG_PRNG : PRNG = struct + (* The modulus is implicitly 2^64 through using Word64. + The multiplier and increment are the same as Newlib and Musl according to Wikipedia. + See: https://en.wikipedia.org/wiki/Linear_congruential_generator#Parameters_in_common_use + *) + val multiplier = Word64.fromInt 6364136223846793005 + val increment = Word64.fromInt 1 + + type state = Word64.word + + val initialize = Word64.fromInt + + fun next s = + let + open Word64 + val s' = multiplier * s + increment + in + (toInt s', s') + end +end + +structure MLCG = PRNG_Algorithms(MLCG_PRNG) diff --git a/src/HOL/Tools/etc/options b/src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options +++ b/src/HOL/Tools/etc/options @@ -1,66 +1,69 @@ (* :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 vampire verit e spass z3 zipperposition" -- "provers for Sledgehammer (separated by blanks)" public option sledgehammer_timeout : int = 30 -- "provers will be interrupted after this time (in seconds)" 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 = false -- "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 -- "timeout in seconds for each action" option mirabelle_stride : int = 1 -- "run actions on every nth goal (0: uniform distribution)" option mirabelle_max_calls : int = 0 -- "max. no. of calls to each action (0: unbounded)" +option mirabelle_randomize : int = 0 + -- "seed to randomize the goals before selection (0: no randomization)" + option mirabelle_output_dir : string = "mirabelle" -- "output directory for log files and generated artefacts" 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)"