# HG changeset patch # User paulson # Date 1677756894 0 # Node ID df1150ec6cd770e94ae05a9e74e4bb8597631e0c # Parent 5b3139a6b0de674135326ceb6ebcffa1122f5560# Parent da41823d09a7aba054d6bcd5fc7e6730dde47f00 merged diff -r da41823d09a7 -r df1150ec6cd7 NEWS --- 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 *** diff -r da41823d09a7 -r df1150ec6cd7 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/List.thy --- 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 \ y \ 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) \ i \ j \ j < length xs \ xs!j \ 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) \ (\ i j. i \ j \ j < length xs \ xs!j \ xs!i)" (is "?L = ?R") @@ -5635,7 +5625,7 @@ "length xs - Suc l \ length xs - Suc k" "length xs - Suc k < length xs" using asms by auto thus "rev xs ! k \ rev xs ! l" - using \?R\ \k \ l\ unfolding rev_nth[OF \k < length xs\] rev_nth[OF \l < length xs\] by blast + by (simp add: \?R\ rev_nth) qed thus ?L by (simp add: sorted_iff_nth_mono) qed @@ -5658,13 +5648,9 @@ using sorted_map_remove1 [of "\x. x"] by simp lemma sorted_butlast: - assumes "xs \ []" and "sorted xs" + assumes "sorted xs" shows "sorted (butlast xs)" -proof - - from \xs \ []\ obtain ys y where "xs = ys @ [y]" - by (cases xs rule: rev_cases) auto - with \sorted xs\ 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 \inj_on f (set xs \ set ys)\ 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 \ 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 \ 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) \ 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 \ set ?dW" + fix x assume x: "x \ 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 "... \ 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 "\ t < f x" by simp qed @@ -7325,12 +7295,15 @@ lemma Cons_acc_listrel1I [intro!]: "x \ Wellfounded.acc r \ xs \ Wellfounded.acc (listrel1 r) \ (x # xs) \ 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 \ 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 \ lists (Wellfounded.acc r) \ xs \ Wellfounded.acc (listrel1 r)" proof (induct set: lists) @@ -7344,11 +7317,13 @@ qed lemma lists_accI: "xs \ Wellfounded.acc (listrel1 r) \ xs \ 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 "\u v. \u \ set x; (v, u) \ r\ \ v \ 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 \ i \ j \ P i \ all_interval_nat P (Suc i) j" proof - have *: "\n. P i \ \n\{Suc i.. i \ n \ n < j \ P n" - proof - - fix n - assume "P i" "\n\{Suc i.. 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 \ i > j \ P i \ all_interval_int P (i + 1) j" proof - have *: "\k. P i \ \k\{i+1..j}. P k \ i \ k \ k \ j \ P k" - proof - - fix k - assume "P i" "\k\{i+1..j}. P k" "i \ k" "k \ 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 \ 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 diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/ATP/atp_problem.ML --- 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 = ":" diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/ATP/atp_proof.ML --- 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; diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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>\False\) 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 \ y" is + prioritized over "x \ 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; diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/ATP/atp_util.ML --- 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) diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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; diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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} diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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, diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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; diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 = diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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} diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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. *) diff -r da41823d09a7 -r df1150ec6cd7 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- 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 diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/Concurrent/future.scala --- 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, diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/Concurrent/isabelle_thread.scala --- 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) diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/ML/ml_console.scala --- 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() diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/ML/ml_process.scala --- 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(_)) diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/PIDE/headless.scala --- 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 } diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/System/isabelle_process.scala --- 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) } diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/Tools/build.scala --- 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 = "" - override def init(build_context: Build_Process.Context): Build_Process = - new Build_Process(build_context) - } + class Default_Engine extends Engine("") { override def toString: String = "" } lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine]) diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/Tools/build_job.scala --- 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()) { diff -r da41823d09a7 -r df1150ec6cd7 src/Pure/Tools/build_process.scala --- 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) } } } diff -r da41823d09a7 -r df1150ec6cd7 src/Tools/VSCode/src/language_server.scala --- 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()) diff -r da41823d09a7 -r df1150ec6cd7 src/Tools/jEdit/src/jedit_sessions.scala --- 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)