--- a/NEWS Tue Feb 28 16:46:56 2023 +0000
+++ b/NEWS Thu Mar 02 11:34:54 2023 +0000
@@ -246,9 +246,13 @@
Minor INCOMPATIBILITY.
* Sledgehammer:
- - Added refutational mode to find likely unprovable conectures. It is
- enabled by default in addition to the usual proving mode and can be
- enabled or disabled using the 'refute' option.
+ - Added an inconsistency check mode to find likely unprovable
+ conjectures. It is enabled by default in addition to the usual
+ proving mode and can be controlled using the 'falsify' option.
+ - Added an abduction mode to find likely missing hypotheses to
+ conjectures. It currently works only with the E prover. It is
+ enabled by default and can be controlled using the 'abduce'
+ option.
*** ML ***
--- a/src/Doc/Sledgehammer/document/root.tex Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Mar 02 11:34:54 2023 +0000
@@ -100,7 +100,7 @@
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
-to find proofs but also to find inconsistencies.%
+to find proofs but also to refute the goal.%
\footnote{The distinction between ATPs and SMT solvers is mostly
historical but convenient.}
%
@@ -242,8 +242,7 @@
e: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\
z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\
-vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
-Done
+vampire: Try this: \textbf{by} \textit{simp} (0.3 ms)
\postw
Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel.
@@ -277,11 +276,17 @@
\prew
\slshape
-vampire found an inconsistency\ldots \\
-vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
-Done
+vampire found a falsification\ldots \\
+vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
\postw
+Sometimes Sledgehammer will helpfully suggest a missing assumption:
+
+\prew
+\slshape
+e: Candidate missing assumption: \\
+length ys = length xs
+\postw
\section{Hints}
\label{hints}
@@ -813,15 +818,30 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opsmart{check\_consistent}{dont\_check\_consistent}
-Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
-default, it looks for both proofs and inconsistencies.
+\opsmartx{falsify}{dont\_falsify}
+Specifies whether Sledgehammer should look for falsifications or for proofs. By
+default, it looks for both.
-An inconsistency indicates that the goal, taken as an axiom, would be
+A falsification indicates that the goal, taken as an axiom, would be
inconsistent with some specific background facts if it were added as a lemma,
indicating a likely issue with the goal. Sometimes the inconsistency involves
-only the background theory; this might happen, for example, if an axiom is used
-or if a lemma was introduced with \textbf{sorry}.
+only the background theory; this might happen, for example, if a flawed axiom is
+used or if a flawed lemma was introduced with \textbf{sorry}.
+
+\opdefault{abduce}{smart\_int}{smart}
+Specifies the maximum number of candidate missing assumptions that may be
+displayed. These hypotheses are discovered heuristically by a process called
+abduction (which stands in contrast to deduction)---that is, they are guessed
+and found to be sufficient to prove the goal.
+
+Abduction is currently supported only by E. If the option is set to
+\textit{smart} (the default), abduction is enabled only in some of the E time
+slices, and at most one candidate missing assumption is displayed. You can
+disable abduction altogether by setting the option to 0 or enable it in all
+time slices by setting it to a nonzero value.
+
+\optrueonly{dont\_abduce}
+Alias for ``\textit{abduce} = 0''.
\optrue{minimize}{dont\_minimize}
Specifies whether the proof minimization tool should be invoked automatically
@@ -1199,6 +1219,7 @@
\item[\labelitemi] \textbf{\textit{some\_preplayed}:} Sledgehammer found a proof that was successfully preplayed.
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
+\item[\labelitemi] \textbf{\textit{resources\_out}:} Sledgehammer ran out of resources.
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
problem.
\end{enum}
--- a/src/HOL/List.thy Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/List.thy Thu Mar 02 11:34:54 2023 +0000
@@ -4999,15 +4999,7 @@
lemma distinct_set_subseqs:
assumes "distinct xs"
shows "distinct (map set (subseqs xs))"
-proof (rule card_distinct)
- have "finite (set xs)" ..
- then have "card (Pow (set xs)) = 2 ^ card (set xs)"
- by (rule card_Pow)
- with assms distinct_card [of xs] have "card (Pow (set xs)) = 2 ^ length xs"
- by simp
- then show "card (set (map set (subseqs xs))) = length (map set (subseqs xs))"
- by (simp add: subseqs_powset length_subseqs)
-qed
+ by (simp add: assms card_Pow card_distinct distinct_card length_subseqs subseqs_powset)
lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
by (induct n) simp_all
@@ -5559,7 +5551,7 @@
next
case snoc
thus ?case
- by (auto simp: nth_append sorted_wrt_append)
+ by (simp add: nth_append sorted_wrt_append)
(metis less_antisym not_less nth_mem)
qed
@@ -5581,7 +5573,7 @@
by simp
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
- by(induction zs) auto
+ by auto
lemmas sorted2_simps = sorted1 sorted2
@@ -5618,9 +5610,7 @@
lemma sorted_rev_nth_mono:
"sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
- using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
- rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
- by auto
+ by (metis local.nle_le order_class.antisym_conv1 sorted_wrt_iff_nth_less sorted_wrt_rev)
lemma sorted_rev_iff_nth_mono:
"sorted (rev xs) \<longleftrightarrow> (\<forall> i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs!j \<le> xs!i)" (is "?L = ?R")
@@ -5635,7 +5625,7 @@
"length xs - Suc l \<le> length xs - Suc k" "length xs - Suc k < length xs"
using asms by auto
thus "rev xs ! k \<le> rev xs ! l"
- using \<open>?R\<close> \<open>k \<le> l\<close> unfolding rev_nth[OF \<open>k < length xs\<close>] rev_nth[OF \<open>l < length xs\<close>] by blast
+ by (simp add: \<open>?R\<close> rev_nth)
qed
thus ?L by (simp add: sorted_iff_nth_mono)
qed
@@ -5658,13 +5648,9 @@
using sorted_map_remove1 [of "\<lambda>x. x"] by simp
lemma sorted_butlast:
- assumes "xs \<noteq> []" and "sorted xs"
+ assumes "sorted xs"
shows "sorted (butlast xs)"
-proof -
- from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]"
- by (cases xs rule: rev_cases) auto
- with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
-qed
+ by (simp add: assms butlast_conv_take sorted_wrt_take)
lemma sorted_replicate [simp]: "sorted(replicate n x)"
by(induction n) (auto)
@@ -5701,28 +5687,13 @@
"sorted (map f ys)" "distinct (map f ys)"
assumes "set xs = set ys"
shows "xs = ys"
-proof -
- from assms have "map f xs = map f ys"
- by (simp add: sorted_distinct_set_unique)
- with \<open>inj_on f (set xs \<union> set ys)\<close> show "xs = ys"
- by (blast intro: map_inj_on)
-qed
-
-lemma
- assumes "sorted xs"
- shows sorted_take: "sorted (take n xs)"
- and sorted_drop: "sorted (drop n xs)"
-proof -
- from assms have "sorted (take n xs @ drop n xs)" by simp
- then show "sorted (take n xs)" and "sorted (drop n xs)"
- unfolding sorted_append by simp_all
-qed
+ using assms map_inj_on sorted_distinct_set_unique by fastforce
lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
- by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
+ by (auto dest: sorted_wrt_drop simp add: dropWhile_eq_drop)
lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
- by (subst takeWhile_eq_take) (auto dest: sorted_take)
+ by (subst takeWhile_eq_take) (auto dest: sorted_wrt_take)
lemma sorted_filter:
"sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
@@ -5745,7 +5716,7 @@
(is "filter ?P xs = ?tW")
proof (rule takeWhile_eq_filter[symmetric])
let "?dW" = "dropWhile ?P xs"
- fix x assume "x \<in> set ?dW"
+ fix x assume x: "x \<in> set ?dW"
then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
unfolding in_set_conv_nth by auto
hence "length ?tW + i < length (?tW @ ?dW)"
@@ -5759,8 +5730,7 @@
unfolding nth_append_length_plus nth_i
using i preorder_class.le_less_trans[OF le0 i] by simp
also have "... \<le> t"
- using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
- using hd_conv_nth[of "?dW"] by simp
+ by (metis hd_conv_nth hd_dropWhile length_greater_0_conv length_pos_if_in_set local.leI x)
finally show "\<not> t < f x" by simp
qed
@@ -7325,12 +7295,15 @@
lemma Cons_acc_listrel1I [intro!]:
"x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
-apply (induct arbitrary: xs set: Wellfounded.acc)
-apply (erule thin_rl)
-apply (erule acc_induct)
- apply (rule accI)
-apply (blast)
-done
+proof (induction arbitrary: xs set: Wellfounded.acc)
+ case outer: (1 u)
+ show ?case
+ proof (induct xs rule: acc_induct)
+ case 1
+ show "xs \<in> Wellfounded.acc (listrel1 r)"
+ by (simp add: outer.prems)
+ qed (metis (no_types, lifting) Cons_listrel1E2 acc.simps outer.IH)
+qed
lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
proof (induct set: lists)
@@ -7344,11 +7317,13 @@
qed
lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
-apply (induct set: Wellfounded.acc)
-apply clarify
-apply (rule accI)
-apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
-done
+proof (induction set: Wellfounded.acc)
+ case (1 x)
+ then have "\<And>u v. \<lbrakk>u \<in> set x; (v, u) \<in> r\<rbrakk> \<Longrightarrow> v \<in> Wellfounded.acc r"
+ by (metis in_lists_conv_set in_set_conv_decomp listrel1I)
+ then show ?case
+ by (meson acc.intros in_listsI)
+qed
lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
by (auto simp: wf_acc_iff
@@ -7856,11 +7831,7 @@
"all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
proof -
have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
- proof -
- fix n
- assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
- then show "P n" by (cases "n = i") simp_all
- qed
+ using le_less_Suc_eq by fastforce
show ?thesis by (auto simp add: all_interval_nat_def intro: *)
qed
@@ -7879,11 +7850,7 @@
"all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
proof -
have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
- proof -
- fix k
- assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
- then show "P k" by (cases "k = i") simp_all
- qed
+ by (smt (verit, best) atLeastAtMost_iff)
show ?thesis by (auto simp add: all_interval_int_def intro: *)
qed
@@ -8084,11 +8051,7 @@
lemma card_set [code]:
"card (set xs) = length (remdups xs)"
-proof -
- have "card (set (remdups xs)) = length (remdups xs)"
- by (rule distinct_card) simp
- then show ?thesis by simp
-qed
+ by (simp add: length_remdups_card_conv)
lemma the_elem_set [code]:
"the_elem (set [x]) = x"
@@ -8255,15 +8218,8 @@
thus "distinct_adj xs \<longleftrightarrow> distinct_adj ys"
proof (induction rule: list_all2_induct)
case (Cons x xs y ys)
- note * = this
show ?case
- proof (cases xs)
- case [simp]: (Cons x' xs')
- with * obtain y' ys' where [simp]: "ys = y' # ys'"
- by (cases ys) auto
- from * show ?thesis
- using assms by (auto simp: distinct_adj_Cons bi_unique_def)
- qed (use * in auto)
+ by (metis Cons assms bi_unique_def distinct_adj_Cons list.rel_sel)
qed auto
qed
--- a/src/HOL/TPTP/atp_theory_export.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Mar 02 11:34:54 2023 +0000
@@ -57,7 +57,7 @@
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
space_implode " " (File.bash_path (Path.explode path) ::
- arguments ctxt false "" atp_timeout prob_file)
+ arguments false false "" atp_timeout prob_file)
val outcome =
Timeout.apply atp_timeout Isabelle_System.bash_output command
|> fst
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Mar 02 11:34:54 2023 +0000
@@ -64,6 +64,7 @@
val tptp_cnf : string
val tptp_fof : string
+ val tptp_tcf : string
val tptp_tff : string
val tptp_thf : string
val tptp_has_type : string
@@ -222,6 +223,7 @@
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
+val tptp_tcf = "tcf" (* sometimes appears in E's output *)
val tptp_tff = "tff"
val tptp_thf = "thf"
val tptp_has_type = ":"
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Mar 02 11:34:54 2023 +0000
@@ -24,6 +24,7 @@
ProofMissing |
ProofIncomplete |
ProofUnparsable |
+ UnsoundProof of bool * string list |
TimedOut |
Inappropriate |
OutOfResources |
@@ -99,6 +100,8 @@
val atp_proof_of_tstplike_proof : bool -> string -> string atp_problem -> string ->
string atp_proof
+ val atp_abduce_candidates_of_output : string -> string atp_problem -> string ->
+ (string, string, (string, string atp_type) atp_term, string) atp_formula list
end;
structure ATP_Proof : ATP_PROOF =
@@ -142,6 +145,7 @@
ProofMissing |
ProofIncomplete |
ProofUnparsable |
+ UnsoundProof of bool * string list |
TimedOut |
Inappropriate |
OutOfResources |
@@ -158,12 +162,21 @@
else
""
+fun from_lemmas [] = ""
+ | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
+
fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
- | string_of_atp_failure Unprovable = "Unprovable problem"
+ | string_of_atp_failure Unprovable = "Problem unprovable"
| string_of_atp_failure GaveUp = "Gave up"
| string_of_atp_failure ProofMissing = "Proof missing"
| string_of_atp_failure ProofIncomplete = "Proof incomplete"
| string_of_atp_failure ProofUnparsable = "Proof unparsable"
+ | string_of_atp_failure (UnsoundProof (false, ss)) =
+ "Derived the lemma \"False\"" ^ from_lemmas ss ^
+ ", likely due to the use of an unsound type encoding"
+ | string_of_atp_failure (UnsoundProof (true, ss)) =
+ "Derived the lemma \"False\"" ^ from_lemmas ss ^
+ ", likely due to inconsistent axioms or \"sorry\"d lemmas"
| string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate = "Problem outside the prover's scope"
| string_of_atp_failure OutOfResources = "Out of resources"
@@ -570,7 +583,8 @@
end)
fun parse_tstp_fol_line full problem =
- ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
+ ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tcf
+ || Scan.this_string tptp_tff) -- $$ "(")
|-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
-- (if full then parse_fol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
-- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
@@ -724,4 +738,58 @@
|> parse_proof full local_prover problem
|> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))))
+val e_symbol_prefixes = ["esk", "epred"]
+
+fun exists_name_in_term pred =
+ let
+ fun ex_name (ATerm ((s, _), tms)) = pred s orelse exists ex_name tms
+ | ex_name (AAbs ((_, tm), tms)) = exists ex_name (tm :: tms)
+ in ex_name end
+
+fun exists_name_in_formula pred phi =
+ formula_fold NONE (fn _ => fn tm => fn ex => ex orelse exists_name_in_term pred tm) phi false
+
+fun exists_symbol_in_formula prefixes =
+ exists_name_in_formula (fn s => exists (fn prefix => String.isPrefix prefix s) prefixes)
+
+fun atp_abduce_candidates_of_output local_prover problem output =
+ let
+ (* Truncate too large output to avoid memory issues. *)
+ val max_size = 1000000
+ val output =
+ if String.size output > max_size then
+ String.substring (output, 0, max_size)
+ else
+ output
+
+ fun fold_extract accum [] = accum
+ | fold_extract accum (line :: lines) =
+ if String.isSubstring "# info" line
+ andalso String.isSubstring "negated_conjecture" line then
+ if String.isSubstring ", 0, 0," line then
+ (* This pattern occurs in the "info()" comment of an E clause that directly emerges from
+ the conjecture. We don't want to tell the user that they can prove "P" by assuming
+ "P". *)
+ fold_extract accum lines
+ else
+ let
+ val clean_line =
+ (case space_explode "#" line of
+ [] => ""
+ | before_hash :: _ => before_hash)
+ in
+ (case try (parse_proof true local_prover problem) clean_line of
+ SOME [(_, _, phi, _, _)] =>
+ if local_prover = eN andalso exists_symbol_in_formula e_symbol_prefixes phi then
+ fold_extract accum lines
+ else
+ fold_extract (phi :: accum) lines
+ | _ => fold_extract accum lines)
+ end
+ else
+ fold_extract accum lines
+ in
+ fold_extract [] (split_lines output)
+ end
+
end;
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Mar 02 11:34:54 2023 +0000
@@ -44,6 +44,7 @@
bool -> int Symtab.table ->
(string, string, (string, string atp_type) atp_term, string) atp_formula -> term
+ val is_conjecture_used_in_proof : string atp_proof -> bool
val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
(string * stature) list
val atp_proof_prefers_lifting : string atp_proof -> bool
@@ -58,6 +59,11 @@
val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
(term, string) atp_step list
+ val termify_atp_abduce_candidate : Proof.context -> string -> ATP_Problem.atp_format ->
+ ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
+ int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula ->
+ term
+ val top_abduce_candidates : int -> term list -> term list
end;
structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -506,6 +512,8 @@
fun is_axiom_used_in_proof pred =
exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
+val is_conjecture_used_in_proof = is_axiom_used_in_proof (is_some o resolve_conjecture)
+
fun add_fact ctxt facts ((num, ss), _, _, rule, deps) =
(if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
String.isPrefix satallax_tab_rule_prefix rule then
@@ -624,7 +632,7 @@
#> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop)
#> local_prover = waldmeisterN ? repair_waldmeister_endgame
-fun unskolemize_term skos =
+fun unskolemize_spass_term skos =
let
val is_skolem_name = member (op =) skos
@@ -653,10 +661,10 @@
val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1)
- fun unskolem t =
+ fun unskolem_inner t =
(case find_argless_skolem t of
SOME (x as (s, T)) =>
- HOLogic.exists_const T $ Abs (s, T, unskolem (safe_abstract_over (Free x, t)))
+ HOLogic.exists_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Free x, t)))
| NONE =>
(case find_skolem_arg t of
SOME (v as ((s, _), T)) =>
@@ -667,16 +675,19 @@
|> apply2 (fn lits => fold (curry s_disj) lits \<^term>\<open>False\<close>)
in
s_disj (HOLogic.all_const T
- $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
- unskolem have_nots)
+ $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, kill_skolem_arg haves))),
+ unskolem_inner have_nots)
end
| NONE =>
(case find_var t of
SOME (v as ((s, _), T)) =>
- HOLogic.all_const T $ Abs (s, T, unskolem (safe_abstract_over (Var v, t)))
+ HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, t)))
| NONE => t)))
+
+ fun unskolem_outer (@{const Trueprop} $ t) = @{const Trueprop} $ unskolem_outer t
+ | unskolem_outer t = unskolem_inner t
in
- HOLogic.mk_Trueprop o unskolem o HOLogic.dest_Trueprop
+ unskolem_outer
end
fun rename_skolem_args t =
@@ -740,7 +751,7 @@
fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps []
val deps = map (snd #> #1) skoXss_steps
in
- [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
+ [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps),
(name, Unknown, t, spass_skolemize_rule, [name0])]
end
@@ -782,4 +793,65 @@
map repair_deps atp_proof
end
+fun termify_atp_abduce_candidate ctxt local_prover format type_enc pool lifted sym_tab phi =
+ let
+ val proof = [(("", []), Conjecture, mk_anot phi, "", [])]
+ val new_proof = termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab proof
+ in
+ (case new_proof of
+ [(_, _, phi', _, _)] => phi'
+ | _ => error "Impossible case in termify_atp_abduce_candidate")
+ end
+
+fun sort_top n scored_items =
+ if n <= 0 orelse null scored_items then
+ []
+ else
+ let
+ fun split_min accum [] (_, best_item) = (best_item, List.rev accum)
+ | split_min accum ((score, item) :: scored_items) (best_score, best_item) =
+ if score < best_score then
+ split_min ((best_score, best_item) :: accum) scored_items (score, item)
+ else
+ split_min ((score, item) :: accum) scored_items (best_score, best_item)
+
+ val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items)
+ in
+ min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items)
+ |> distinct (op aconv)
+ end
+
+fun top_abduce_candidates max_candidates candidates =
+ let
+ (* We prefer free variables to other constructs, so that e.g. "x \<le> y" is
+ prioritized over "x \<le> 0". *)
+ fun score t =
+ Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0
+
+ (* Equations of the form "x = ..." or "... = x" or similar are too specific
+ to be useful. Quantified formulas are also filtered out. As for "True",
+ it may seem an odd choice for abduction, but it sometimes arises in
+ conjunction with type class constraints, which are removed by the
+ termifier. *)
+ fun maybe_score t =
+ (case t of
+ @{prop True} => NONE
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE
+ | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+ | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+ | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE
+ | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE
+ | _ => SOME (score t, t))
+ in
+ sort_top max_candidates (map_filter maybe_score candidates)
+ end
+
end;
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Mar 02 11:34:54 2023 +0000
@@ -62,8 +62,7 @@
val timestamp = timestamp_format o Time.now
(* This hash function is recommended in "Compilers: Principles, Techniques, and
- Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
- particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
+ Tools" by Aho, Sethi, and Ullman. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
@@ -416,8 +415,8 @@
val map_prod = Ctr_Sugar_Util.map_prod
-(* Compare the length of a list with an integer n while traversing at most n elements of the list.
-*)
+(* Compare the length of a list with an integer n while traversing at most n
+elements of the list. *)
fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
| compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 02 11:34:54 2023 +0000
@@ -24,7 +24,8 @@
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
| SH_Unknown
- | SH_Timeout
+ | SH_TimeOut
+ | SH_ResourcesOut
| SH_None
val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string
@@ -57,12 +58,14 @@
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
| SH_Unknown
-| SH_Timeout
+| SH_TimeOut
+| SH_ResourcesOut
| SH_None
fun short_string_of_sledgehammer_outcome (SH_Some _) = "some"
| short_string_of_sledgehammer_outcome SH_Unknown = "unknown"
- | short_string_of_sledgehammer_outcome SH_Timeout = "timeout"
+ | short_string_of_sledgehammer_outcome SH_TimeOut = "timeout"
+ | short_string_of_sledgehammer_outcome SH_ResourcesOut = "resources_out"
| short_string_of_sledgehammer_outcome SH_None = "none"
fun alternative f (SOME x) (SOME y) = SOME (f (x, y))
@@ -79,18 +82,20 @@
fun max_outcome outcomes =
let
val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
+ val timeout = find_first (fn (SH_TimeOut, _) => true | _ => false) outcomes
+ val resources_out = find_first (fn (SH_ResourcesOut, _) => true | _ => false) outcomes
val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes
- val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes
val none = find_first (fn (SH_None, _) => true | _ => false) outcomes
in
some
|> alternative snd unknown
|> alternative snd timeout
+ |> alternative snd resources_out
|> alternative snd none
|> the_default (SH_Unknown, "")
end
-fun play_one_line_proofs minimize timeout used_facts state i methss =
+fun play_one_line_proofs minimize timeout used_facts state goal i methss =
(if timeout = Time.zeroTime then
[]
else
@@ -98,7 +103,7 @@
val ctxt = Proof.context_of state
val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
val fact_names = map fst used_facts
- val {facts = chained, goal, ...} = Proof.goal state
+ val {facts = chained, ...} = Proof.goal state
val goal_t = Logic.get_goal (Thm.prop_of goal) i
fun try_methss ress [] = ress
@@ -154,20 +159,18 @@
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem)
- (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name =
+ (slice as ((slice_size, abduce, falsify, num_facts, fact_filter), _)) name =
let
val ctxt = Proof.context_of state
val _ = spying spy (fn () => (state, subgoal, name,
- "Launched" ^ (if abduce then " (abduce)" else "") ^
- (if check_consistent then " (check_consistent)" else "")))
+ "Launched" ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "")))
val _ =
if verbose then
writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
- (if abduce then " (abduce)" else "") ^
- (if check_consistent then " (check_consistent)" else "") ^ "...")
+ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "") ^ "...")
else
()
@@ -177,8 +180,7 @@
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> prefix ("Facts in " ^ name ^ " " ^
- (if check_consistent then "inconsistency" else "proof") ^ ": ")
+ |> prefix ("Facts in " ^ name ^ " " ^ (if falsify then "falsification" else "proof") ^ ": ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -206,7 +208,7 @@
|> AList.group (op =)
|> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
in
- "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^
+ "Success: Found " ^ (if falsify then "falsification" else "proof") ^ " with " ^
string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^
(if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
end
@@ -220,18 +222,20 @@
|> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
end
-fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
+fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state goal subgoal
(result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
let
val (output, chosen_preplay_outcome) =
if outcome = SOME ATP_Proof.TimedOut then
- (SH_Timeout, select_one_line_proof used_facts (fst preferred_methss) [])
+ (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) [])
+ else if outcome = SOME ATP_Proof.OutOfResources then
+ (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) [])
else if is_some outcome then
(SH_None, select_one_line_proof used_facts (fst preferred_methss) [])
else
let
val preplay_results =
- play_one_line_proofs minimize preplay_timeout used_facts state subgoal
+ play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal
(snd preferred_methss)
val chosen_preplay_outcome =
select_one_line_proof used_facts (fst preferred_methss) preplay_results
@@ -243,9 +247,11 @@
(output, output_message)
end
-fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) =
+fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) =
if outcome = SOME ATP_Proof.TimedOut then
- (SH_Timeout, K "")
+ (SH_TimeOut, K "")
+ else if outcome = SOME ATP_Proof.OutOfResources then
+ (SH_ResourcesOut, K "")
else if is_some outcome then
(SH_None, K "")
else
@@ -253,9 +259,9 @@
(if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then
(case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of
[] => "The goal is inconsistent"
- | facts => "The goal is inconsistent with these facts: " ^ commas facts)
+ | facts => "The goal is falsified by these facts: " ^ commas facts)
else
- "The following facts are inconsistent: " ^
+ "Derived \"False\" from these facts alone: " ^
commas (map fst used_facts)))
fun check_expected_outcome ctxt prover_name expect outcome =
@@ -275,14 +281,15 @@
else
error ("Unexpected outcome: the external prover found a proof but preplay failed")
| ("unknown", SH_Unknown) => ()
- | ("timeout", SH_Timeout) => ()
+ | ("timeout", SH_TimeOut) => ()
+ | ("resources_out", SH_ResourcesOut) => ()
| ("none", SH_None) => ()
| _ => error ("Unexpected outcome: " ^ quote outcome_code))
end
-fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode found_something
- writeln_result learn (problem as {state, subgoal, ...})
- (slice as ((_, _, check_consistent, _, _), _)) prover_name =
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode
+ has_already_found_something found_something writeln_result learn
+ (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name =
let
val ctxt = Proof.context_of state
val hard_timeout = Time.scale 5.0 timeout
@@ -306,15 +313,16 @@
in
{comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1,
subgoal_count = 1, factss = map (apsnd (append new_facts)) factss,
+ has_already_found_something = has_already_found_something,
found_something = found_something "an inconsistency"}
end
- val problem = problem |> check_consistent ? flip_problem
+ val problem as {goal, ...} = problem |> falsify ? flip_problem
fun really_go () =
launch_prover params mode learn problem slice prover_name
- |> (if check_consistent then analyze_prover_result_for_consistency else
- preplay_prover_result params state subgoal)
+ |> (if falsify then analyze_prover_result_for_inconsistency else
+ preplay_prover_result params state goal subgoal)
fun go () =
if debug then
@@ -322,10 +330,10 @@
else
(really_go ()
handle
- ERROR msg => (SH_Unknown, fn () => "Warning: " ^ msg ^ "\n")
+ ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
| exn =>
if Exn.is_interrupt exn then Exn.reraise exn
- else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+ else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
val (outcome, message) = Timeout.apply hard_timeout go ()
val () = check_expected_outcome ctxt prover_name expect outcome
@@ -354,11 +362,10 @@
val default_slice_schedule =
(* FUDGE (loosely inspired by Seventeen evaluation) *)
- [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N,
- zipperpositionN, cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN,
- cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN,
- vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN,
- zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N,
+ [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN,
+ cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN,
+ spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN,
+ iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N,
zipperpositionN]
fun schedule_of_provers provers num_slices =
@@ -380,16 +387,16 @@
@ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
end
-fun prover_slices_of_schedule ctxt factss
- ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
+fun prover_slices_of_schedule ctxt goal subgoal factss
+ ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
...} : params)
schedule =
let
fun triplicate_slices original =
let
val shift =
- map (apfst (fn (slice_size, abduce, check_consistent, num_facts, fact_filter) =>
- (slice_size, abduce, check_consistent, num_facts,
+ map (apfst (fn (slice_size, abduce, falsify, num_facts, fact_filter) =>
+ (slice_size, abduce, falsify, num_facts,
if fact_filter = mashN then mepoN
else if fact_filter = mepoN then meshN
else mashN)))
@@ -407,16 +414,23 @@
| adjust_extra (extra as SMT_Slice _) = extra
fun adjust_slice max_slice_size
- ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) =
+ ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =
let
val slice_size = Int.min (max_slice_size, slice_size0)
- val abduce = abduce |> the_default abduce0
- val check_consistent = check_consistent |> the_default check_consistent0
+ val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False})
+ val abduce =
+ (case abduce of
+ NONE => abduce0 andalso goal_not_False
+ | SOME max_candidates => max_candidates > 0)
+ val falsify =
+ (case falsify of
+ NONE => falsify0 andalso goal_not_False
+ | SOME falsify => falsify)
val fact_filter = fact_filter |> the_default fact_filter0
val max_facts = max_facts |> the_default num_facts0
val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
in
- ((slice_size, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra)
+ ((slice_size, abduce, falsify, num_facts, fact_filter), adjust_extra extra)
end
val provers = distinct (op =) schedule
@@ -445,9 +459,8 @@
|> distinct (op =)
end
-fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules,
- max_facts, max_proofs, slices, ...})
- mode writeln_result i (fact_override as {only, ...}) state =
+fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
+ max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
if null provers then
error "No prover is set"
else
@@ -458,11 +471,17 @@
val _ = Proof.assert_backward state
val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
- val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0
+ val found_proofs_and_falsifications = Synchronized.var "found_proofs_and_falsifications" 0
+
+ fun has_already_found_something () =
+ if mode = Normal then
+ Synchronized.value found_proofs_and_falsifications > 0
+ else
+ false
fun found_something a_proof_or_inconsistency prover_name =
if mode = Normal then
- (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1);
+ (Synchronized.change found_proofs_and_falsifications (fn n => n + 1);
(the_default writeln writeln_result) (prover_name ^ " found " ^
a_proof_or_inconsistency ^ "..."))
else
@@ -521,14 +540,16 @@
val factss = get_factss provers
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = factss, found_something = found_something "a proof"}
+ factss = factss, has_already_found_something = has_already_found_something,
+ found_something = found_something "a proof"}
val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
- val launch = launch_prover_and_preplay params mode found_something writeln_result learn
+ val launch = launch_prover_and_preplay params mode has_already_found_something
+ found_something writeln_result learn
val schedule =
if mode = Auto_Try then provers
else schedule_of_provers provers slices
- val prover_slices = prover_slices_of_schedule ctxt factss params schedule
+ val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule
val _ =
if verbose then
@@ -545,32 +566,33 @@
else
(learn chained_thms;
Par_List.map (fn (prover, slice) =>
- if Synchronized.value found_proofs_and_inconsistencies < max_proofs then
+ if Synchronized.value found_proofs_and_falsifications < max_proofs then
launch problem slice prover
else
(SH_None, ""))
prover_slices
|> max_outcome)
end
+
+ fun normal_failure () =
+ (the_default writeln writeln_result
+ ("No " ^ (if falsify = SOME true then "falsification" else "proof") ^
+ " found");
+ false)
in
(launch_provers ()
- handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
+ handle Timeout.TIMEOUT _ => (SH_TimeOut, ""))
|> `(fn (outcome, message) =>
(case outcome of
SH_Some _ => (the_default writeln writeln_result "Done"; true)
- | SH_Unknown => (the_default writeln writeln_result message; false)
- | SH_Timeout =>
- (the_default writeln writeln_result
- ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
- " found");
- false)
- | SH_None => (the_default writeln writeln_result
- (if message = "" then
- "No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
- " found"
- else
- "Warning: " ^ message);
- false)))
+ | SH_Unknown =>
+ if message = "" then normal_failure ()
+ else (the_default writeln writeln_result ("Warning: " ^ message); false)
+ | SH_TimeOut => normal_failure ()
+ | SH_ResourcesOut => normal_failure ()
+ | SH_None =>
+ if message = "" then normal_failure ()
+ else (the_default writeln writeln_result ("Warning: " ^ message); false)))
end)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 02 11:34:54 2023 +0000
@@ -15,7 +15,7 @@
type atp_slice = atp_format * string * string * bool * string
type atp_config =
{exec : string list * string list,
- arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list,
+ arguments : bool -> bool -> string -> Time.time -> Path.T -> string list,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -67,7 +67,7 @@
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
-(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *)
+(* desired slice size, abduce, falsify, desired number of facts, fact filter *)
type base_slice = int * bool * bool * int * string
(* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
@@ -76,7 +76,7 @@
type atp_config =
{exec : string list * string list,
- arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list,
+ arguments : bool -> bool -> string -> Time.time -> Path.T -> string list,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -176,10 +176,13 @@
val e_config : atp_config =
{exec = (["E_HOME"], ["eprover-ho", "eprover"]),
- arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
- ["--tstp-in --tstp-out --silent " ^ extra_options ^
- " --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^
- File.bash_path problem],
+ arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem =>
+ ["--tstp-in --tstp-out --silent " ^
+ (if abduce then
+ "--auto --print-saturated=ieIE --print-sat-info --soft-cpu-limit="
+ else
+ extra_options ^ " --cpu-limit=") ^
+ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem],
proof_delims =
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
tstp_proof_delims,
@@ -192,8 +195,9 @@
good_slices =
let
val (format, type_enc, lam_trans, extra_options) =
- if string_ord (getenv "E_VERSION", "2.7") <> LESS then
- (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
+ if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+ (* '$ite' support appears to be unsound. *)
+ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
else
@@ -201,11 +205,11 @@
in
(* FUDGE *)
K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, false, 128, mepoN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options)),
- ((1000 (* infinity *), false, false, 64, mashN), (format, type_enc, combsN, false, extra_options))]
+ ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
end,
good_max_mono_iters = default_max_mono_iters,
good_max_new_mono_instances = default_max_new_mono_instances}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 02 11:34:54 2023 +0000
@@ -54,7 +54,7 @@
("overlord", "false"),
("spy", "false"),
("abduce", "smart"),
- ("check_consistent", "smart"),
+ ("falsify", "smart"),
("type_enc", "smart"),
("strict", "false"),
("lam_trans", "smart"),
@@ -77,6 +77,7 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
+ ("dont_abduce", ("abduce", ["0"])),
("dont_preplay", ("preplay_timeout", ["0"])),
("dont_compress", ("compress", ["1"])),
("dont_slice", ("slices", ["1"])),
@@ -86,8 +87,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_spy", "spy"),
- ("dont_abduce", "abduce"),
- ("dont_check_consistent", "check_consistent"),
+ ("dont_falsify", "falsify"),
("non_strict", "strict"),
("no_uncurried_aliases", "uncurried_aliases"),
("dont_learn", "learn"),
@@ -232,16 +232,12 @@
val overlord = lookup_bool "overlord"
val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
- val check_consistent =
- if mode = Auto_Try then
- SOME false
- else
- lookup_option lookup_bool "check_consistent"
val abduce =
- if mode = Auto_Try then
- SOME false
- else
- lookup_option lookup_bool "abduce"
+ if mode = Auto_Try then SOME 0
+ else lookup_option lookup_int "abduce"
+ val falsify =
+ if mode = Auto_Try then SOME false
+ else lookup_option lookup_bool "falsify"
val type_enc =
if mode = Auto_Try then
NONE
@@ -275,7 +271,7 @@
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict,
+ abduce = abduce, falsify = falsify, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 02 11:34:54 2023 +0000
@@ -21,6 +21,7 @@
val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
one_line_params -> string
+ val abduce_text : Proof.context -> term list -> string
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -528,4 +529,8 @@
else
one_line_proof_text ctxt num_chained) one_line_params
+fun abduce_text ctxt tms =
+ "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^
+ cat_lines (map (Syntax.string_of_term ctxt) tms)
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 02 11:34:54 2023 +0000
@@ -868,7 +868,8 @@
let
val problem =
{comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
- subgoal_count = 1, factss = [("", facts)], found_something = K ()}
+ subgoal_count = 1, factss = [("", facts)], has_already_found_something = K false,
+ found_something = K ()}
val slice = hd (get_slices ctxt prover)
in
get_minimizing_prover ctxt MaSh (K ()) prover params problem slice
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 02 11:34:54 2023 +0000
@@ -29,8 +29,8 @@
overlord : bool,
spy : bool,
provers : string list,
- abduce : bool option,
- check_consistent : bool option,
+ abduce : int option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
@@ -63,6 +63,7 @@
subgoal : int,
subgoal_count : int,
factss : (string * fact list) list,
+ has_already_found_something : unit -> bool,
found_something : string -> unit}
datatype prover_slice_extra =
@@ -82,6 +83,7 @@
type prover = params -> prover_problem -> prover_slice -> prover_result
val SledgehammerN : string
+ val default_abduce_max_candidates : int
val str_of_mode : mode -> string
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
@@ -113,6 +115,8 @@
(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
val SledgehammerN = "Sledgehammer"
+val default_abduce_max_candidates = 1
+
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
fun str_of_mode Auto_Try = "Auto Try"
@@ -136,8 +140,8 @@
overlord : bool,
spy : bool,
provers : string list,
- abduce : bool option,
- check_consistent : bool option,
+ abduce : int option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
@@ -182,6 +186,7 @@
subgoal : int,
subgoal_count : int,
factss : (string * fact list) list,
+ has_already_found_something : unit -> bool,
found_something : string -> unit}
datatype prover_slice_extra =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Mar 02 11:34:54 2023 +0000
@@ -99,15 +99,17 @@
| suffix_of_mode Minimize = "_min"
(* Important messages are important but not so important that users want to see them each time. *)
-val atp_important_message_keep_quotient = 25
+val important_message_keep_quotient = 25
fun run_atp mode name
- ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs,
- compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params)
- ({comment, state, goal, subgoal, subgoal_count, factss, found_something} : prover_problem)
+ ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters,
+ max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout,
+ preplay_timeout, spy, ...} : params)
+ ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something,
+ found_something} : prover_problem)
slice =
let
- val (basic_slice as (slice_size, _, _, _, _),
+ val (basic_slice as (slice_size, abduce, _, _, _),
ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) =
slice
val facts = facts_of_basic_slice basic_slice factss
@@ -185,11 +187,12 @@
val strictness = if strict then Strict else Non_Strict
val type_enc = choose_type_enc strictness good_format good_type_enc
val run_timeout = slice_timeout slice_size slices timeout
- val generous_run_timeout = if mode = MaSh then one_day else run_timeout
+ val generous_run_timeout =
+ if mode = MaSh then one_day
+ else if abduce then run_timeout + seconds 5.0
+ else run_timeout
val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () =>
- let
- val readable_names = not (Config.get ctxt atp_full_names)
- in
+ let val readable_names = not (Config.get ctxt atp_full_names) in
facts
|> not (is_type_enc_sound type_enc) ?
filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
@@ -203,7 +206,7 @@
(state, subgoal, name, "Generating ATP problem in " ^
string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
- val args = arguments ctxt full_proofs extra run_timeout prob_path
+ val args = arguments abduce full_proofs extra run_timeout prob_path
val command = space_implode " " (File.bash_path executable :: args)
fun run_command () =
@@ -220,6 +223,8 @@
cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
|> File.write_list prob_path
+ val local_name = name |> perhaps (try (unprefix remote_prefix))
+
val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) =
Timeout.apply generous_run_timeout run_command ()
|>> overlord ?
@@ -227,30 +232,36 @@
|> (fn accum as (output, _) =>
(accum,
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> `(atp_proof_of_tstplike_proof false (perhaps (try (unprefix remote_prefix)) name)
- atp_problem)
+ |>> `(atp_proof_of_tstplike_proof false local_name atp_problem)
handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable)))
handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut))
| ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg)))
+ val atp_abduce_candidates =
+ if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then
+ atp_abduce_candidates_of_output local_name atp_problem output
+ else
+ []
+
val () = spying spy (fn () =>
(state, subgoal, name, "Running command in " ^
string_of_int (Time.toMilliseconds run_time) ^ " ms"))
- val _ =
+ val outcome =
(case outcome of
- NONE => found_something name
- | _ => ())
+ NONE => (found_something name; NONE)
+ | _ => outcome)
in
(atp_problem_data,
- (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome),
+ (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates,
+ outcome),
(good_format, type_enc))
end
- (* If the problem file has not been exported, remove it; otherwise, export
- the proof file too. *)
+ (* If the problem file has not been exported, remove it; otherwise, export the proof file
+ too. *)
fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else ()
- fun export (_, (output, _, _, _, _, _, _), _) =
+ fun export (_, (output, _, _, _, _, _, _, _), _) =
let
val proof_dest_dir_path = Path.explode proof_dest_dir
val make_export_file_name =
@@ -259,7 +270,8 @@
#> swap
#> uncurry Path.ext
in
- if proof_dest_dir = "" then Output.system_message "don't export proof"
+ if proof_dest_dir = "" then
+ Output.system_message "don't export proof"
else if File.exists proof_dest_dir_path then
File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output
else
@@ -267,20 +279,28 @@
end
val ((_, pool, lifted, sym_tab),
- (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, outcome),
+ (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
+ atp_abduce_candidates, outcome),
(format, type_enc)) =
with_cleanup clean_up run () |> tap export
val important_message =
- if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
+ if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0
then extract_important_message output
else ""
- val (used_facts, preferred_methss, message) =
+ val (outcome, used_facts, preferred_methss, message) =
(case outcome of
NONE =>
let
val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
+ val _ =
+ if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof)
+ andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then
+ warning ("Derived \"False\" from these facts alone: " ^ commas (map fst used_facts))
+ else
+ ()
+
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val preferred = Metis_Method (NONE, NONE)
val preferred_methss =
@@ -291,7 +311,7 @@
else
[[preferred]])
in
- (used_facts, preferred_methss,
+ (NONE, used_facts, preferred_methss,
fn preplay =>
let
val _ = if verbose then writeln "Generating proof text..." else ()
@@ -330,7 +350,19 @@
end)
end
| SOME failure =>
- ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
+ let
+ val max_abduce_candidates =
+ the_default default_abduce_max_candidates abduce_max_candidates
+ val abduce_candidates = atp_abduce_candidates
+ |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab)
+ |> top_abduce_candidates max_abduce_candidates
+ in
+ if null abduce_candidates then
+ (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)
+ else
+ (NONE, [], (Auto_Method (* dummy *), []), fn _ =>
+ abduce_text ctxt abduce_candidates)
+ end)
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,
preferred_methss = preferred_methss, run_time = run_time, message = message}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Mar 02 11:34:54 2023 +0000
@@ -83,8 +83,8 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
minimize, preplay_timeout, induction_rules, ...} : params)
- (slice as ((_, abduce, check_consistent, _, _), _)) silent (prover : prover) timeout i n state
- goal facts =
+ (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
+ state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -92,8 +92,8 @@
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- type_enc = type_enc, abduce = SOME abduce, check_consistent = SOME check_consistent,
- strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
+ type_enc = type_enc, abduce = SOME 0, falsify = SOME false, strict = strict,
+ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
@@ -102,10 +102,10 @@
expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)], found_something = K ()}
+ factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
message} =
- prover params problem slice
+ prover params problem ((1, false, false, length facts, fact_filter), slice_extra)
val result as {outcome, ...} =
if is_none outcome0 andalso
forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
@@ -118,14 +118,12 @@
(case outcome of
SOME failure => string_of_atp_failure failure
| NONE =>
- "Found " ^ (if check_consistent then "inconsistency" else "proof") ^
+ "Found " ^ (if falsify then "falsification" else "proof") ^
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
" (" ^ string_of_time run_time ^ ")"));
result
end
-(* minimalization of facts *)
-
(* Give the external prover some slack. The ATP gets further slack because the
Sledgehammer preprocessing time is included in the estimate below but isn't
part of the timeout. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Tue Feb 28 16:46:56 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Thu Mar 02 11:34:54 2023 +0000
@@ -45,7 +45,7 @@
|> hd |> snd
val problem =
{comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)], found_something = K ()}
+ factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
val slice = hd (get_slices ctxt name)
in
(case prover params problem slice of
--- a/src/Pure/Concurrent/future.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/Concurrent/future.scala Thu Mar 02 11:34:54 2023 +0000
@@ -139,7 +139,8 @@
daemon: Boolean,
inherit_locals: Boolean,
uninterruptible: Boolean,
- body: => A) extends Future[A] {
+ body: => A
+) extends Future[A] {
private val result = Future.promise[A]
private val thread =
Isabelle_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
--- a/src/Pure/Concurrent/isabelle_thread.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.scala Thu Mar 02 11:34:54 2023 +0000
@@ -124,9 +124,14 @@
else body
}
-class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup,
- pri: Int, daemon: Boolean, inherit_locals: Boolean)
- extends Thread(group, null, name, 0L, inherit_locals) {
+class Isabelle_Thread private(
+ main: Runnable,
+ name: String,
+ group: ThreadGroup,
+ pri: Int,
+ daemon: Boolean,
+ inherit_locals: Boolean
+) extends Thread(group, null, name, 0L, inherit_locals) {
thread =>
thread.setPriority(pri)
--- a/src/Pure/ML/ml_console.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/ML/ml_console.scala Thu Mar 02 11:34:54 2023 +0000
@@ -71,12 +71,14 @@
options, logic, dirs = dirs, include_sessions = include_sessions).check_errors
}
+ val session_heaps =
+ if (raw_ml_system) Nil
+ else ML_Process.session_heaps(store, session_background, logic = logic)
+
// process loop
val process =
- ML_Process(store, options, session_background,
- logic = logic, args = List("-i"), redirect = true,
- modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
- raw_ml_system = raw_ml_system)
+ ML_Process(options, session_background, session_heaps, args = List("-i"), redirect = true,
+ modes = if (raw_ml_system) Nil else modes ::: List("ASCII"))
POSIX_Interrupt.handler { process.interrupt() } {
new TTY_Loop(process.stdin, process.stdout).join()
--- a/src/Pure/ML/ml_process.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/ML/ml_process.scala Thu Mar 02 11:34:54 2023 +0000
@@ -12,12 +12,22 @@
object ML_Process {
+ def session_heaps(
+ store: Sessions.Store,
+ session_background: Sessions.Background,
+ logic: String = ""
+ ): List[Path] = {
+ val logic_name = Isabelle_System.default_logic(logic)
+
+ session_background.sessions_structure.selection(logic_name).
+ build_requirements(List(logic_name)).
+ map(store.the_heap)
+ }
+
def apply(
- store: Sessions.Store,
options: Options,
session_background: Sessions.Background,
- logic: String = "",
- raw_ml_system: Boolean = false,
+ session_heaps: List[Path],
use_prelude: List[String] = Nil,
eval_main: String = "",
args: List[String] = Nil,
@@ -27,18 +37,8 @@
redirect: Boolean = false,
cleanup: () => Unit = () => ()
): Bash.Process = {
- val logic_name = Isabelle_System.default_logic(logic)
-
- val heaps: List[String] =
- if (raw_ml_system) Nil
- else {
- session_background.sessions_structure.selection(logic_name).
- build_requirements(List(logic_name)).
- map(a => File.platform_path(store.the_heap(a)))
- }
-
val eval_init =
- if (heaps.isEmpty) {
+ if (session_heaps.isEmpty) {
List(
"""
fun chapter (_: string) = ();
@@ -58,13 +58,13 @@
"PolyML.Compiler.prompt1 := \"Poly/ML> \"",
"PolyML.Compiler.prompt2 := \"Poly/ML# \"")
}
- else
+ else {
List(
"(PolyML.SaveState.loadHierarchy " +
- ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
- "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
- ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
- "); OS.Process.exit OS.Process.failure)")
+ ML_Syntax.print_list(
+ ML_Syntax.print_string_bytes)(session_heaps.map(File.platform_path)) +
+ "; PolyML.print_depth 0)")
+ }
val eval_modes =
if (modes.isEmpty) Nil
@@ -72,13 +72,13 @@
// options
- val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
+ val eval_options = if (session_heaps.isEmpty) Nil else List("Options.load_default ()")
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
// session resources
- val eval_init_session = if (raw_ml_system) Nil else List("Resources.init_session_env ()")
+ val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()")
val init_session = Isabelle_System.tmp_file("init_session")
Isabelle_System.chmod("600", File.path(init_session))
File.write(init_session, new Resources(session_background).init_session_yxml)
@@ -86,7 +86,7 @@
// process
val eval_process =
proper_string(eval_main).getOrElse(
- if (heaps.isEmpty) {
+ if (session_heaps.isEmpty) {
"PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
}
else "Isabelle_Process.init ()")
@@ -171,9 +171,10 @@
val store = Sessions.store(options)
val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
+ val session_heaps = ML_Process.session_heaps(store, session_background, logic = logic)
val result =
- ML_Process(store, options, session_background,
- logic = logic, args = eval_args, modes = modes).result(
+ ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes)
+ .result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))
--- a/src/Pure/PIDE/headless.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/PIDE/headless.scala Thu Mar 02 11:34:54 2023 +0000
@@ -619,10 +619,11 @@
): Session = {
val session_name = session_background.session_name
val session = new Session(session_name, options, resources)
+ val session_heaps = ML_Process.session_heaps(store, session_background, logic = session_name)
progress.echo("Starting session " + session_name + " ...")
- Isabelle_Process.start(store, options, session, session_background,
- logic = session_name, modes = print_mode).await_startup()
+ Isabelle_Process.start(
+ options, session, session_background, session_heaps, modes = print_mode).await_startup()
session
}
--- a/src/Pure/System/isabelle_process.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/System/isabelle_process.scala Thu Mar 02 11:34:54 2023 +0000
@@ -13,12 +13,10 @@
object Isabelle_Process {
def start(
- store: Sessions.Store,
options: Options,
session: Session,
session_background: Sessions.Background,
- logic: String = "",
- raw_ml_system: Boolean = false,
+ session_heaps: List[Path],
use_prelude: List[String] = Nil,
eval_main: String = "",
modes: List[String] = Nil,
@@ -32,8 +30,7 @@
options.
string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(store, ml_options, session_background,
- logic = logic, raw_ml_system = raw_ml_system,
+ ML_Process(ml_options, session_background, session_heaps,
use_prelude = use_prelude, eval_main = eval_main,
modes = modes, cwd = cwd, env = env)
}
--- a/src/Pure/Tools/build.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/Tools/build.scala Thu Mar 02 11:34:54 2023 +0000
@@ -44,16 +44,13 @@
/* engine */
- abstract class Engine(val name: String) extends Isabelle_System.Service {
+ class Engine(val name: String) extends Isabelle_System.Service {
override def toString: String = name
- def init(build_context: Build_Process.Context): Build_Process
+ def init(build_context: Build_Process.Context): Build_Process =
+ new Build_Process(build_context)
}
- class Default_Engine extends Engine("") {
- override def toString: String = "<default>"
- override def init(build_context: Build_Process.Context): Build_Process =
- new Build_Process(build_context)
- }
+ class Default_Engine extends Engine("") { override def toString: String = "<default>" }
lazy val engines: List[Engine] =
Isabelle_System.make_services(classOf[Engine])
--- a/src/Pure/Tools/build_job.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/Tools/build_job.scala Thu Mar 02 11:34:54 2023 +0000
@@ -43,6 +43,7 @@
progress: Progress,
verbose: Boolean,
session_background: Sessions.Background,
+ session_heaps: List[Path],
store: Sessions.Store,
do_store: Boolean,
resources: Resources,
@@ -62,17 +63,11 @@
private lazy val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
- Exn.Interrupt.expose()
-
- val parent = info.parent.getOrElse("")
-
val env =
Isabelle_System.settings(
List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
- val is_pure = Sessions.is_pure(session_name)
-
- val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
+ val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
val eval_store =
if (do_store) {
@@ -270,13 +265,10 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
- val process =
- Isabelle_Thread.uninterruptible {
- Isabelle_Process.start(store, options, session, session_background,
- logic = parent, raw_ml_system = is_pure,
- use_prelude = use_prelude, eval_main = eval_main,
- cwd = info.dir.file, env = env)
- }
+ val process = {
+ Isabelle_Process.start(options, session, session_background, session_heaps,
+ use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env)
+ }
val build_errors =
Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
--- a/src/Pure/Tools/build_process.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Pure/Tools/build_process.scala Thu Mar 02 11:34:54 2023 +0000
@@ -249,7 +249,7 @@
if_proper(names, Generic.name.member(names)))
}
- object Config {
+ object Base {
val instance = Generic.instance.make_primary_key
val ml_platform = SQL.Column.string("ml_platform")
val options = SQL.Column.string("options")
@@ -257,12 +257,17 @@
val table = make_table("", List(instance, ml_platform, options))
}
- object State {
- val instance = Generic.instance.make_primary_key
+ object Serial {
val serial = SQL.Column.long("serial")
+
+ val table = make_table("serial", List(serial))
+ }
+
+ object Node_Info {
+ val hostname = SQL.Column.string("hostname").make_primary_key
val numa_index = SQL.Column.int("numa_index")
- val table = make_table("state", List(instance, serial, numa_index))
+ val table = make_table("node_info", List(hostname, numa_index))
}
object Pending {
@@ -297,6 +302,39 @@
List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
}
+ def get_serial(db: SQL.Database): Long =
+ db.using_statement(Serial.table.select())(stmt =>
+ stmt.execute_query().iterator(_.long(Serial.serial)).nextOption.getOrElse(0L))
+
+ def set_serial(db: SQL.Database, serial: Long): Unit =
+ if (get_serial(db) != serial) {
+ db.using_statement(Serial.table.delete())(_.execute())
+ db.using_statement(Serial.table.insert()) { stmt =>
+ stmt.long(1) = serial
+ stmt.execute()
+ }
+ }
+
+ def read_numa_index(db: SQL.Database, hostname: String): Int =
+ db.using_statement(
+ Node_Info.table.select(List(Node_Info.numa_index),
+ sql = Node_Info.hostname.where_equal(hostname))
+ )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_index)).nextOption.getOrElse(0))
+
+ def update_numa_index(db: SQL.Database, hostname: String, numa_index: Int): Boolean =
+ if (read_numa_index(db, hostname) != numa_index) {
+ db.using_statement(
+ Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))
+ )(_.execute())
+ db.using_statement(Node_Info.table.insert()) { stmt =>
+ stmt.string(1) = hostname
+ stmt.int(2) = numa_index
+ stmt.execute()
+ }
+ true
+ }
+ else false
+
def read_pending(db: SQL.Database): List[Entry] =
db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt =>
List.from(
@@ -417,40 +455,15 @@
insert.nonEmpty
}
- def write_config(db: SQL.Database, instance: String, hostname: String, options: Options): Unit =
- db.using_statement(Config.table.insert()) { stmt =>
- stmt.string(1) = instance
- stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM")
- stmt.string(3) = options.make_prefs(Options.init(prefs = ""))
- stmt.execute()
- }
-
- def read_state(db: SQL.Database, instance: String): (Long, Int) =
- db.using_statement(
- State.table.select(sql = SQL.where(Generic.sql_equal(instance = instance)))
- ) { stmt =>
- (stmt.execute_query().iterator { res =>
- val serial = res.long(State.serial)
- val numa_index = res.int(State.numa_index)
- (serial, numa_index)
- }).nextOption.getOrElse(error("No build state instance " + instance + " in database " + db))
- }
-
- def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit =
- db.using_statement(State.table.insert()) { stmt =>
- stmt.string(1) = instance
- stmt.long(2) = serial
- stmt.int(3) = numa_index
- stmt.execute()
- }
-
- def reset_state(db: SQL.Database, instance: String): Unit =
- db.using_statement(
- State.table.delete(sql = SQL.where(Generic.sql_equal(instance = instance))))(_.execute())
-
def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
val tables =
- List(Config.table, State.table, Pending.table, Running.table, Results.table)
+ List(
+ Base.table,
+ Serial.table,
+ Node_Info.table,
+ Pending.table,
+ Running.table,
+ Results.table)
for (table <- tables) db.create_table(table)
@@ -462,22 +475,31 @@
for (table <- tables) db.using_statement(table.delete())(_.execute())
- write_config(db, build_context.instance, build_context.hostname, build_context.store.options)
- write_state(db, build_context.instance, 0, 0)
+ db.using_statement(Base.table.insert()) { stmt =>
+ stmt.string(1) = build_context.instance
+ stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM")
+ stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = ""))
+ stmt.execute()
+ }
}
- def update_database(db: SQL.Database, instance: String, state: State): State = {
- val ch1 = update_pending(db, state.pending)
- val ch2 = update_running(db, state.running)
- val ch3 = update_results(db, state.results)
+ def update_database(
+ db: SQL.Database,
+ instance: String,
+ hostname: String,
+ state: State
+ ): State = {
+ val changed =
+ List(
+ update_numa_index(db, hostname, state.numa_index),
+ update_pending(db, state.pending),
+ update_running(db, state.running),
+ update_results(db, state.results))
- val (serial0, _) = read_state(db, instance)
- val serial = if (ch1 || ch2 || ch3) serial0 + 1 else serial0
- if (serial != serial0) {
- reset_state(db, instance)
- write_state(db, instance, serial, state.numa_index)
- }
+ val serial0 = get_serial(db)
+ val serial = if (changed.exists(identity)) serial0 + 1 else serial0
+ set_serial(db, serial)
state.copy(serial = serial)
}
}
@@ -513,12 +535,18 @@
def close(): Unit = database.foreach(_.close())
// global state
- protected var _state: Build_Process.State = init_state()
+ protected var _state: Build_Process.State = init_state(Build_Process.State())
- protected def init_state(): Build_Process.State =
- Build_Process.State(pending =
- (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
- yield Build_Process.Entry(name, preds.toList)).toList)
+ protected def init_state(state: Build_Process.State): Build_Process.State = {
+ val old_pending = state.pending.iterator.map(_.name).toSet
+ val new_pending =
+ List.from(
+ for {
+ (name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator
+ if !old_pending(name)
+ } yield Build_Process.Entry(name, preds.toList))
+ state.copy(pending = new_pending ::: state.pending)
+ }
protected def next_pending(): Option[String] = synchronized {
if (_state.running.size < (build_context.max_jobs max 1)) {
@@ -586,6 +614,12 @@
store.init_session_info(_, session_name))
val session_background = build_deps.background(session_name)
+ val session_heaps =
+ session_background.info.parent match {
+ case None => Nil
+ case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
+ }
+
val resources =
new Resources(session_background, log = log,
command_timings = build_context(session_name).old_command_timings)
@@ -595,9 +629,9 @@
val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
- new Build_Job.Build_Session(progress, verbose, session_background, store, do_store,
- resources, build_context.session_setup, build_deps.sources_shasum(session_name),
- input_heaps, node_info)
+ new Build_Job.Build_Session(progress, verbose, session_background, session_heaps,
+ store, do_store, resources, build_context.session_setup,
+ build_deps.sources_shasum(session_name), input_heaps, node_info)
_state = state1.add_running(session_name, job)
job
}
@@ -626,7 +660,9 @@
for (db <- database) {
synchronized {
db.transaction {
- _state = Build_Process.Data.update_database(db, build_context.instance, _state)
+ _state =
+ Build_Process.Data.update_database(
+ db, build_context.instance, build_context.hostname, _state)
}
}
}
--- a/src/Tools/VSCode/src/language_server.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Tools/VSCode/src/language_server.scala Thu Mar 02 11:34:54 2023 +0000
@@ -297,6 +297,8 @@
for ((session_background, session) <- try_session) {
val store = Sessions.store(options)
+ val session_heaps =
+ ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
session_.change(_ => Some(session))
@@ -306,8 +308,8 @@
dynamic_output.init()
try {
- Isabelle_Process.start(store, options, session, session_background,
- modes = modes, logic = session_background.session_name).await_startup()
+ Isabelle_Process.start(
+ options, session, session_background, session_heaps, modes = modes).await_startup()
reply_ok(
"Welcome to Isabelle/" + session_background.session_name +
Isabelle_System.isabelle_heading())
--- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Feb 28 16:46:56 2023 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 02 11:34:54 2023 +0000
@@ -162,11 +162,12 @@
val session = PIDE.session
val session_background = PIDE.resources.session_background
val store = sessions_store(options = options)
+ val session_heaps =
+ ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
session.phase_changed += PIDE.plugin.session_phase_changed
- Isabelle_Process.start(store, store.options, session, session_background,
- logic = session_background.session_name,
+ Isabelle_Process.start(store.options, session, session_background, session_heaps,
modes =
(space_explode(',', store.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)