--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 20 11:52:45 2020 +0200
@@ -11,33 +11,30 @@
has this pattern (provided it appears in a single line):
val .*K = "PARAMETER" (*DESCRIPTION*)
*)
-(*NOTE: descriptions mention parameters (particularly NAME) without a defined range.*)
-val proverK = "prover" (*=NAME: name of the external prover to call*)
-val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
+
+val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*)
+val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*)
+val fact_filterK = "fact_filter" (*=STRING: fact filter*)
+val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*)
+val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*)
val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*)
-
-val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
-
+val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*)
+val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
+val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
+val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*)
val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
-val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
+val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*)
val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
-val isar_proofsK = "isar_proofs" (*: enable Isar proof generation*)
-val smt_proofsK = "smt_proofs" (*: enable SMT proof generation*)
-val minimizeK = "minimize" (*: instruct sledgehammer to run its minimizer*)
-
-val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*)
-val fact_filterK = "fact_filter" (*=STRING: fact filter*)
+val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*)
+val proverK = "prover" (*=STRING: name of the external prover to call*)
+val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
+val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)
+val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*)
+val strictK = "strict" (*=BOOL: run in strict mode*)
+val term_orderK = "term_order" (*=STRING: term order (in E)*)
val type_encK = "type_enc" (*=STRING: type encoding scheme*)
-val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*)
-val strictK = "strict" (*=BOOL: run in strict mode*)
-val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)
val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*)
-val e_selection_heuristicK = "e_selection_heuristic" (*: FIXME*)
-val term_orderK = "term_order" (*: FIXME*)
-val force_sosK = "force_sos" (*: use SOS*)
-val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*)
-val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "