# HG changeset patch # User paulson # Date 1621365919 -3600 # Node ID 2e3a60ce5a9f9e9cbc803bcb8202fdc3af2d35f2 # Parent 4b1386b2c23e7405a6ebcd748ae19804a3173241# Parent 06aeb9054c07772f376e92e1090aecfe3384b61b merged diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/Isabelle_app/build --- a/Admin/Isabelle_app/build Tue May 18 20:25:08 2021 +0100 +++ b/Admin/Isabelle_app/build Tue May 18 20:25:19 2021 +0100 @@ -2,6 +2,7 @@ set -e +unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" cd "$THIS" diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/bash_process/build --- a/Admin/bash_process/build Tue May 18 20:25:08 2021 +0100 +++ b/Admin/bash_process/build Tue May 18 20:25:19 2021 +0100 @@ -2,6 +2,7 @@ # # Multi-platform build script +unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" PRG="$(basename "$0")" diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/build --- a/Admin/build Tue May 18 20:25:08 2021 +0100 +++ b/Admin/build Tue May 18 20:25:19 2021 +0100 @@ -5,6 +5,7 @@ ## directory layout if [ -z "$ISABELLE_HOME" ]; then + unset CDPATH ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" fi diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/build_history --- a/Admin/build_history Tue May 18 20:25:08 2021 +0100 +++ b/Admin/build_history Tue May 18 20:25:19 2021 +0100 @@ -2,6 +2,7 @@ # # DESCRIPTION: build history versions from another repository clone +unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" "$THIS/build" jars > /dev/null || exit $? diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/build_release --- a/Admin/build_release Tue May 18 20:25:08 2021 +0100 +++ b/Admin/build_release Tue May 18 20:25:19 2021 +0100 @@ -2,6 +2,7 @@ # # DESCRIPTION: build full Isabelle distribution from repository +unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" "$THIS/build" jars || exit $? diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/cronjob/main --- a/Admin/cronjob/main Tue May 18 20:25:08 2021 +0100 +++ b/Admin/cronjob/main Tue May 18 20:25:19 2021 +0100 @@ -2,6 +2,7 @@ # # DESCRIPTION: start the main Isabelle cronjob +unset CDPATH THIS="$(cd "$(dirname "$0")"; pwd)" source "$HOME/.bashrc" diff -r 06aeb9054c07 -r 2e3a60ce5a9f Admin/init --- a/Admin/init Tue May 18 20:25:08 2021 +0100 +++ b/Admin/init Tue May 18 20:25:19 2021 +0100 @@ -7,6 +7,7 @@ ## environment +unset CDPATH export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle" diff -r 06aeb9054c07 -r 2e3a60ce5a9f bin/isabelle --- a/bin/isabelle Tue May 18 20:25:08 2021 +0100 +++ b/bin/isabelle Tue May 18 20:25:19 2021 +0100 @@ -4,6 +4,8 @@ # # Isabelle tool wrapper. +unset CDPATH + if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" diff -r 06aeb9054c07 -r 2e3a60ce5a9f bin/isabelle_java --- a/bin/isabelle_java Tue May 18 20:25:08 2021 +0100 +++ b/bin/isabelle_java Tue May 18 20:25:19 2021 +0100 @@ -4,6 +4,8 @@ # # Isabelle/Java cold start -- without settings environment +unset CDPATH + if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" diff -r 06aeb9054c07 -r 2e3a60ce5a9f bin/isabelle_scala_script --- a/bin/isabelle_scala_script Tue May 18 20:25:08 2021 +0100 +++ b/bin/isabelle_scala_script Tue May 18 20:25:19 2021 +0100 @@ -4,6 +4,8 @@ # # Isabelle/Scala script wrapper. +unset CDPATH + if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" diff -r 06aeb9054c07 -r 2e3a60ce5a9f etc/components --- a/etc/components Tue May 18 20:25:08 2021 +0100 +++ b/etc/components Tue May 18 20:25:19 2021 +0100 @@ -2,7 +2,6 @@ src/Tools/jEdit src/Tools/Graphview src/Tools/VSCode -src/HOL/Mirabelle src/HOL/Mutabelle src/HOL/Library/Sum_of_Squares src/HOL/SPARK diff -r 06aeb9054c07 -r 2e3a60ce5a9f etc/options --- a/etc/options Tue May 18 20:25:08 2021 +0100 +++ b/etc/options Tue May 18 20:25:19 2021 +0100 @@ -83,6 +83,8 @@ -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" +option parallel_presentation : bool = true + -- "parallel theory presentation" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" @@ -111,6 +113,9 @@ option timeout : real = 0 -- "timeout for session build job (seconds > 0)" +option timeout_build : bool = true + -- "observe timeout for session build" + option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Tue May 18 20:25:19 2021 +0100 @@ -878,7 +878,7 @@ lemma perm_map [intro]: assumes p: "a <~~> b" shows "map f a <~~> map f b" - using p by (simp add: perm_iff_eq_mset) + using p by simp lemma perm_map_switch: assumes m: "map f a = map f b" and p: "b <~~> c" @@ -887,7 +887,7 @@ from m have \length a = length b\ by (rule map_eq_imp_length_eq) from p have \mset c = mset b\ - by (simp add: perm_iff_eq_mset) + by simp then obtain p where \p permutes {.. \permute_list p b = c\ by (rule mset_eq_permutation) with \length a = length b\ have \p permutes {.. @@ -897,48 +897,27 @@ using m \p permutes {.. \permute_list p b = c\ by (auto simp flip: permute_list_map) then show ?thesis - by (auto simp add: perm_iff_eq_mset) + by auto qed lemma (in monoid) perm_assoc_switch: assumes a:"as [\] bs" and p: "bs <~~> cs" shows "\bs'. as <~~> bs' \ bs' [\] cs" - using p a -proof (induction bs cs arbitrary: as) - case (swap y x l) - then show ?case - by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap) -next -case (Cons xs ys z) - then show ?case - by (metis list_all2_Cons2 perm.Cons) -next - case (trans xs ys zs) - then show ?case - by (meson perm.trans) -qed auto +proof - + from p have \mset cs = mset bs\ + by simp + then obtain p where \p permutes {.. \permute_list p bs = cs\ + by (rule mset_eq_permutation) + moreover define bs' where \bs' = permute_list p as\ + ultimately have \as <~~> bs'\ and \bs' [\] cs\ + using a by (auto simp add: list_all2_permute_list_iff list_all2_lengthD) + then show ?thesis by blast +qed lemma (in monoid) perm_assoc_switch_r: assumes p: "as <~~> bs" and a:"bs [\] cs" shows "\bs'. as [\] bs' \ bs' <~~> cs" - using p a -proof (induction as bs arbitrary: cs) - case Nil - then show ?case - by auto -next - case (swap y x l) - then show ?case - by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap) -next - case (Cons xs ys z) - then show ?case - by (metis list_all2_Cons1 perm.Cons) -next - case (trans xs ys zs) - then show ?case - by (blast intro: elim: ) -qed + using a p by (rule list_all2_reorder_left_invariance) declare perm_sym [sym] @@ -946,14 +925,7 @@ assumes perm: "as <~~> bs" and as: "P (set as)" shows "P (set bs)" -proof - - from perm have "mset as = mset bs" - by (simp add: mset_eq_perm) - then have "set as = set bs" - by (rule mset_eq_setD) - with as show "P (set bs)" - by simp -qed + using assms by (metis set_mset_mset) lemmas (in monoid) perm_closed = perm_setP[of _ _ "\as. as \ carrier G"] @@ -1006,7 +978,7 @@ from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\] bcs" by blast assume "as <~~> abs" - with p have pp: "as <~~> bs'" by fast + with p have pp: "as <~~> bs'" by simp from pp ascarr have c1: "set bs' \ carrier G" by (rule perm_closed) from pb bscarr have c2: "set bcs \ carrier G" by (rule perm_closed) assume "bcs [\] cs" @@ -1063,14 +1035,15 @@ assumes prm: "as <~~> bs" and ascarr: "set as \ carrier G" shows "foldr (\) as \ = foldr (\) bs \" - using prm ascarr -proof induction - case (swap y x l) then show ?case - by (simp add: m_lcomm) -next - case (trans xs ys zs) then show ?case - using perm_closed by auto -qed auto +proof - + from prm have \mset (rev as) = mset (rev bs)\ + by simp + moreover note one_closed + ultimately have \fold (\) (rev as) \ = fold (\) (rev bs) \\ + by (rule fold_permuted_eq) (use ascarr in \auto intro: m_lcomm\) + then show ?thesis + by (simp add: foldr_conv_fold) +qed lemma (in comm_monoid_cancel) multlist_ee_cong: assumes "essentially_equal G fs fs'" @@ -1197,12 +1170,13 @@ proof (elim essentially_equalE) fix fs assume prm: "as <~~> fs" - with carr have fscarr: "set fs \ carrier G" by (simp add: perm_closed) + with carr have fscarr: "set fs \ carrier G" + using perm_closed by blast note bfs also assume [symmetric]: "fs [\] bs" also (wfactors_listassoc_cong_l) - note prm[symmetric] + have \mset fs = mset as\ using prm by simp finally (wfactors_perm_cong_l) show "wfactors G as b" by (simp add: carr fscarr) qed @@ -1621,7 +1595,7 @@ lemma (in monoid) fmset_perm_cong: assumes prm: "as <~~> bs" shows "fmset G as = fmset G bs" - using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast + using perm_map[OF prm] unfolding fmset_def by blast lemma (in comm_monoid_cancel) eqc_listassoc_cong: assumes "as [\] bs" and "set as \ carrier G" and "set bs \ carrier G" @@ -1683,7 +1657,7 @@ by (simp_all add: permute_list_map) moreover define as' where \as' = permute_list p as\ ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs" - by (simp_all add: perm_iff_eq_mset) + by simp_all from tp show ?thesis proof (rule essentially_equalI) from tm tp ascarr have as'carr: "set as' \ carrier G" @@ -1941,7 +1915,7 @@ then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" by (fast elim: essentially_equalE) then have "p \ set ds" - by (simp add: perm_set_eq[symmetric]) + by (metis \mset (p # cs) = mset ds\ insert_iff list.set(2) perm_set_eq) with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" unfolding list_all2_conv_all_nth set_conv_nth by force then consider "p' \ set as" | "p' \ set bs" by auto @@ -2003,7 +1977,7 @@ then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\] (as @ bs)" by (fast elim: essentially_equalE) then have "p \ set ds" - by (simp add: perm_set_eq[symmetric]) + by (metis list.set_intros(1) set_mset_mset) with dsassoc obtain p' where "p' \ set (as@bs)" and pp': "p \ p'" unfolding list_all2_conv_all_nth set_conv_nth by force then consider "p' \ set as" | "p' \ set bs" by auto @@ -2641,7 +2615,7 @@ proof (induct as arbitrary: a as') case Nil then have "a \ \" - by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors) + by (simp add: perm_wfactorsD) then have "as' = []" using Nil.prems assoc_unit_l unit_wfactors_empty by blast then show ?case @@ -2728,8 +2702,12 @@ by (simp add: a'carr set_drop set_take) from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')" using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto - with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" - by (auto simp: essentially_equal_def) + then obtain bs where \mset as = mset bs\ \bs [\] take i as' @ drop (Suc i) as'\ + by (auto simp add: essentially_equal_def) + with carr_ah have \mset (ah # as) = mset (ah # bs)\ \ah # bs [\] ah # take i as' @ drop (Suc i) as'\ + by simp_all + then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" + unfolding essentially_equal_def by blast have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') (as' ! i # take i as' @ drop (Suc i) as')" proof (intro essentially_equalI) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Combinatorics/List_Permutation.thy --- a/src/HOL/Combinatorics/List_Permutation.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Combinatorics/List_Permutation.thy Tue May 18 20:25:19 2021 +0100 @@ -13,52 +13,10 @@ \<^text>\Permutations\; it should be seldom needed. \ -subsection \An inductive definition \ldots\ - -inductive perm :: "'a list \ 'a list \ bool" (infixr \<~~>\ 50) -where - Nil [intro!]: "[] <~~> []" -| swap [intro!]: "y # x # l <~~> x # y # l" -| Cons [intro!]: "xs <~~> ys \ z # xs <~~> z # ys" -| trans [intro]: "xs <~~> ys \ ys <~~> zs \ xs <~~> zs" - -proposition perm_refl [iff]: "l <~~> l" - by (induct l) auto - -text \\ldots that is equivalent to an already existing notion:\ +subsection \An existing notion\ -lemma perm_iff_eq_mset: - \xs <~~> ys \ mset xs = mset ys\ -proof - assume \mset xs = mset ys\ - then show \xs <~~> ys\ - proof (induction xs arbitrary: ys) - case Nil - then show ?case - by simp - next - case (Cons x xs) - from Cons.prems [symmetric] have \mset xs = mset (remove1 x ys)\ - by simp - then have \xs <~~> remove1 x ys\ - by (rule Cons.IH) - then have \x # xs <~~> x # remove1 x ys\ - by (rule perm.Cons) - moreover from Cons.prems have \x \ set ys\ - by (auto dest: union_single_eq_member) - then have \x # remove1 x ys <~~> ys\ - by (induction ys) auto - ultimately show \x # xs <~~> ys\ - by (rule perm.trans) - qed -next - assume \xs <~~> ys\ - then show \mset xs = mset ys\ - by induction simp_all -qed - -theorem mset_eq_perm: \mset xs = mset ys \ xs <~~> ys\ - by (simp add: perm_iff_eq_mset) +abbreviation (input) perm :: \'a list \ 'a list \ bool\ (infixr \<~~>\ 50) + where \xs <~~> ys \ mset xs = mset ys\ subsection \Nontrivial conclusions\ @@ -66,29 +24,29 @@ proposition perm_swap: \xs[i := xs ! j, j := xs ! i] <~~> xs\ if \i < length xs\ \j < length xs\ - using that by (simp add: perm_iff_eq_mset mset_swap) + using that by (simp add: mset_swap) proposition mset_le_perm_append: "mset xs \# mset ys \ (\zs. xs @ zs <~~> ys)" - by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym) + by (auto simp add: mset_subset_eq_exists_conv ex_mset dest: sym) proposition perm_set_eq: "xs <~~> ys \ set xs = set ys" - by (rule mset_eq_setD) (simp add: perm_iff_eq_mset) + by (rule mset_eq_setD) simp proposition perm_distinct_iff: "xs <~~> ys \ distinct xs \ distinct ys" - by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset) + by (rule mset_eq_imp_distinct_iff) simp theorem eq_set_perm_remdups: "set xs = set ys \ remdups xs <~~> remdups ys" - by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) + by (simp add: set_eq_iff_mset_remdups_eq) proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \ set x = set y" - by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) + by (simp add: set_eq_iff_mset_remdups_eq) theorem permutation_Ex_bij: assumes "xs <~~> ys" shows "\f. bij_betw f {.. (\imset xs = mset ys\ \length xs = length ys\ - by (auto simp add: perm_iff_eq_mset dest: mset_eq_length) + by (auto simp add: dest: mset_eq_length) from \mset xs = mset ys\ obtain p where \p permutes {.. \permute_list p ys = xs\ by (rule mset_eq_permutation) then have \bij_betw p {.. @@ -101,84 +59,84 @@ qed proposition perm_finite: "finite {B. B <~~> A}" - using mset_eq_finite by (auto simp add: perm_iff_eq_mset) + using mset_eq_finite by auto subsection \Trivial conclusions:\ proposition perm_empty_imp: "[] <~~> ys \ ys = []" - by (simp add: perm_iff_eq_mset) + by simp text \\medskip This more general theorem is easier to understand!\ proposition perm_length: "xs <~~> ys \ length xs = length ys" - by (rule mset_eq_length) (simp add: perm_iff_eq_mset) + by (rule mset_eq_length) simp proposition perm_sym: "xs <~~> ys \ ys <~~> xs" - by (simp add: perm_iff_eq_mset) + by simp text \We can insert the head anywhere in the list.\ proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append_swap: "xs @ ys <~~> ys @ xs" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append_single: "a # xs <~~> xs @ [a]" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_rev: "rev xs <~~> xs" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append1: "xs <~~> ys \ l @ xs <~~> l @ ys" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append2: "xs <~~> ys \ xs @ l <~~> ys @ l" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_empty [iff]: "[] <~~> xs \ xs = []" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_empty2 [iff]: "xs <~~> [] \ xs = []" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_sing_imp: "ys <~~> xs \ xs = [y] \ ys = [y]" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_sing_eq [iff]: "ys <~~> [y] \ ys = [y]" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_sing_eq2 [iff]: "[y] <~~> ys \ ys = [y]" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_remove: "x \ set ys \ ys <~~> x # remove1 x ys" - by (simp add: perm_iff_eq_mset) + by simp text \\medskip Congruence rule\ proposition perm_remove_perm: "xs <~~> ys \ remove1 z xs <~~> remove1 z ys" - by (simp add: perm_iff_eq_mset) + by simp proposition remove_hd [simp]: "remove1 z (z # xs) = xs" - by (simp add: perm_iff_eq_mset) + by simp proposition cons_perm_imp_perm: "z # xs <~~> z # ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) + by simp proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) + by simp proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) + by simp proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \ xs <~~> ys" - by (simp add: perm_iff_eq_mset) + by simp end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Combinatorics/Permutations.thy --- a/src/HOL/Combinatorics/Permutations.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Combinatorics/Permutations.thy Tue May 18 20:25:19 2021 +0100 @@ -1150,6 +1150,11 @@ by (induct xs) (auto simp: inv_f_f surj_f_inv_f) qed +lemma list_all2_permute_list_iff: + \list_all2 P (permute_list p xs) (permute_list p ys) \ list_all2 P xs ys\ + if \p permutes {.. + using that by (auto simp add: list_all2_iff simp flip: permute_list_zip) + subsection \More lemmas about permutations\ diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Library/Multiset.thy Tue May 18 20:25:19 2021 +0100 @@ -1923,26 +1923,55 @@ using assms by (metis count_mset) lemma fold_multiset_equiv: - assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" - and equiv: "mset xs = mset ys" - shows "List.fold f xs = List.fold f ys" - using f equiv [symmetric] -proof (induct xs arbitrary: ys) + \List.fold f xs = List.fold f ys\ + if f: \\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x\ + and \mset xs = mset ys\ +using f \mset xs = mset ys\ [symmetric] proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) - then have *: "set ys = set (x # xs)" + then have *: \set ys = set (x # xs)\ by (blast dest: mset_eq_setD) - have "\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x" + have \\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x\ by (rule Cons.prems(1)) (simp_all add: *) - moreover from * have "x \ set ys" + moreover from * have \x \ set ys\ + by simp + ultimately have \List.fold f ys = List.fold f (remove1 x ys) \ f x\ + by (fact fold_remove1_split) + moreover from Cons.prems have \List.fold f xs = List.fold f (remove1 x ys)\ + by (auto intro: Cons.IH) + ultimately show ?case by simp - ultimately have "List.fold f ys = List.fold f (remove1 x ys) \ f x" - by (fact fold_remove1_split) - moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" - by (auto intro: Cons.hyps) - ultimately show ?case by simp +qed + +lemma fold_permuted_eq: + \List.fold (\) xs z = List.fold (\) ys z\ + if \mset xs = mset ys\ + and \P z\ and P: \\x z. x \ set xs \ P z \ P (x \ z)\ + and f: \\x y z. x \ set xs \ y \ set xs \ P z \ x \ (y \ z) = y \ (x \ z)\ + for f (infixl \\\ 70) +using \P z\ P f \mset xs = mset ys\ [symmetric] proof (induction xs arbitrary: ys z) + case Nil + then show ?case by simp +next + case (Cons x xs) + then have *: \set ys = set (x # xs)\ + by (blast dest: mset_eq_setD) + have \P z\ + by (fact Cons.prems(1)) + moreover have \\x z. x \ set ys \ P z \ P (x \ z)\ + by (rule Cons.prems(2)) (simp_all add: *) + moreover have \\x y z. x \ set ys \ y \ set ys \ P z \ x \ (y \ z) = y \ (x \ z)\ + by (rule Cons.prems(3)) (simp_all add: *) + moreover from * have \x \ set ys\ + by simp + ultimately have \fold (\) ys z = fold (\) (remove1 x ys) (x \ z)\ + by (induction ys arbitrary: z) auto + moreover from Cons.prems have \fold (\) xs (x \ z) = fold (\) (remove1 x ys) (x \ z)\ + by (auto intro: Cons.IH) + ultimately show ?case + by simp qed lemma mset_shuffles: "zs \ shuffles xs ys \ mset zs = mset xs + mset ys" diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Main.thy --- a/src/HOL/Main.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Main.thy Tue May 18 20:25:19 2021 +0100 @@ -9,6 +9,7 @@ imports Predicate_Compile Quickcheck_Narrowing + Mirabelle Extraction Nunchaku BNF_Greatest_Fixpoint diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle.thy Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,18 @@ +(* Title: HOL/Mirabelle.thy + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius +*) + +theory Mirabelle + imports Sledgehammer Predicate_Compile +begin + +ML_file \Tools/Mirabelle/mirabelle.ML\ +ML_file \Tools/Mirabelle/mirabelle_arith.ML\ +ML_file \Tools/Mirabelle/mirabelle_metis.ML\ +ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ +ML_file \Tools/Mirabelle/mirabelle_sledgehammer.ML\ +ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ +ML_file \Tools/Mirabelle/mirabelle_try0.ML\ + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/Mirabelle/Mirabelle.thy - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -theory Mirabelle -imports Main -begin - -ML_file \Tools/mirabelle.ML\ -ML_file \../TPTP/sledgehammer_tactics.ML\ - -ML \Toplevel.add_hook Mirabelle.step_hook\ - -ML \ -signature MIRABELLE_ACTION = -sig - val invoke : (string * string) list -> theory -> theory -end -\ - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Mirabelle_Test.thy --- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: HOL/Mirabelle/Mirabelle_Test.thy - Author: Sascha Boehme, TU Munich -*) - -section \Simple test theory for Mirabelle actions\ - -theory Mirabelle_Test -imports Main Mirabelle -begin - -ML_file \Tools/mirabelle_arith.ML\ -ML_file \Tools/mirabelle_metis.ML\ -ML_file \Tools/mirabelle_quickcheck.ML\ -ML_file \Tools/mirabelle_refute.ML\ -ML_file \Tools/mirabelle_sledgehammer.ML\ -ML_file \Tools/mirabelle_sledgehammer_filter.ML\ -ML_file \Tools/mirabelle_try0.ML\ - -text \ - Only perform type-checking of the actions, - any reasonable test would be too complicated. -\ - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -signature MIRABELLE = -sig - (*configuration*) - val logfile : string Config.T - val timeout : int Config.T - val start_line : int Config.T - val end_line : int Config.T - - (*core*) - type init_action = int -> theory -> theory - type done_args = {last: Toplevel.state, log: string -> unit} - type done_action = int -> done_args -> unit - type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} - type run_action = int -> run_args -> unit - type action = init_action * run_action * done_action - val catch : (int -> string) -> run_action -> run_action - val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> - int -> run_args -> 'a - val register : action -> theory -> theory - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> - unit - - (*utility functions*) - val can_apply : Time.time -> (Proof.context -> int -> tactic) -> - Proof.state -> bool - val theorems_in_proof_term : theory -> thm -> thm list - val theorems_of_sucessful_proof : Toplevel.state option -> thm list - val get_setting : (string * string) list -> string * string -> string - val get_int_setting : (string * string) list -> string * int -> int - val get_bool_setting : (string * string) list -> string * bool -> bool - val cpu_time : ('a -> 'b) -> 'a -> 'b * int -end - - - -structure Mirabelle : MIRABELLE = -struct - -(* Mirabelle configuration *) - -val logfile = Attrib.setup_config_string \<^binding>\mirabelle_logfile\ (K "") -val timeout = Attrib.setup_config_int \<^binding>\mirabelle_timeout\ (K 30) -val start_line = Attrib.setup_config_int \<^binding>\mirabelle_start_line\ (K 0) -val end_line = Attrib.setup_config_int \<^binding>\mirabelle_end_line\ (K ~1) - - -(* Mirabelle core *) - -type init_action = int -> theory -> theory -type done_args = {last: Toplevel.state, log: string -> unit} -type done_action = int -> done_args -> unit -type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} -type run_action = int -> run_args -> unit -type action = init_action * run_action * done_action - -structure Actions = Theory_Data -( - type T = (int * run_action * done_action) list - val empty = [] - val extend = I - fun merge data = Library.merge (K true) data (* FIXME potential data loss because of (K true) *) -) - - -fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e) - -fun catch tag f id (st as {log, ...}: run_args) = (f id st; ()) - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ()) - -fun catch_result tag d f id (st as {log, ...}: run_args) = f id st - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d) - -fun register (init, run, done) thy = - let val id = length (Actions.get thy) + 1 - in - thy - |> init id - |> Actions.map (cons (id, run, done)) - end - -local - -fun log thy s = - let fun append_to n = if n = "" then K () else File.append (Path.explode n) - in append_to (Config.get_global thy logfile) (s ^ "\n") end - (* FIXME: with multithreading and parallel proofs enabled, we might need to - encapsulate this inside a critical section *) - -fun log_sep thy = log thy "------------------" - -fun apply_actions thy pos name info (pre, post, time) actions = - let - fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} - fun run (id, run, _) = (apply (run id); log_sep thy) - in (log thy info; log_sep thy; List.app run actions) end - -fun in_range _ _ NONE = true - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) - -fun only_within_range thy pos f x = - let val l = Config.get_global thy start_line and r = Config.get_global thy end_line - in if in_range l r (Position.line_of pos) then f x else () end - -in - -fun run_actions tr pre post = - let - val thy = Proof.theory_of pre - val pos = Toplevel.pos_of tr - val name = Toplevel.name_of tr - val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout)) - - val str0 = string_of_int o the_default 0 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) - val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" - in - only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) - end - -fun done_actions st = - let - val thy = Toplevel.theory_of st - val _ = log thy "\n\n"; - in - thy - |> Actions.get - |> List.app (fn (id, _, done) => done id {last=st, log=log thy}) - end - -end - -val whitelist = ["apply", "by", "proof"] - -fun step_hook tr pre post = - (* FIXME: might require wrapping into "interruptible" *) - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso - member (op =) whitelist (Toplevel.name_of tr) - then run_actions tr (Toplevel.proof_of pre) (SOME post) - else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post - then done_actions pre - else () (* FIXME: add theory_hook here *) - - - -(* Mirabelle utility functions *) - -fun can_apply time tac st = - let - val {context = ctxt, facts, goal} = Proof.goal st - val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt) - in - (case try (Timeout.apply time (Seq.pull o full_tac)) goal of - SOME (SOME _) => true - | _ => false) - end - -local - -fun fold_body_thms f = - let - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => - fn (x, seen) => - if Inttab.defined seen i then (x, seen) - else - let - val name = Proofterm.thm_node_name thm_node - val prop = Proofterm.thm_node_prop thm_node - val body = Future.join (Proofterm.thm_node_body thm_node) - val (x', seen') = app (n + (if name = "" then 0 else 1)) body - (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end - -in - -fun theorems_in_proof_term thy thm = - let - val all_thms = Global_Theory.all_thms_of thy true - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE - fun resolve_thms names = map_filter (member_of names) all_thms - in - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) - end - -end - -fun theorems_of_sucessful_proof state = - (case state of - NONE => [] - | SOME st => - if not (Toplevel.is_proof st) then [] - else - theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st)))) - -fun get_setting settings (key, default) = - the_default default (AList.lookup (op =) settings key) - -fun get_int_setting settings (key, default) = - (case Option.map Int.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | SOME NONE => error ("bad option: " ^ key) - | NONE => default) - -fun get_bool_setting settings (key, default) = - (case Option.map Bool.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | SOME NONE => error ("bad option: " ^ key) - | NONE => default) - -fun cpu_time f x = - let val ({cpu, ...}, y) = Timing.timing f x - in (y, Time.toMilliseconds cpu) end - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_arith.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Arith : MIRABELLE_ACTION = -struct - -fun arith_tag id = "#" ^ string_of_int id ^ " arith: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then log (arith_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Metis : MIRABELLE_ACTION = -struct - -fun metis_tag id = "#" ^ string_of_int id ^ " metis: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = - let - val thms = Mirabelle.theorems_of_sucessful_proof post - val names = map Thm.get_name_hint thms - val add_info = if null names then I else suffix (":\n" ^ commas names) - - val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))) - - fun metis ctxt = - Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt - (thms @ facts) - in - (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> prefix (metis_tag id) - |> add_info - |> log - end - handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout") - | ERROR msg => log (metis_tag id ^ "error: " ^ msg) - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Quickcheck : MIRABELLE_ACTION = -struct - -fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " - -fun init _ = I -fun done _ _ = () - -fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) = - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst - val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1 - in - (case Timeout.apply timeout quickcheck pre of - NONE => log (qc_tag id ^ "no counterexample") - | SOME _ => log (qc_tag id ^ "counterexample found")) - end - handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout") - | ERROR msg => log (qc_tag id ^ "error: " ^ msg) - -fun invoke args = - Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_refute.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_refute.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Refute : MIRABELLE_ACTION = -struct - - -(* FIXME: -fun refute_action args timeout {pre=st, ...} = - let - val subgoal = 1 - val thy = Proof.theory_of st - val thm = #goal (Proof.raw_goal st) - - val refute = Refute.refute_goal thy args thm - val _ = Timeout.apply timeout refute subgoal - in - val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) - val warn_log = Substring.full (the (Symtab.lookup tab "warning")) - - val r = - if Substring.isSubstring "model found" writ_log - then - if Substring.isSubstring "spurious" warn_log - then SOME "potential counterexample" - else SOME "real counterexample (bug?)" - else - if Substring.isSubstring "time limit" writ_log - then SOME "no counterexample (timeout)" - else if Substring.isSubstring "Search terminated" writ_log - then SOME "no counterexample (normal termination)" - else SOME "no counterexample (unknown)" - in r end -*) - -fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,658 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich -*) - -structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = -struct - -(*To facilitate synching the description of Mirabelle Sledgehammer parameters - (in ../lib/Tools/mirabelle) with the parameters actually used by this - interface, the former extracts PARAMETER and DESCRIPTION from code below which - has this pattern (provided it appears in a single line): - val .*K = "PARAMETER" (*DESCRIPTION*) -*) -(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) - -val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) -val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) -val fact_filterK = "fact_filter" (*=STRING: fact filter*) -val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) -val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) -val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) -val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) -val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) -val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) -val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) -val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) -val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) -val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) -val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) -val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) -val proverK = "prover" (*=STRING: name of the external prover to call*) -val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) -val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) -val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) -val strictK = "strict" (*=BOOL: run in strict mode*) -val strideK = "stride" (*=NUM: run every nth goal*) -val term_orderK = "term_order" (*=STRING: term order (in E)*) -val type_encK = "type_enc" (*=STRING: type encoding scheme*) -val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) - -fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " -fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " - -val separator = "-----" - -(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) -(*defaults used in this Mirabelle action*) -val preplay_timeout_default = "1" -val lam_trans_default = "smart" -val uncurried_aliases_default = "smart" -val fact_filter_default = "smart" -val type_enc_default = "smart" -val strict_default = "false" -val stride_default = 1 -val max_facts_default = "smart" -val slice_default = "true" -val max_calls_default = 10000000 -val check_trivial_default = false - -(*If a key is present in args then augment a list with its pair*) -(*This is used to avoid fixing default values at the Mirabelle level, and - instead use the default values of the tool (Sledgehammer in this case).*) -fun available_parameter args key label list = - let - val value = AList.lookup (op =) args key - in if is_some value then (label, the value) :: list else list end - -datatype sh_data = ShData of { - calls: int, - success: int, - nontriv_calls: int, - nontriv_success: int, - lemmas: int, - max_lems: int, - time_isa: int, - time_prover: int, - time_prover_fail: int} - -datatype re_data = ReData of { - calls: int, - success: int, - nontriv_calls: int, - nontriv_success: int, - proofs: int, - time: int, - timeout: int, - lemmas: int * int * int, - posns: (Position.T * bool) list - } - -fun make_sh_data - (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, - time_prover,time_prover_fail) = - ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, - nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, - time_isa=time_isa, time_prover=time_prover, - time_prover_fail=time_prover_fail} - -fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, - timeout,lemmas,posns) = - ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, - nontriv_success=nontriv_success, proofs=proofs, time=time, - timeout=timeout, lemmas=lemmas, posns=posns} - -val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) -val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) - -fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, - lemmas, max_lems, time_isa, - time_prover, time_prover_fail}) = (calls, success, nontriv_calls, - nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) - -fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, - proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, - nontriv_success, proofs, time, timeout, lemmas, posns) - -datatype data = Data of { - sh: sh_data, - re_u: re_data (* proof method with unminimized set of lemmas *) - } - -fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} - -val empty_data = make_data (empty_sh_data, empty_re_data) - -fun map_sh_data f (Data {sh, re_u}) = - let val sh' = make_sh_data (f (tuple_of_sh_data sh)) - in make_data (sh', re_u) end - -fun map_re_data f (Data {sh, re_u}) = - let - val f' = make_re_data o f o tuple_of_re_data - val re_u' = f' re_u - in make_data (sh, re_u') end - -fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); - -val inc_sh_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_nontriv_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_nontriv_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) - -fun inc_sh_lemmas n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) - -fun inc_sh_max_lems n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) - -fun inc_sh_time_isa t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) - -fun inc_sh_time_prover t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) - -fun inc_sh_time_prover_fail t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) - -val inc_proof_method_calls = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_success = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_nontriv_calls = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_nontriv_success = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_proofs = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) - -fun inc_proof_method_time t = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) - -val inc_proof_method_timeout = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) - -fun inc_proof_method_lemmas n = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) - -fun inc_proof_method_posns pos = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) - -val str0 = string_of_int o the_default 0 - -local - -val str = string_of_int -val str3 = Real.fmt (StringCvt.FIX (SOME 3)) -fun percentage a b = string_of_int (a * 100 div b) -fun time t = Real.fromInt t / 1000.0 -fun avg_time t n = - if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 - -fun log_sh_data log - (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = - (log ("Total number of sledgehammer calls: " ^ str calls); - log ("Number of successful sledgehammer calls: " ^ str success); - log ("Number of sledgehammer lemmas: " ^ str lemmas); - log ("Max number of sledgehammer lemmas: " ^ str max_lems); - log ("Success rate: " ^ percentage success calls ^ "%"); - log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); - log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); - log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); - log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); - log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); - log ("Average time for sledgehammer calls (Isabelle): " ^ - str3 (avg_time time_isa calls)); - log ("Average time for successful sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover success)); - log ("Average time for failed sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover_fail (calls - success))) - ) - -fun str_of_pos (pos, triv) = - str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ - (if triv then "[T]" else "") - -fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, - re_nontriv_success, re_proofs, re_time, re_timeout, - (lemmas, lems_sos, lems_max), re_posns) = - (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); - log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ - " (proof: " ^ str re_proofs ^ ")"); - log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); - log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); - log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); - log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ - " (proof: " ^ str re_proofs ^ ")"); - log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); - log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); - log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); - log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); - log ("Average time for successful " ^ tag ^ "proof method calls: " ^ - str3 (avg_time re_time re_success)); - if tag="" - then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) - else () - ) - -in - -fun log_data id log (Data {sh, re_u}) = - let - val ShData {calls=sh_calls, ...} = sh - - fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () - fun log_re tag m = - log_re_data log tag sh_calls (tuple_of_re_data m) - fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log "")) - in - if sh_calls > 0 - then - (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); - log_sh_data log (tuple_of_sh_data sh); - log ""; - log_proof_method ("", re_u)) - else () - end - -end - -(* Warning: we implicitly assume single-threaded execution here *) -val data = Unsynchronized.ref ([] : (int * data) list) - -fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) -fun done id ({log, ...}: Mirabelle.done_args) = - AList.lookup (op =) (!data) id - |> Option.map (log_data id log) - |> K () - -fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) - -fun get_prover_name thy args = - let - fun default_prover_name () = - hd (#provers (Sledgehammer_Commands.default_params thy [])) - handle List.Empty => error "No ATP available" - in - (case AList.lookup (op =) args proverK of - SOME name => name - | NONE => default_prover_name ()) - end - -fun get_prover ctxt name params goal = - let - val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) - in - Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name - end - -type stature = ATP_Problem_Generate.stature - -fun is_good_line s = - (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) - andalso not (String.isSubstring "(> " s) - andalso not (String.isSubstring ", > " s) - andalso not (String.isSubstring "may fail" s) - -(* Fragile hack *) -fun proof_method_from_msg args msg = - (case AList.lookup (op =) args proof_methodK of - SOME name => - if name = "smart" then - if exists is_good_line (split_lines msg) then - "none" - else - "fail" - else - name - | NONE => - if exists is_good_line (split_lines msg) then - "none" (* trust the preplayed proof *) - else if String.isSubstring "metis (" msg then - msg |> Substring.full - |> Substring.position "metis (" - |> snd |> Substring.position ")" - |> fst |> Substring.string - |> suffix ")" - else if String.isSubstring "metis" msg then - "metis" - else - "smt") - -local - -datatype sh_result = - SH_OK of int * int * (string * stature) list | - SH_FAIL of int * int | - SH_ERROR - -fun run_sh prover_name fact_filter type_enc strict max_facts slice - lam_trans uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = - let - val thy = Proof.theory_of st - val {context = ctxt, facts = chained_ths, goal} = Proof.goal st - val i = 1 - fun set_file_name (SOME dir) = - Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir - #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix - ("prob_" ^ str0 (Position.line_of pos) ^ "__") - #> Config.put SMT_Config.debug_files - (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" - ^ serial_string ()) - | set_file_name NONE = I - val st' = - st - |> Proof.map_context - (set_file_name dir - #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) - e_selection_heuristic |> the_default I) - #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) - term_order |> the_default I) - #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) - force_sos |> the_default I)) - val params as {max_facts, minimize, preplay_timeout, ...} = - Sledgehammer_Commands.default_params thy - ([(* ("verbose", "true"), *) - ("fact_filter", fact_filter), - ("type_enc", type_enc), - ("strict", strict), - ("lam_trans", lam_trans |> the_default lam_trans_default), - ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), - ("max_facts", max_facts), - ("slice", slice), - ("timeout", string_of_int timeout), - ("preplay_timeout", preplay_timeout)] - |> isar_proofsLST - |> smt_proofsLST - |> minimizeLST (*don't confuse the two minimization flags*) - |> max_new_mono_instancesLST - |> max_mono_itersLST) - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt - val time_limit = - (case hard_timeout of - NONE => I - | SOME secs => Timeout.apply (Time.fromSeconds secs)) - fun failed failure = - ({outcome = SOME failure, used_facts = [], used_from = [], - preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, - message = K ""}, ~1) - val ({outcome, used_facts, preferred_methss, run_time, message, ...} - : Sledgehammer_Prover.prover_result, - time_isa) = time_limit (Mirabelle.cpu_time (fn () => - let - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - val factss = - facts - |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name - (the_default default_max_facts max_facts) - Sledgehammer_Fact.no_fact_override hyp_ts concl_t - |> tap (fn factss => - "Line " ^ str0 (Position.line_of pos) ^ ": " ^ - Sledgehammer.string_of_factss factss - |> writeln) - val prover = get_prover ctxt prover_name params goal - val problem = - {comment = "", state = st', goal = goal, subgoal = i, - subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} - in prover params problem end)) () - handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut - | Fail "inappropriate" => failed ATP_Proof.Inappropriate - val time_prover = run_time |> Time.toMilliseconds - val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts - st' i preferred_methss) - in - (case outcome of - NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) - | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) - end - handle ERROR msg => ("error: " ^ msg, SH_ERROR) - -in - -fun run_sledgehammer trivial args proof_method named_thms id - ({pre=st, log, pos, ...}: Mirabelle.run_args) = - let - val thy = Proof.theory_of st - val triv_str = if trivial then "[T] " else "" - val _ = change_data id inc_sh_calls - val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val prover_name = get_prover_name thy args - val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default - val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default - val strict = AList.lookup (op =) args strictK |> the_default strict_default - val max_facts = - (case AList.lookup (op =) args max_factsK of - SOME max => max - | NONE => - (case AList.lookup (op =) args max_relevantK of - SOME max => max - | NONE => max_facts_default)) - val slice = AList.lookup (op =) args sliceK |> the_default slice_default - val lam_trans = AList.lookup (op =) args lam_transK - val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK - val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK - val term_order = AList.lookup (op =) args term_orderK - val force_sos = AList.lookup (op =) args force_sosK - |> Option.map (curry (op <>) "false") - val dir = AList.lookup (op =) args keepK - val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) - (* always use a hard timeout, but give some slack so that the automatic - minimizer has a chance to do its magic *) - val preplay_timeout = AList.lookup (op =) args preplay_timeoutK - |> the_default preplay_timeout_default - val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" - val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" - val minimizeLST = available_parameter args minimizeK "minimize" - val max_new_mono_instancesLST = - available_parameter args max_new_mono_instancesK max_new_mono_instancesK - val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK - val hard_timeout = SOME (4 * timeout) - val (msg, result) = - run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans - uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st - in - (case result of - SH_OK (time_isa, time_prover, names) => - let - fun get_thms (name, stature) = - try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) - name - |> Option.map (pair (name, stature)) - in - change_data id inc_sh_success; - if trivial then () else change_data id inc_sh_nontriv_success; - change_data id (inc_sh_lemmas (length names)); - change_data id (inc_sh_max_lems (length names)); - change_data id (inc_sh_time_isa time_isa); - change_data id (inc_sh_time_prover time_prover); - proof_method := proof_method_from_msg args msg; - named_thms := SOME (map_filter get_thms names); - log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ - string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) - end - | SH_FAIL (time_isa, time_prover) => - let - val _ = change_data id (inc_sh_time_isa time_isa) - val _ = change_data id (inc_sh_time_prover_fail time_prover) - in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end - | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)) - end - -end - -fun override_params prover type_enc timeout = - [("provers", prover), - ("max_facts", "0"), - ("type_enc", type_enc), - ("strict", "true"), - ("slice", "false"), - ("timeout", timeout |> Time.toSeconds |> string_of_int)] - -fun run_proof_method trivial full name meth named_thms id - ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = - let - fun do_method named_thms ctxt = - let - val ref_of_str = (* FIXME proper wrapper for parser combinators *) - suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none - #> Parse.thm #> fst - val thms = named_thms |> maps snd - val facts = named_thms |> map (ref_of_str o fst o fst) - val fact_override = {add = facts, del = [], only = true} - fun my_timeout time_slice = - timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal - fun sledge_tac time_slice prover type_enc = - Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (override_params prover type_enc (my_timeout time_slice)) fact_override [] - in - if !meth = "sledgehammer_tac" then - sledge_tac 0.2 ATP_Proof.vampireN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" - ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" - ORELSE' SMT_Solver.smt_tac ctxt thms - else if !meth = "smt" then - SMT_Solver.smt_tac ctxt thms - else if full then - Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] - ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if String.isPrefix "metis (" (!meth) then - let - val (type_encs, lam_trans) = - !meth - |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start - |> filter Token.is_proper |> tl - |> Metis_Tactic.parse_metis_options |> fst - |>> the_default [ATP_Proof_Reconstruct.partial_typesN] - ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans - in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end - else if !meth = "metis" then - Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if !meth = "none" then - K all_tac - else if !meth = "fail" then - K no_tac - else - (warning ("Unknown method " ^ quote (!meth)); K no_tac) - end - fun apply_method named_thms = - Mirabelle.can_apply timeout (do_method named_thms) st - - fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" - | with_time (true, t) = (change_data id inc_proof_method_success; - if trivial then () - else change_data id inc_proof_method_nontriv_success; - change_data id (inc_proof_method_lemmas (length named_thms)); - change_data id (inc_proof_method_time t); - change_data id (inc_proof_method_posns (pos, trivial)); - if name = "proof" then change_data id inc_proof_method_proofs else (); - "succeeded (" ^ string_of_int t ^ ")") - fun timed_method named_thms = - (with_time (Mirabelle.cpu_time apply_method named_thms), true) - handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false)) - | ERROR msg => ("error: " ^ msg, false) - - val _ = log separator - val _ = change_data id inc_proof_method_calls - val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls - in - named_thms - |> timed_method - |>> log o prefix (proof_method_tag meth id) - |> snd - end - -val try_timeout = seconds 5.0 - -(* crude hack *) -val num_sledgehammer_calls = Unsynchronized.ref 0 -val remaining_stride = Unsynchronized.ref stride_default - -fun sledgehammer_action args = - let - val stride = Mirabelle.get_int_setting args (strideK, stride_default) - val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default) - val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default) - in - fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) => - let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in - if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then - () - else if !remaining_stride > 1 then - (* We still have some steps to do *) - (remaining_stride := !remaining_stride - 1; - log "Skipping because of stride") - else - (* This was the last step, now run the action *) - let - val _ = remaining_stride := stride - val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1 - in - if !num_sledgehammer_calls > max_calls then - log "Skipping because max number of calls reached" - else - let - val meth = Unsynchronized.ref "" - val named_thms = - Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) - val trivial = - if check_trivial then - Try0.try0 (SOME try_timeout) ([], [], [], []) pre - handle Timeout.TIMEOUT _ => false - else false - fun apply_method () = - (Mirabelle.catch_result (proof_method_tag meth) false - (run_proof_method trivial false name meth (these (!named_thms))) id st; ()) - in - Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; - if is_some (!named_thms) then apply_method () else () - end - end - end - end - -fun invoke args = - Mirabelle.register (init, sledgehammer_action args, done) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,178 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML - Author: Jasmin Blanchette, TU Munich -*) - -structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = -struct - -fun get args name default_value = - case AList.lookup (op =) args name of - SOME value => Value.parse_real value - | NONE => default_value - -fun extract_relevance_fudge args - {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, - abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight, - chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus, - chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} = - {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier, - worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, - higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight, - abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, - abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, - theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight, - theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight, - chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight, - intro_bonus = get args "intro_bonus" intro_bonus, - elim_bonus = get args "elim_bonus" elim_bonus, - simp_bonus = get args "simp_bonus" simp_bonus, - local_bonus = get args "local_bonus" local_bonus, - assum_bonus = get args "assum_bonus" assum_bonus, - chained_bonus = get args "chained_bonus" chained_bonus, - max_imperfect = get args "max_imperfect" max_imperfect, - max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, - threshold_divisor = get args "threshold_divisor" threshold_divisor, - ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} - -structure Prooftab = - Table(type key = int * int val ord = prod_ord int_ord int_ord) - -val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table) - -val num_successes = Unsynchronized.ref ([] : (int * int) list) -val num_failures = Unsynchronized.ref ([] : (int * int) list) -val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) -val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) -val num_found_facts = Unsynchronized.ref ([] : (int * int) list) -val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) - -fun get id c = the_default 0 (AList.lookup (op =) (!c) id) -fun add id c n = - c := (case AList.lookup (op =) (!c) id of - SOME m => AList.update (op =) (id, m + n) (!c) - | NONE => (id, n) :: !c) - -fun init proof_file _ thy = - let - fun do_line line = - (case line |> space_explode ":" of - [line_num, offset, proof] => - SOME (apply2 (the o Int.fromString) (line_num, offset), - proof |> space_explode " " |> filter_out (curry (op =) "")) - | _ => NONE) - val proofs = File.read (Path.explode proof_file) - val proof_tab = - proofs |> space_explode "\n" - |> map_filter do_line - |> AList.coalesce (op =) - |> Prooftab.make - in proof_table := proof_tab; thy end - -fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) -fun percentage_alt a b = percentage a (a + b) - -fun done id ({log, ...} : Mirabelle.done_args) = - if get id num_successes + get id num_failures > 0 then - (log ""; - log ("Number of overall successes: " ^ string_of_int (get id num_successes)); - log ("Number of overall failures: " ^ string_of_int (get id num_failures)); - log ("Overall success rate: " ^ - percentage_alt (get id num_successes) (get id num_failures) ^ "%"); - log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs)); - log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs)); - log ("Proof found rate: " ^ - percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ "%"); - log ("Number of found facts: " ^ string_of_int (get id num_found_facts)); - log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts)); - log ("Fact found rate: " ^ - percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ "%")) - else - () - -val default_prover = ATP_Proof.eN (* arbitrary ATP *) - -fun with_index (i, s) = s ^ "@" ^ string_of_int i - -fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = - case (Position.line_of pos, Position.offset_of pos) of - (SOME line_num, SOME offset) => - (case Prooftab.lookup (!proof_table) (line_num, offset) of - SOME proofs => - let - val thy = Proof.theory_of pre - val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre - val prover = AList.lookup (op =) args "prover" |> the_default default_prover - val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover - val relevance_fudge = - extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge - val subgoal = 1 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - |> Sledgehammer_Fact.drop_duplicate_facts - |> Sledgehammer_MePo.mepo_suggested_facts ctxt params - (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t - |> map (fst o fst) - val (found_facts, lost_facts) = - flat proofs |> sort_distinct string_ord - |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) - |> List.partition (curry (op <=) 0 o fst) - |>> sort (prod_ord int_ord string_ord) ||> map snd - val found_proofs = filter (forall (member (op =) facts)) proofs - val n = length found_proofs - val _ = - if n = 0 then - (add id num_failures 1; log "Failure") - else - (add id num_successes 1; - add id num_found_proofs n; - log ("Success (" ^ string_of_int n ^ " of " ^ - string_of_int (length proofs) ^ " proofs)")) - val _ = add id num_lost_proofs (length proofs - n) - val _ = add id num_found_facts (length found_facts) - val _ = add id num_lost_facts (length lost_facts) - val _ = - if null found_facts then - () - else - let - val found_weight = - Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) - / Real.fromInt (length found_facts) - |> Math.sqrt |> Real.ceil - in - log ("Found facts (among " ^ string_of_int (length facts) ^ - ", weight " ^ string_of_int found_weight ^ "): " ^ - commas (map with_index found_facts)) - end - val _ = if null lost_facts then - () - else - log ("Lost facts (among " ^ string_of_int (length facts) ^ - "): " ^ commas lost_facts) - in () end - | NONE => log "No known proof") - | _ => () - -val proof_fileK = "proof_file" - -fun invoke args = - let - val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst) - val proof_file = - (case pf_args of - [] => error "No \"proof_file\" specified" - | (_, s) :: _ => s) - in Mirabelle.register (init proof_file, action other_args, done) end - -end; - -(* Workaround to keep the "mirabelle.pl" script happy *) -structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/Tools/mirabelle_try0.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML - Author: Jasmin Blanchette, TU Munich -*) - -structure Mirabelle_Try0 : MIRABELLE_ACTION = -struct - -fun try0_tag id = "#" ^ string_of_int id ^ " try0: " - -fun init _ = I -fun done _ _ = () - -fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre - then log (try0_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) - -end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/etc/settings --- a/src/HOL/Mirabelle/etc/settings Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -MIRABELLE_HOME="$COMPONENT" - -MIRABELLE_LOGIC=HOL -MIRABELLE_THEORY=Main -MIRABELLE_TIMEOUT=30 - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/ex/Ex.thy --- a/src/HOL/Mirabelle/ex/Ex.thy Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -theory Ex imports Pure -begin - -ML \ - val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; if isabelle build -n \"$MIRABELLE_LOGIC\"; then isabelle mirabelle arith Inner_Product.thy; fi"; - if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) - else (); -\ \ \some arbitrary small test case\ - -end - diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,136 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Sascha Boehme -# -# DESCRIPTION: testing tool for automated proof tools - - -PRG="$(basename "$0")" - -function print_action_names() -{ - for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML - do - echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' - done -} - -function print_sledgehammer_options() { - grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ - perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' -} - -function usage() { - # Do not forget to update the Sledgehammer documentation to reflect changes here. - [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" - timeout="$MIRABELLE_TIMEOUT" - echo - echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" - echo - echo " Options are:" - echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" - echo " -O DIR output directory for test data (default $out)" - echo " -S FILE user-provided setup file (no actions required)" - echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" - echo " -d DIR include session directory" - echo " -q be quiet (suppress output of Isabelle process)" - echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo - echo " Apply the given actions at all proof steps in the given theory files." - echo - echo " ACTIONS is a colon-separated list of actions, where each action is" - echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" - print_action_names - echo - echo " Available OPTIONs for the ACTION sledgehammer:" - print_sledgehammer_options - echo - echo " FILES is a list of theory files, where each file is either NAME.thy" - echo " or NAME.thy[START:END] and START and END are numbers indicating the" - echo " range the given actions are to be applied." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -[ $# -eq 0 ] && usage - -MIRABELLE_DIR= -MIRABELLE_SETUP_FILE= - -while getopts "L:T:O:d:t:S:q?" OPT -do - case "$OPT" in - L) - MIRABELLE_LOGIC="$OPTARG" - ;; - T) - MIRABELLE_THEORY="$OPTARG" - ;; - O) - MIRABELLE_OUTPUT_PATH="$OPTARG" - ;; - d) - MIRABELLE_DIR="$OPTARG" - ;; - t) - MIRABELLE_TIMEOUT="$OPTARG" - ;; - S) - MIRABELLE_SETUP_FILE="$OPTARG" - ;; - q) - MIRABELLE_QUIET="true" - ;; - \?) - usage - ;; - esac -done - -export MIRABELLE_DIR -export MIRABELLE_SETUP_FILE -export MIRABELLE_QUIET - -shift $(($OPTIND - 1)) - -export MIRABELLE_ACTIONS="$1" - -shift - - -# setup - -if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then - MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$" - PURGE_OUTPUT="true" -fi - -mkdir -p "$MIRABELLE_OUTPUT_PATH" - -export MIRABELLE_OUTPUT_PATH - - -## main - -for FILE in "$@" -do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." -done - - -## cleanup - -if [ -n "$PURGE_OUTPUT" ]; then - rm -rf "$MIRABELLE_OUTPUT_PATH" -fi diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,182 +0,0 @@ -# -# Author: Jasmin Blanchette and Sascha Boehme -# -# Testing tool for automated proof tools. -# - -use File::Basename; - -# environment - -my $isabelle_home = $ENV{'ISABELLE_HOME'}; -my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; -my $mirabelle_dir = $ENV{'MIRABELLE_DIR'}; -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; -my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; -my $be_quiet = $ENV{'MIRABELLE_QUIET'}; -my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'}; -my $actions = $ENV{'MIRABELLE_ACTIONS'}; - -my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; - - -# argument - -my $thy_file = $ARGV[0]; - -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); -my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10); -my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix; -my $new_thy_file = $path . "/" . $new_thy_name . $ext; - - -# setup - -my $setup_file; -my $setup_full_name; - -if (-e $user_setup_file) { - $setup_file = undef; - my ($name, $path, $ext) = fileparse($user_setup_file, ".thy"); - $setup_full_name = $path . "/" . $name; -} -else { - -my $start_line = "0"; -my $end_line = "~1"; -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { - $thy_file = $1; - $start_line = $2; - $end_line = $3; -} - -my $setup_thy_name = $thy_name . "_Setup"; -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; -my $log_file = $output_path . "/" . $thy_name . ".log"; - -my @action_files; -my @action_names; -foreach (split(/:/, $actions)) { - if (m/([^[]*)/) { - push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; - push @action_names, $1; - } -} -my $tools = ""; -if ($#action_files >= 0) { - # uniquify - my $s = join ("\n", @action_files); - my @action_files = split(/\n/, $s . "\n" . $s); - %action_files = sort(@action_files); - $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files)))); -} - -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; - -print SETUP_FILE < - Config.put_global Mirabelle.timeout $timeout #> - Config.put_global Mirabelle.start_line $start_line #> - Config.put_global Mirabelle.end_line $end_line -*} - -END - -@action_list = split(/:/, $actions); - -foreach (reverse(@action_list)) { - if (m/([^[]*)(?:\[(.*)\])?/) { - my ($name, $settings_str) = ($1, $2 || ""); - $name =~ s/^([a-z])/\U$1/; - print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; - my $sep = ""; - foreach (split(/,/, $settings_str)) { - if (m/\s*([^=]*)\s*=\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"$2\")"; - $sep = ", "; - } - elsif (m/\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"\")"; - $sep = ", "; - } - } - print SETUP_FILE "] *}\n"; - } -} - -print SETUP_FILE "\nend"; -close SETUP_FILE; - -$setup_full_name = $output_path . "/" . $setup_thy_name; - -open(LOG_FILE, ">$log_file"); -print LOG_FILE "Run of $new_thy_file with:\n"; -foreach $action (@action_list) { - print LOG_FILE " $action\n"; -} -close(LOG_FILE); - -} - - -# modify target theory file - -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; -my @lines = ; -close(OLD_FILE); - -my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); - -my $thy_text = join("", @lines); -my $old_len = length($thy_text); -$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; -$thy_text =~ s/\b$thy_name\./$new_thy_name./g; -$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; -die "No 'imports' found" if length($thy_text) == $old_len; - -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; -print NEW_FILE $thy_text; -close(NEW_FILE); - - -# run isabelle - -my $quiet = ""; -my $output_log = 1; -if (defined $be_quiet and $be_quiet ne "") { - $quiet = " > /dev/null 2>&1"; - $output_log = 0; -} - -if ($output_log) { print "Mirabelle: $thy_file\n"; } - -my $cmd = - "isabelle process -o quick_and_dirty -o threads=1" . - " -T \"$path/$new_thy_name\" " . - ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") . - "-l $mirabelle_logic" . $quiet; -my $result = system "bash", "-c", $cmd; - -if ($output_log) { - my $outcome = ($result ? "failure" : "success"); - print "\nFinished: $thy_file [$outcome]\n"; -} - - -# cleanup - -if (defined $setup_file) { - unlink $setup_file; -} -unlink $new_thy_file; - -exit ($result ? 1 : 0); diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/ROOT --- a/src/HOL/ROOT Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/ROOT Tue May 18 20:25:19 2021 +0100 @@ -937,12 +937,13 @@ theories NSPrimes -session "HOL-Mirabelle" in Mirabelle = HOL + - theories Mirabelle_Test - -session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + - options [timeout = 60] - theories Ex +session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + + description "Some arbitrary small test case for Mirabelle." + options [timeout = 60, mirabelle_actions = "arith"] + sessions + "HOL-Analysis" + theories + "HOL-Analysis.Inner_Product" session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Sledgehammer.thy Tue May 18 20:25:19 2021 +0100 @@ -33,5 +33,6 @@ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ +ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Tue May 18 20:25:19 2021 +0100 @@ -8,8 +8,6 @@ imports Complex_Main TPTP_Interpret "HOL-Library.Refute" begin -ML_file \sledgehammer_tactics.ML\ - ML \Proofterm.proofs := 0\ declare [[show_consts]] (* for Refute *) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/TPTP/TPTP_Parser_Example.thy --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Tue May 18 20:25:19 2021 +0100 @@ -8,8 +8,6 @@ imports TPTP_Parser TPTP_Interpret begin -ML_file "sledgehammer_tactics.ML" - import_tptp "$TPTP/Problems/LCL/LCL414+1.p" ML \ diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Tue May 18 20:25:08 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -(* Title: HOL/TPTP/sledgehammer_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2010, 2011 - -Sledgehammer as a tactic. -*) - -signature SLEDGEHAMMER_TACTICS = -sig - type fact_override = Sledgehammer_Fact.fact_override - - val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> - thm list -> int -> tactic - val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> - thm list -> int -> tactic -end; - -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = -struct - -open Sledgehammer_Util -open Sledgehammer_Fact -open Sledgehammer_Prover -open Sledgehammer_Prover_ATP -open Sledgehammer_Prover_Minimize -open Sledgehammer_MaSh -open Sledgehammer_Commands - -fun run_prover override_params fact_override chained i n ctxt goal = - let - val thy = Proof_Context.theory_of ctxt - val mode = Normal - val params as {provers, max_facts, ...} = default_params thy override_params - val name = hd provers - val prover = get_prover ctxt mode name - val default_max_facts = default_max_facts_of_prover ctxt name - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt - val ho_atp = exists (is_ho_atp ctxt) provers - val keywords = Thy_Header.get_keywords' ctxt - val css_table = clasimpset_rule_table_of ctxt - val facts = - nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t - |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override - hyp_ts concl_t - |> hd |> snd - val problem = - {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_proof = I} - in - (case prover params problem of - {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME - | _ => NONE) - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) - end - -fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = - let val override_params = override_params @ [("preplay_timeout", "0")] in - (case run_prover override_params fact_override chained i i ctxt th of - SOME facts => - Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt - (maps (thms_of_name ctxt) facts) i th - | NONE => Seq.empty) - end - -fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = - let - val override_params = - override_params @ - [("preplay_timeout", "0"), - ("minimize", "false")] - val xs = run_prover override_params fact_override chained i i ctxt th - in - if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty - end - -end; diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,252 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius +*) + +signature MIRABELLE = +sig + (*core*) + val print_name: string -> string + val print_properties: Properties.T -> string + type context = + {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} + type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} + val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory + val log_command: command -> XML.body -> XML.tree + val log_report: Properties.T -> XML.body -> XML.tree + val print_exn: exn -> string + val command_action: binding -> (context -> command -> string) -> theory -> theory + + (*utility functions*) + val can_apply : Time.time -> (Proof.context -> int -> tactic) -> + Proof.state -> bool + val theorems_in_proof_term : theory -> thm -> thm list + val theorems_of_sucessful_proof: Toplevel.state -> thm list + val get_argument : (string * string) list -> string * string -> string + val get_int_argument : (string * string) list -> string * int -> int + val get_bool_argument : (string * string) list -> string * bool -> bool + val cpu_time : ('a -> 'b) -> 'a -> 'b * int +end + +structure Mirabelle : MIRABELLE = +struct + +(** Mirabelle core **) + +(* concrete syntax *) + +val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); + +val print_name = Token.print_name keywords; +val print_properties = Token.print_properties keywords; + +fun read_actions str = + Token.read_body keywords + (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) + (Symbol_Pos.explode0 str); + + +(* actions *) + +type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; +type context = + {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; + +structure Data = Theory_Data +( + type T = (context -> command list -> XML.body) Name_Space.table; + val empty = Name_Space.empty_table "mirabelle_action"; + val extend = I; + val merge = Name_Space.merge_tables; +); + +fun theory_action binding action thy = + let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); + in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; + + +(* log content *) + +fun log_action name arguments = + XML.Elem (("action", (Markup.nameN, name) :: arguments), + [XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); + +fun log_command ({name, pos, ...}: command) body = + XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); + +fun log_report props body = + XML.Elem (("report", props), body); + + +(* apply actions *) + +fun apply_action index name arguments timeout commands thy = + let + val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); + val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; + val context = {index = index, tag = tag, arguments = arguments, timeout = timeout, theory = thy}; + val export_body = action context commands; + val export_head = log_action name arguments; + val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); + in + if null export_body then () + else Export.export thy export_name (export_head :: export_body) + end; + +fun print_exn exn = + (case exn of + Timeout.TIMEOUT _ => "timeout" + | ERROR msg => "error: " ^ msg + | exn => "exception:\n" ^ General.exnMessage exn); + +fun command_action binding action = + let + fun apply context command = + let val s = + action context command handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else #tag context ^ print_exn exn; + in + if s = "" then NONE + else SOME (log_command command [XML.Text s]) end; + in theory_action binding (map_filter o apply) end; + + +(* theory line range *) + +local + +val theory_name = + Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) + >> Symbol_Pos.content; + +val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); +val end_line = Symbol_Pos.$$ ":" |-- line; +val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; + +in + +fun read_theory_range str = + (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of + SOME res => res + | NONE => error ("Malformed specification of theory line range: " ^ quote str)); + +end; + +fun check_theories strs = + let + val theories = map read_theory_range strs; + fun get_theory name = + if null theories then SOME NONE + else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; + fun check_line NONE _ = false + | check_line _ NONE = true + | check_line (SOME NONE) _ = true + | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i + | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; + fun check_pos range = check_line range o Position.line_of; + in check_pos o get_theory end; + + +(* presentation hook *) + +val whitelist = ["apply", "by", "proof"]; + +val _ = + Theory.setup (Thy_Info.add_presentation (fn context => fn thy => + let + val {options, adjust_pos, segments, ...} = context; + val mirabelle_timeout = Options.seconds options \<^system_option>\mirabelle_timeout\; + val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; + val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; + + val actions = + (case read_actions mirabelle_actions of + SOME actions => actions + | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); + val check = check_theories (space_explode "," mirabelle_theories); + val commands = + segments |> map_filter (fn {command = tr, prev_state = st, state = st', ...} => + let + val name = Toplevel.name_of tr; + val pos = adjust_pos (Toplevel.pos_of tr); + in + if can (Proof.assert_backward o Toplevel.proof_of) st andalso + member (op =) whitelist name andalso + check (Context.theory_long_name thy) pos + then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} + else NONE + end); + + fun apply (i, (name, arguments)) () = + apply_action (i + 1) name arguments mirabelle_timeout commands thy; + in if null commands then () else fold_index apply actions () end)); + + +(* Mirabelle utility functions *) + +fun can_apply time tac st = + let + val {context = ctxt, facts, goal} = Proof.goal st; + val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); + in + (case try (Timeout.apply time (Seq.pull o full_tac)) goal of + SOME (SOME _) => true + | _ => false) + end; + +local + +fun fold_body_thms f = + let + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => + fn (x, seen) => + if Inttab.defined seen i then (x, seen) + else + let + val name = Proofterm.thm_node_name thm_node; + val prop = Proofterm.thm_node_prop thm_node; + val body = Future.join (Proofterm.thm_node_body thm_node); + val (x', seen') = + app (n + (if name = "" then 0 else 1)) body + (x, Inttab.update (i, ()) seen); + in (x' |> n = 0 ? f (name, prop, body), seen') end); + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; + +in + +fun theorems_in_proof_term thy thm = + let + val all_thms = Global_Theory.all_thms_of thy true; + fun collect (s, _, _) = if s <> "" then insert (op =) s else I; + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; + fun resolve_thms names = map_filter (member_of names) all_thms; + in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; + +end; + +fun theorems_of_sucessful_proof st = + (case try Toplevel.proof_of st of + NONE => [] + | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); + +fun get_argument arguments (key, default) = + the_default default (AList.lookup (op =) arguments key); + +fun get_int_argument arguments (key, default) = + (case Option.map Int.fromString (AList.lookup (op =) arguments key) of + SOME (SOME i) => i + | SOME NONE => error ("bad option: " ^ key) + | NONE => default); + +fun get_bool_argument arguments (key, default) = + (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of + SOME (SOME i) => i + | SOME NONE => error ("bad option: " ^ key) + | NONE => default); + +fun cpu_time f x = + let val ({cpu, ...}, y) = Timing.timing f x + in (y, Time.toMilliseconds cpu) end; + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,273 @@ +/* Title: HOL/Tools/Mirabelle/mirabelle.scala + Author: Makarius + +Isabelle/Scala front-end for Mirabelle. +*/ + +package isabelle.mirabelle + +import isabelle._ + + +object Mirabelle +{ + /* actions and options */ + + def action_names(): List[String] = + { + val Pattern = """Mirabelle action: "(\w+)".*""".r + (for { + file <- + File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, + pred = _.getName.endsWith(".ML")) + line <- split_lines(File.read(file)) + name <- line match { case Pattern(a) => Some(a) case _ => None } + } yield name).sorted + } + + def sledgehammer_options(): List[String] = + { + val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r + split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). + flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) + } + + + /* exported log content */ + + object Log + { + def export_name(index: Int, theory: String = ""): String = + Export.compound_name(theory, "mirabelle/" + index) + + val separator = "\n------------------\n" + + sealed abstract class Entry { def print: String } + + case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry + { + def print: String = "action: " + XML.content(body) + separator + } + case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry + { + def print: String = "\n" + print_head + separator + Pretty.string_of(body) + def print_head: String = + { + val line = Position.Line.get(position) + val offset = Position.Offset.get(position) + val loc = line.toString + ":" + offset.toString + "at " + loc + " (" + name + "):" + } + } + case class Report(result: Properties.T, body: XML.Body) extends Entry + { + override def print: String = "\n" + separator + Pretty.string_of(body) + } + + def entry(export_name: String, xml: XML.Tree): Entry = + xml match { + case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) => + Action(name, props, body) + case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) => + Command(name, props.filter(Markup.position_property), body) + case XML.Elem(Markup("report", props), body) => Report(props, body) + case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml) + } + } + + + /* main mirabelle */ + + def mirabelle( + options: Options, + actions: List[String], + output_dir: Path, + theories: List[String] = Nil, + selection: Sessions.Selection = Sessions.Selection.empty, + progress: Progress = new Progress, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + numa_shuffling: Boolean = false, + max_jobs: Int = 1, + verbose: Boolean = false): Build.Results = + { + require(!selection.requirements) + + progress.echo("Building required heaps ...") + val build_results0 = + Build.build(options, build_heap = true, + selection = selection.copy(requirements = true), progress = progress, dirs = dirs, + select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, + verbose = verbose) + + if (build_results0.ok) { + val build_options = + options + "timeout_build=false" + "parallel_presentation=false" + + ("mirabelle_actions=" + actions.mkString(";")) + + ("mirabelle_theories=" + theories.mkString(",")) + + progress.echo("Running Mirabelle ...") + val build_results = + Build.build(build_options, clean_build = true, + selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) + + if (build_results.ok) { + val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) + val store = Sessions.store(build_options) + + using(store.open_database_context())(db_context => + { + var seen_theories = Set.empty[String] + for { + session <- structure.imports_selection(selection).iterator + session_hierarchy = structure.hierarchy(session) + theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) + theory <- theories + if !seen_theories(theory) + index <- 1 to actions.length + export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index)) + body = export.uncompressed_yxml + if body.nonEmpty + } { + seen_theories += theory + val export_name = Log.export_name(index, theory = theory) + val log = body.map(Log.entry(export_name, _)) + val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) + val log_file = log_dir + Path.basic("mirabelle" + index).log + progress.echo("Writing " + log_file) + File.write(log_file, terminate_lines(log.map(_.print))) + } + }) + } + + build_results + } + else build_results0 + } + + + /* Isabelle tool wrapper */ + + val default_output_dir: Path = Path.explode("mirabelle") + + val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", + Scala_Project.here, args => + { + val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) + + var actions: List[String] = Nil + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var numa_shuffling = false + var output_dir = default_output_dir + var requirements = false + var theories: List[String] = Nil + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var max_jobs = 1 + var options = Options.init(opts = build_options) + var verbose = false + var exclude_sessions: List[String] = Nil + + val default_timeout = options.seconds("mirabelle_timeout") + + val getopts = Getopts(""" +Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] + + Options are: + -A ACTION add to list of actions + -B NAME include session NAME and all descendants + -D DIR include session directory and select its sessions + -N cyclic shuffling of NUMA CPU nodes (performance tuning) + -O DIR output directory for log files (default: """ + default_output_dir + """, + -R refer to requirements of selected sessions + -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -j INT maximum number of parallel jobs (default 1) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -t SECONDS timeout for each action (default """ + default_timeout + """) + -v verbose + -x NAME exclude session NAME and all descendants + + Apply the given actions at all theories and proof steps of the + specified sessions. + + The absence of theory restrictions (option -T) means to check all + theories fully. Otherwise only the named theories are checked. + + Each ACTION is either of the form NAME or NAME [OPTION, ...] + following Isabelle/Isar outer syntax. + + Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ + + For the ACTION "sledgehammer", the following OPTIONs are available:""" + + sledgehammer_options().mkString("\n ", "\n ", "\n"), + "A:" -> (arg => actions = actions ::: List(arg)), + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "N" -> (_ => numa_shuffling = true), + "O:" -> (arg => output_dir = Path.explode(arg)), + "R" -> (_ => requirements = true), + "T:" -> (arg => theories = theories ::: List(arg)), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "o:" -> (arg => options = options + arg), + "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + if (actions.isEmpty) getopts.usage() + + val progress = new Console_Progress(verbose = verbose) + + val start_date = Date.now() + + if (verbose) { + progress.echo("Started at " + Build_Log.print_date(start_date)) + } + + val results = + progress.interrupt_handler { + mirabelle(options, actions, output_dir, + theories = theories, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions), + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), + max_jobs = max_jobs, + verbose = verbose) + } + + val end_date = Date.now() + val elapsed_time = end_date.time - start_date.time + + if (verbose) { + progress.echo("\nFinished at " + Build_Log.print_date(end_date)) + } + + val total_timing = + results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) + + sys.exit(results.rc) + }) +} diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,17 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius + +Mirabelle action: "arith". +*) + +structure Mirabelle_Arith: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\arith\ + (fn {timeout, ...} => fn {pre, ...} => + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre + then "succeeded" else "")); + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,23 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "metis". +*) + +structure Mirabelle_Metis: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\metis\ + (fn {timeout, ...} => fn {pre, post, ...} => + let + val thms = Mirabelle.theorems_of_sucessful_proof post; + val names = map Thm.get_name_hint thms; + val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))); + fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts); + in + (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") + |> not (null names) ? suffix (":\n" ^ commas names) + end)); + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,23 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "quickcheck". +*) + +structure Mirabelle_Quickcheck: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\quickcheck\ + (fn {arguments, timeout, ...} => fn {pre, ...} => + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst; + val quickcheck = + Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1; + in + (case Timeout.apply timeout quickcheck pre of + NONE => "no counterexample" + | SOME _ => "counterexample found") + end)); + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,684 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML + Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich + Author: Makarius + +Mirabelle action: "sledgehammer". +*) + +structure Mirabelle_Sledgehammer: sig end = +struct + +(*To facilitate synching the description of Mirabelle Sledgehammer parameters + (in ../lib/Tools/mirabelle) with the parameters actually used by this + interface, the former extracts PARAMETER and DESCRIPTION from code below which + has this pattern (provided it appears in a single line): + val .*K = "PARAMETER" (*DESCRIPTION*) +*) +(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) + +val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) +val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) +val fact_filterK = "fact_filter" (*=STRING: fact filter*) +val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) +val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) +val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) +val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) +val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) +val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) +val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) +val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) +val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) +val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) +val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) +val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) +val proverK = "prover" (*=STRING: name of the external prover to call*) +val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) +val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) +val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) +val strictK = "strict" (*=BOOL: run in strict mode*) +val strideK = "stride" (*=NUM: run every nth goal*) +val term_orderK = "term_order" (*=STRING: term order (in E)*) +val type_encK = "type_enc" (*=STRING: type encoding scheme*) +val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) + +val separator = "-----" + +(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) +(*defaults used in this Mirabelle action*) +val preplay_timeout_default = "1" +val lam_trans_default = "smart" +val uncurried_aliases_default = "smart" +val fact_filter_default = "smart" +val type_enc_default = "smart" +val strict_default = "false" +val stride_default = 1 +val max_facts_default = "smart" +val slice_default = "true" +val max_calls_default = 10000000 +val check_trivial_default = false + +(*If a key is present in args then augment a list with its pair*) +(*This is used to avoid fixing default values at the Mirabelle level, and + instead use the default values of the tool (Sledgehammer in this case).*) +fun available_parameter args key label list = + let + val value = AList.lookup (op =) args key + in if is_some value then (label, the value) :: list else list end + +datatype sh_data = ShData of { + calls: int, + success: int, + nontriv_calls: int, + nontriv_success: int, + lemmas: int, + max_lems: int, + time_isa: int, + time_prover: int, + time_prover_fail: int} + +datatype re_data = ReData of { + calls: int, + success: int, + nontriv_calls: int, + nontriv_success: int, + proofs: int, + time: int, + timeout: int, + lemmas: int * int * int, + posns: (Position.T * bool) list + } + +fun make_sh_data + (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, + time_prover,time_prover_fail) = + ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, + nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, + time_isa=time_isa, time_prover=time_prover, + time_prover_fail=time_prover_fail} + +fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, + timeout,lemmas,posns) = + ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, + nontriv_success=nontriv_success, proofs=proofs, time=time, + timeout=timeout, lemmas=lemmas, posns=posns} + +val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) +val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) + +fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, + lemmas, max_lems, time_isa, + time_prover, time_prover_fail}) = (calls, success, nontriv_calls, + nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) + +fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, + proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, + nontriv_success, proofs, time, timeout, lemmas, posns) + +datatype data = Data of { + sh: sh_data, + re_u: re_data (* proof method with unminimized set of lemmas *) + } + +type change_data = (data -> data) -> unit + +fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} + +val empty_data = make_data (empty_sh_data, empty_re_data) + +fun map_sh_data f (Data {sh, re_u}) = + let val sh' = make_sh_data (f (tuple_of_sh_data sh)) + in make_data (sh', re_u) end + +fun map_re_data f (Data {sh, re_u}) = + let + val f' = make_re_data o f o tuple_of_re_data + val re_u' = f' re_u + in make_data (sh, re_u') end + +fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); + +val inc_sh_calls = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_success = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_nontriv_calls = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_nontriv_success = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + +fun inc_sh_lemmas n = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) + +fun inc_sh_max_lems n = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) + +fun inc_sh_time_isa t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) + +fun inc_sh_time_prover t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) + +fun inc_sh_time_prover_fail t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) + +val inc_proof_method_calls = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_success = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_nontriv_calls = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_nontriv_success = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_proofs = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) + +fun inc_proof_method_time t = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) + +val inc_proof_method_timeout = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) + +fun inc_proof_method_lemmas n = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) + +fun inc_proof_method_posns pos = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) + +val str0 = string_of_int o the_default 0 + +local + +val str = string_of_int +val str3 = Real.fmt (StringCvt.FIX (SOME 3)) +fun percentage a b = string_of_int (a * 100 div b) +fun ms t = Real.fromInt t / 1000.0 +fun avg_time t n = + if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 + +fun log_sh_data (ShData + {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = + let + val props = + [("sh_calls", str calls), + ("sh_success", str success), + ("sh_nontriv_calls", str nontriv_calls), + ("sh_nontriv_success", str nontriv_success), + ("sh_lemmas", str lemmas), + ("sh_max_lems", str max_lems), + ("sh_time_isa", str3 (ms time_isa)), + ("sh_time_prover", str3 (ms time_prover)), + ("sh_time_prover_fail", str3 (ms time_prover_fail))] + val text = + "\nTotal number of sledgehammer calls: " ^ str calls ^ + "\nNumber of successful sledgehammer calls: " ^ str success ^ + "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ + "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ + "\nSuccess rate: " ^ percentage success calls ^ "%" ^ + "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ + "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ + "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ + "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^ + "\nAverage time for sledgehammer calls (Isabelle): " ^ + str3 (avg_time time_isa calls) ^ + "\nAverage time for successful sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover success) ^ + "\nAverage time for failed sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover_fail (calls - success)) + in (props, text) end + +fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, + nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = + let + val proved = + posns |> map (fn (pos, triv) => + str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ + (if triv then "[T]" else "")) + val props = + [("re_calls", str calls), + ("re_success", str success), + ("re_nontriv_calls", str nontriv_calls), + ("re_nontriv_success", str nontriv_success), + ("re_proofs", str proofs), + ("re_time", str3 (ms time)), + ("re_timeout", str timeout), + ("re_lemmas", str lemmas), + ("re_lems_sos", str lems_sos), + ("re_lems_max", str lems_max), + ("re_proved", space_implode "," proved)] + val text = + "\nTotal number of proof method calls: " ^ str calls ^ + "\nNumber of successful proof method calls: " ^ str success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of proof method timeouts: " ^ str timeout ^ + "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ + "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of successful proof method lemmas: " ^ str lemmas ^ + "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ + "\nMax number of successful proof method lemmas: " ^ str lems_max ^ + "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ + "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ + "\nProved: " ^ space_implode " " proved + in (props, text) end + +in + +fun log_data index (Data {sh, re_u}) = + let + val ShData {calls=sh_calls, ...} = sh + val ReData {calls=re_calls, ...} = re_u + in + if sh_calls > 0 then + let + val (props1, text1) = log_sh_data sh + val (props2, text2) = log_re_data sh_calls re_u + val text = + "\n\nReport #" ^ string_of_int index ^ ":\n" ^ + (if re_calls > 0 then text1 ^ "\n" ^ text2 else text1) + in [Mirabelle.log_report (props1 @ props2) [XML.Text text]] end + else [] + end + +end + +fun get_prover_name thy args = + let + fun default_prover_name () = + hd (#provers (Sledgehammer_Commands.default_params thy [])) + handle List.Empty => error "No ATP available" + in + (case AList.lookup (op =) args proverK of + SOME name => name + | NONE => default_prover_name ()) + end + +fun get_prover ctxt name params goal = + let + val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) + in + Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name + end + +type stature = ATP_Problem_Generate.stature + +fun is_good_line s = + (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) + andalso not (String.isSubstring "(> " s) + andalso not (String.isSubstring ", > " s) + andalso not (String.isSubstring "may fail" s) + +(* Fragile hack *) +fun proof_method_from_msg args msg = + (case AList.lookup (op =) args proof_methodK of + SOME name => + if name = "smart" then + if exists is_good_line (split_lines msg) then + "none" + else + "fail" + else + name + | NONE => + if exists is_good_line (split_lines msg) then + "none" (* trust the preplayed proof *) + else if String.isSubstring "metis (" msg then + msg |> Substring.full + |> Substring.position "metis (" + |> snd |> Substring.position ")" + |> fst |> Substring.string + |> suffix ")" + else if String.isSubstring "metis" msg then + "metis" + else + "smt") + +local + +datatype sh_result = + SH_OK of int * int * (string * stature) list | + SH_FAIL of int * int | + SH_ERROR + +fun run_sh prover_name fact_filter type_enc strict max_facts slice + lam_trans uncurried_aliases e_selection_heuristic term_order force_sos + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = + let + val thy = Proof.theory_of st + val {context = ctxt, facts = chained_ths, goal} = Proof.goal st + val i = 1 + fun set_file_name (SOME dir) = + Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir + #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix + ("prob_" ^ str0 (Position.line_of pos) ^ "__") + #> Config.put SMT_Config.debug_files + (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" + ^ serial_string ()) + | set_file_name NONE = I + val st' = + st + |> Proof.map_context + (set_file_name dir + #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) + e_selection_heuristic |> the_default I) + #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) + term_order |> the_default I) + #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) + force_sos |> the_default I)) + val params as {max_facts, minimize, preplay_timeout, ...} = + Sledgehammer_Commands.default_params thy + ([(* ("verbose", "true"), *) + ("fact_filter", fact_filter), + ("type_enc", type_enc), + ("strict", strict), + ("lam_trans", lam_trans |> the_default lam_trans_default), + ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), + ("max_facts", max_facts), + ("slice", slice), + ("timeout", string_of_int timeout), + ("preplay_timeout", preplay_timeout)] + |> isar_proofsLST + |> smt_proofsLST + |> minimizeLST (*don't confuse the two minimization flags*) + |> max_new_mono_instancesLST + |> max_mono_itersLST) + val default_max_facts = + Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt + val time_limit = + (case hard_timeout of + NONE => I + | SOME secs => Timeout.apply (Time.fromSeconds secs)) + fun failed failure = + ({outcome = SOME failure, used_facts = [], used_from = [], + preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, + message = K ""}, ~1) + val ({outcome, used_facts, preferred_methss, run_time, message, ...} + : Sledgehammer_Prover.prover_result, + time_isa) = time_limit (Mirabelle.cpu_time (fn () => + let + val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name + val keywords = Thy_Header.get_keywords' ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_fact_override keywords css_table chained_ths + hyp_ts concl_t + val factss = + facts + |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name + (the_default default_max_facts max_facts) + Sledgehammer_Fact.no_fact_override hyp_ts concl_t + |> tap (fn factss => + "Line " ^ str0 (Position.line_of pos) ^ ": " ^ + Sledgehammer.string_of_factss factss + |> writeln) + val prover = get_prover ctxt prover_name params goal + val problem = + {comment = "", state = st', goal = goal, subgoal = i, + subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} + in prover params problem end)) () + handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut + | Fail "inappropriate" => failed ATP_Proof.Inappropriate + val time_prover = run_time |> Time.toMilliseconds + val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts + st' i preferred_methss) + in + (case outcome of + NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) + | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) + end + handle ERROR msg => ("error: " ^ msg, SH_ERROR) + +in + +fun run_sledgehammer change_data trivial args proof_method named_thms pos st = + let + val thy = Proof.theory_of st + val triv_str = if trivial then "[T] " else "" + val _ = change_data inc_sh_calls + val _ = if trivial then () else change_data inc_sh_nontriv_calls + val prover_name = get_prover_name thy args + val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default + val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default + val strict = AList.lookup (op =) args strictK |> the_default strict_default + val max_facts = + (case AList.lookup (op =) args max_factsK of + SOME max => max + | NONE => + (case AList.lookup (op =) args max_relevantK of + SOME max => max + | NONE => max_facts_default)) + val slice = AList.lookup (op =) args sliceK |> the_default slice_default + val lam_trans = AList.lookup (op =) args lam_transK + val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK + val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK + val term_order = AList.lookup (op =) args term_orderK + val force_sos = AList.lookup (op =) args force_sosK + |> Option.map (curry (op <>) "false") + val dir = AList.lookup (op =) args keepK + val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30) + (* always use a hard timeout, but give some slack so that the automatic + minimizer has a chance to do its magic *) + val preplay_timeout = AList.lookup (op =) args preplay_timeoutK + |> the_default preplay_timeout_default + val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" + val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" + val minimizeLST = available_parameter args minimizeK "minimize" + val max_new_mono_instancesLST = + available_parameter args max_new_mono_instancesK max_new_mono_instancesK + val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK + val hard_timeout = SOME (4 * timeout) + val (msg, result) = + run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans + uncurried_aliases e_selection_heuristic term_order force_sos + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st + in + (case result of + SH_OK (time_isa, time_prover, names) => + let + fun get_thms (name, stature) = + try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) + name + |> Option.map (pair (name, stature)) + in + change_data inc_sh_success; + if trivial then () else change_data inc_sh_nontriv_success; + change_data (inc_sh_lemmas (length names)); + change_data (inc_sh_max_lems (length names)); + change_data (inc_sh_time_isa time_isa); + change_data (inc_sh_time_prover time_prover); + proof_method := proof_method_from_msg args msg; + named_thms := SOME (map_filter get_thms names); + triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ + string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg + end + | SH_FAIL (time_isa, time_prover) => + let + val _ = change_data (inc_sh_time_isa time_isa) + val _ = change_data (inc_sh_time_prover_fail time_prover) + in triv_str ^ "failed: " ^ msg end + | SH_ERROR => "failed: " ^ msg) + end + +end + +fun override_params prover type_enc timeout = + [("provers", prover), + ("max_facts", "0"), + ("type_enc", type_enc), + ("strict", "true"), + ("slice", "false"), + ("timeout", timeout |> Time.toSeconds |> string_of_int)] + +fun run_proof_method change_data trivial full name meth named_thms timeout pos st = + let + fun do_method named_thms ctxt = + let + val ref_of_str = (* FIXME proper wrapper for parser combinators *) + suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none + #> Parse.thm #> fst + val thms = named_thms |> maps snd + val facts = named_thms |> map (ref_of_str o fst o fst) + val fact_override = {add = facts, del = [], only = true} + fun my_timeout time_slice = + timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal + fun sledge_tac time_slice prover type_enc = + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (override_params prover type_enc (my_timeout time_slice)) fact_override [] + in + if !meth = "sledgehammer_tac" then + sledge_tac 0.2 ATP_Proof.vampireN "mono_native" + ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" + ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" + ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" + ORELSE' SMT_Solver.smt_tac ctxt thms + else if !meth = "smt" then + SMT_Solver.smt_tac ctxt thms + else if full then + Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] + ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms + else if String.isPrefix "metis (" (!meth) then + let + val (type_encs, lam_trans) = + !meth + |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start + |> filter Token.is_proper |> tl + |> Metis_Tactic.parse_metis_options |> fst + |>> the_default [ATP_Proof_Reconstruct.partial_typesN] + ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans + in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end + else if !meth = "metis" then + Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms + else if !meth = "none" then + K all_tac + else if !meth = "fail" then + K no_tac + else + (warning ("Unknown method " ^ quote (!meth)); K no_tac) + end + fun apply_method named_thms = + Mirabelle.can_apply timeout (do_method named_thms) st + + fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" + | with_time (true, t) = (change_data inc_proof_method_success; + if trivial then () + else change_data inc_proof_method_nontriv_success; + change_data (inc_proof_method_lemmas (length named_thms)); + change_data (inc_proof_method_time t); + change_data (inc_proof_method_posns (pos, trivial)); + if name = "proof" then change_data inc_proof_method_proofs else (); + "succeeded (" ^ string_of_int t ^ ")") + fun timed_method named_thms = + with_time (Mirabelle.cpu_time apply_method named_thms) + handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout") + | ERROR msg => ("error: " ^ msg) + + val _ = change_data inc_proof_method_calls + val _ = if trivial then () else change_data inc_proof_method_nontriv_calls + in timed_method named_thms end + +val try_timeout = seconds 5.0 + +fun catch e = + e () handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else Mirabelle.print_exn exn + +(* crude hack *) +val num_sledgehammer_calls = Unsynchronized.ref 0 +val remaining_stride = Unsynchronized.ref stride_default + +val _ = + Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer\ + (fn context => fn commands => + let + val {index, tag = sh_tag, arguments = args, timeout, ...} = context + fun proof_method_tag meth = "#" ^ string_of_int index ^ " " ^ meth ^ " (sledgehammer): " + + val data = Unsynchronized.ref empty_data + val change_data = Unsynchronized.change data + + val stride = Mirabelle.get_int_argument args (strideK, stride_default) + val max_calls = Mirabelle.get_int_argument args (max_callsK, max_calls_default) + val check_trivial = Mirabelle.get_bool_argument args (check_trivialK, check_trivial_default) + + val results = + commands |> maps (fn command => + let + val {name, pos, pre = st, ...} = command + val goal = Thm.major_prem_of (#goal (Proof.goal st)) + val log = + if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then [] + else if !remaining_stride > 1 then + (* We still have some steps to do *) + (Unsynchronized.dec remaining_stride; ["Skipping because of stride"]) + else + (* This was the last step, now run the action *) + let + val _ = remaining_stride := stride + val _ = Unsynchronized.inc num_sledgehammer_calls + in + if !num_sledgehammer_calls > max_calls then + ["Skipping because max number of calls reached"] + else + let + val meth = Unsynchronized.ref "" + val named_thms = + Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) + val trivial = + if check_trivial then + Try0.try0 (SOME try_timeout) ([], [], [], []) st + handle Timeout.TIMEOUT _ => false + else false + val log1 = + sh_tag ^ catch (fn () => + run_sledgehammer change_data trivial args meth named_thms pos st) + val log2 = + (case ! named_thms of + SOME thms => + [separator, + proof_method_tag (!meth) ^ + catch (fn () => + run_proof_method change_data trivial false name meth thms + timeout pos st)] + | NONE => []) + in log1 :: log2 end + end + in + if null log then [] + else [Mirabelle.log_command command [XML.Text (cat_lines log)]] + end) + + val report = log_data index (! data) + in results @ report end)) + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,183 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML + Author: Jasmin Blanchette, TU Munich + Author: Makarius + +Mirabelle action: "sledgehammer_filter". +*) + +structure Mirabelle_Sledgehammer_Filter: sig end = +struct + +fun get args name default_value = + case AList.lookup (op =) args name of + SOME value => Value.parse_real value + | NONE => default_value + +fun extract_relevance_fudge args + {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, + abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight, + chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus, + chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} = + {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier, + worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, + higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight, + abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, + abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, + theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight, + theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight, + chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight, + intro_bonus = get args "intro_bonus" intro_bonus, + elim_bonus = get args "elim_bonus" elim_bonus, + simp_bonus = get args "simp_bonus" simp_bonus, + local_bonus = get args "local_bonus" local_bonus, + assum_bonus = get args "assum_bonus" assum_bonus, + chained_bonus = get args "chained_bonus" chained_bonus, + max_imperfect = get args "max_imperfect" max_imperfect, + max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, + threshold_divisor = get args "threshold_divisor" threshold_divisor, + ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} + +structure Prooftab = + Table(type key = int * int val ord = prod_ord int_ord int_ord) + +fun print_int x = Value.print_int (! x) + +fun percentage a b = if b = 0 then "N/A" else Value.print_int (a * 100 div b) +fun percentage_alt a b = percentage a (a + b) + +val default_prover = ATP_Proof.eN (* arbitrary ATP *) + +fun with_index (i, s) = s ^ "@" ^ Value.print_int i + +val proof_fileK = "proof_file" + +val _ = + Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer_filter\ + (fn context => fn commands => + let + val (proof_table, args) = + let + val (pf_args, other_args) = + #arguments context |> List.partition (curry (op =) proof_fileK o fst) + val proof_file = + (case pf_args of + [] => error "No \"proof_file\" specified" + | (_, s) :: _ => s) + fun do_line line = + (case line |> space_explode ":" of + [line_num, offset, proof] => + SOME (apply2 (the o Int.fromString) (line_num, offset), + proof |> space_explode " " |> filter_out (curry (op =) "")) + | _ => NONE) + val proof_table = + File.read (Path.explode proof_file) + |> space_explode "\n" + |> map_filter do_line + |> AList.coalesce (op =) + |> Prooftab.make + in (proof_table, other_args) end + + val num_successes = Unsynchronized.ref 0 + val num_failures = Unsynchronized.ref 0 + val num_found_proofs = Unsynchronized.ref 0 + val num_lost_proofs = Unsynchronized.ref 0 + val num_found_facts = Unsynchronized.ref 0 + val num_lost_facts = Unsynchronized.ref 0 + + val results = + commands |> maps (fn {pos, pre, ...} => + (case (Position.line_of pos, Position.offset_of pos) of + (SOME line_num, SOME offset) => + (case Prooftab.lookup proof_table (line_num, offset) of + SOME proofs => + let + val thy = Proof.theory_of pre + val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre + val prover = AList.lookup (op =) args "prover" |> the_default default_prover + val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args + val default_max_facts = + Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover + val relevance_fudge = + extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge + val subgoal = 1 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt + val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover + val keywords = Thy_Header.get_keywords' ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_fact_override keywords css_table chained_ths + hyp_ts concl_t + |> Sledgehammer_Fact.drop_duplicate_facts + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params + (the_default default_max_facts max_facts) + (SOME relevance_fudge) hyp_ts concl_t + |> map (fst o fst) + val (found_facts, lost_facts) = + flat proofs |> sort_distinct string_ord + |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) + |> List.partition (curry (op <=) 0 o fst) + |>> sort (prod_ord int_ord string_ord) ||> map snd + val found_proofs = filter (forall (member (op =) facts)) proofs + val n = length found_proofs + val log1 = + if n = 0 then + (Unsynchronized.inc num_failures; "Failure") + else + (Unsynchronized.inc num_successes; + Unsynchronized.add num_found_proofs n; + "Success (" ^ Value.print_int n ^ " of " ^ + Value.print_int (length proofs) ^ " proofs)") + val _ = Unsynchronized.add num_lost_proofs (length proofs - n) + val _ = Unsynchronized.add num_found_facts (length found_facts) + val _ = Unsynchronized.add num_lost_facts (length lost_facts) + val log2 = + if null found_facts then [] + else + let + val found_weight = + Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) + / Real.fromInt (length found_facts) + |> Math.sqrt |> Real.ceil + in + ["Found facts (among " ^ Value.print_int (length facts) ^ + ", weight " ^ Value.print_int found_weight ^ "): " ^ + commas (map with_index found_facts)] + end + val log3 = + if null lost_facts then [] + else + ["Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ + commas lost_facts] + in [XML.Text (cat_lines (log1 :: log2 @ log3))] end + | NONE => [XML.Text "No known proof"]) + | _ => [])) + + val report = + if ! num_successes + ! num_failures > 0 then + let + val props = + [("num_successes", print_int num_successes), + ("num_failures", print_int num_failures), + ("num_found_proofs", print_int num_found_proofs), + ("num_lost_proofs", print_int num_lost_proofs), + ("num_found_facts", print_int num_found_facts), + ("num_lost_facts", print_int num_lost_facts)] + val text = + "\nNumber of overall successes: " ^ print_int num_successes ^ + "\nNumber of overall failures: " ^ print_int num_failures ^ + "\nOverall success rate: " ^ + percentage_alt (! num_successes) (! num_failures) ^ "%" ^ + "\nNumber of found proofs: " ^ print_int num_found_proofs ^ + "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ + "\nProof found rate: " ^ + percentage_alt (! num_found_proofs) (! num_lost_proofs) ^ "%" ^ + "\nNumber of found facts: " ^ print_int num_found_facts ^ + "\nNumber of lost facts: " ^ print_int num_lost_facts ^ + "\nFact found rate: " ^ + percentage_alt (! num_found_facts) (! num_lost_facts) ^ "%" + in [Mirabelle.log_report props [XML.Text text]] end + else [] + in results @ report end)) + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,17 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML + Author: Jasmin Blanchette, TU Munich + Author: Makarius + +Mirabelle action: "try0". +*) + +structure Mirabelle_Try0 : sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\try0\ + (fn {timeout, ...} => fn {pre, ...} => + if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre + then "succeeded" else "")); + +end diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue May 18 20:25:19 2021 +0100 @@ -10,6 +10,7 @@ val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params + val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = @@ -353,7 +354,8 @@ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] -val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) @@ -366,7 +368,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" - (Scan.optional Parse.name runN -- parse_params + (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof @@ -374,7 +376,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" - (parse_params >> (fn params => + (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Tue May 18 20:25:19 2021 +0100 @@ -0,0 +1,76 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2010, 2011 + +Sledgehammer as a tactic. +*) + +signature SLEDGEHAMMER_TACTICS = +sig + type fact_override = Sledgehammer_Fact.fact_override + + val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> + thm list -> int -> tactic + val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> + thm list -> int -> tactic +end; + +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = +struct + +open Sledgehammer_Util +open Sledgehammer_Fact +open Sledgehammer_Prover +open Sledgehammer_Prover_ATP +open Sledgehammer_Prover_Minimize +open Sledgehammer_MaSh +open Sledgehammer_Commands + +fun run_prover override_params fact_override chained i n ctxt goal = + let + val thy = Proof_Context.theory_of ctxt + val mode = Normal + val params as {provers, max_facts, ...} = default_params thy override_params + val name = hd provers + val prover = get_prover ctxt mode name + val default_max_facts = default_max_facts_of_prover ctxt name + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt + val ho_atp = exists (is_ho_atp ctxt) provers + val keywords = Thy_Header.get_keywords' ctxt + val css_table = clasimpset_rule_table_of ctxt + val facts = + nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t + |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override + hyp_ts concl_t + |> hd |> snd + val problem = + {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, + factss = [("", facts)], found_proof = I} + in + (case prover params problem of + {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME + | _ => NONE) + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) + end + +fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = + let val override_params = override_params @ [("preplay_timeout", "0")] in + (case run_prover override_params fact_override chained i i ctxt th of + SOME facts => + Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt + (maps (thms_of_name ctxt) facts) i th + | NONE => Seq.empty) + end + +fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = + let + val override_params = + override_params @ + [("preplay_timeout", "0"), + ("minimize", "false")] + val xs = run_prover override_params fact_override chained i i ctxt th + in + if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty + end + +end; diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Tue May 18 20:25:08 2021 +0100 +++ b/src/HOL/Tools/etc/options Tue May 18 20:25:19 2021 +0100 @@ -46,3 +46,15 @@ public option kodkod_max_threads : int = 0 -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" + + +section "Mirabelle" + +option mirabelle_timeout : real = 30 + -- "default timeout for Mirabelle actions" + +option mirabelle_actions : string = "" + -- "Mirabelle actions (outer syntax, separated by semicolons)" + +option mirabelle_theories : string = "" + -- "Mirabelle theories (names with optional line range, separated by commas)" diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Admin/build_release.scala Tue May 18 20:25:19 2021 +0100 @@ -307,7 +307,7 @@ # main -declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) +declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue May 18 20:25:19 2021 +0100 @@ -303,6 +303,16 @@ val remote_builds1: List[List[Remote_Build]] = { List( + List(Remote_Build("Linux A", "i21of4", user = "i21isatest", + proxy_host = "lxbroy10", proxy_user = "i21isatest", + self_update = true, + options = "-m32 -M1x4,2,4" + + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + + " -e ISABELLE_GHC_SETUP=true" + + " -e ISABELLE_MLTON=mlton" + + " -e ISABELLE_SMLNJ=sml" + + " -e ISABELLE_SWIPL=swipl", + args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", @@ -541,7 +551,7 @@ { running.partition(_.is_finished) match { case (Nil, Nil) => - case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running) + case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running) case (_ :: _, remaining) => join(remaining) } } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Concurrent/par_list.ML Tue May 18 20:25:19 2021 +0100 @@ -16,7 +16,7 @@ signature PAR_LIST = sig - val map_name: string -> ('a -> 'b) -> 'a list -> 'b list + val map': {name: string, sequential: bool} -> ('a -> 'b) -> 'a list -> 'b list val map_independent: ('a -> 'b) -> 'a list -> 'b list val map: ('a -> 'b) -> 'a list -> 'b list val get_some: ('a -> 'b option) -> 'a list -> 'b option @@ -28,20 +28,22 @@ structure Par_List: PAR_LIST = struct -fun forked_results name f xs = - if Future.relevant xs - then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs) - else map (Exn.capture f) xs; +fun managed_results {name, sequential} f xs = + if sequential orelse not (Future.relevant xs) then map (Exn.capture f) xs + else + Future.forked_results + {name = if name = "" then "Par_List.map" else name, deps = []} + (map (fn x => fn () => f x) xs); -fun map_name name f xs = Par_Exn.release_first (forked_results name f xs); -fun map f = map_name "Par_List.map" f; +fun map' params f xs = Par_Exn.release_first (managed_results params f xs); +fun map f = map' {name = "", sequential = false} f; fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all; fun get_some f xs = let exception FOUND of 'b; val results = - forked_results "Par_List.get_some" + managed_results {name = "Par_List.get_some", sequential = false} (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs; in (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Concurrent/unsynchronized.ML --- a/src/Pure/Concurrent/unsynchronized.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Concurrent/unsynchronized.ML Tue May 18 20:25:19 2021 +0100 @@ -13,6 +13,7 @@ val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b val inc: int ref -> int val dec: int ref -> int + val add: int ref -> int -> int val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c end; @@ -29,6 +30,7 @@ fun inc i = (i := ! i + (1: int); ! i); fun dec i = (i := ! i - (1: int); ! i); +fun add i n = (i := ! i + (n: int); ! i); fun setmp flag value f x = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/General/mercurial.scala Tue May 18 20:25:19 2021 +0100 @@ -376,7 +376,7 @@ while (repos.importing) { progress.echo("Awaiting remote repository ...") - Time.seconds(0.5).sleep + Time.seconds(0.5).sleep() repos = phabricator.the_repository(repos.phid) } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/General/path.scala --- a/src/Pure/General/path.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/General/path.scala Tue May 18 20:25:19 2021 +0100 @@ -220,6 +220,7 @@ def thy: Path = ext("thy") def tar: Path = ext("tar") def gz: Path = ext("gz") + def log: Path = ext("log") def backup: Path = { diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/General/ssh.scala Tue May 18 20:25:19 2021 +0100 @@ -243,7 +243,7 @@ val exit_status: Future[Int] = Future.thread("ssh_wait") { - while (!channel.isClosed) exec_wait_delay.sleep + while (!channel.isClosed) exec_wait_delay.sleep() channel.getExitStatus } @@ -282,7 +282,7 @@ if (line_buffer.size > 0) line_flush() finished = true } - else exec_wait_delay.sleep + else exec_wait_delay.sleep() } result.toList diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/General/time.scala --- a/src/Pure/General/time.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/General/time.scala Tue May 18 20:25:19 2021 +0100 @@ -65,5 +65,5 @@ def instant: Instant = Instant.ofEpochMilli(ms) - def sleep: Unit = Thread.sleep(ms) + def sleep(): Unit = Thread.sleep(ms) } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Isar/parse.ML Tue May 18 20:25:19 2021 +0100 @@ -61,7 +61,6 @@ val and_list1': 'a context_parser -> 'a list context_parser val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser - val properties: Properties.T parser val name: string parser val name_range: (string * Position.range) parser val name_position: (string * Position.T) parser @@ -259,8 +258,6 @@ fun list1 scan = enum1 "," scan; fun list scan = enum "," scan; -val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")"); - (* names and embedded content *) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue May 18 20:25:19 2021 +0100 @@ -1532,15 +1532,13 @@ fun print_cases_proof ctxt0 ctxt = let - val print_name = Token.print_name (Thy_Header.get_keywords' ctxt); - fun trim_name x = if Name.is_internal x then Name.clean x else "_"; val trim_names = map trim_name #> drop_suffix (equal "_"); fun print_case name xs = (case trim_names xs of - [] => print_name name - | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs')))); + [] => print_name ctxt name + | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs')))); fun is_case x t = x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t); diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Isar/token.ML Tue May 18 20:25:19 2021 +0100 @@ -93,6 +93,7 @@ val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string + val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list @@ -698,13 +699,16 @@ fun explode0 keywords = explode keywords Position.none; -(* print name in parsable form *) +(* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; +fun print_properties keywords = + map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; + (* make *) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue May 18 20:25:19 2021 +0100 @@ -79,7 +79,6 @@ val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b - val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state @@ -88,7 +87,7 @@ val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result - val join_results: result -> (transition * state) list + val join_results: result -> (state * transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; @@ -602,19 +601,6 @@ Position.setmp_thread_data pos f x; -(* post-transition hooks *) - -local - val hooks = - Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); -in - -fun add_hook hook = Synchronized.change hooks (cons hook); -fun get_hooks () = Synchronized.value hooks; - -end; - - (* apply transitions *) local @@ -634,7 +620,6 @@ val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); - val _ = get_hooks () |> List.app (fn f => ignore \<^try>\f tr st st'\); in (st', opt_err') end; end; @@ -693,9 +678,16 @@ Result_List of result list | Result_Future of result future; -fun join_results (Result x) = [x] - | join_results (Result_List xs) = maps join_results xs - | join_results (Result_Future x) = join_results (Future.join x); +fun join_results result = + let + fun add (tr, st') res = + (case res of + [] => [(init_toplevel (), tr, st')] + | (_, _, st) :: _ => (st, tr, st') :: res); + fun acc (Result r) = add r + | acc (Result_List rs) = fold acc rs + | acc (Result_Future x) = acc (Future.join x); + in rev (acc result []) end; local diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/PIDE/document.ML Tue May 18 20:25:19 2021 +0100 @@ -738,13 +738,18 @@ if Options.bool options "editor_presentation" then let val (_, offsets, rev_segments) = - iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => + iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) => (case opt_exec of SOME (eval, _) => let val command_id = Command.eval_command_id eval; val span = the_command_span command_id; + val st = + (case try (#1 o the o the_entry node o the) prev of + NONE => Toplevel.init_toplevel () + | SOME prev_eval => Command.eval_result_state prev_eval); + val exec_id = Command.eval_exec_id eval; val tr = Command.eval_result_command eval; val st' = Command.eval_result_state eval; @@ -753,14 +758,15 @@ val offsets' = offsets |> Inttab.update (command_id, offset) |> Inttab.update (exec_id, offset); - val segments' = (span, tr, st') :: segments; + val segments' = (span, (st, tr, st')) :: segments; in SOME (offset', offsets', segments') end | NONE => NONE)) node (0, Inttab.empty, []); val adjust = Inttab.lookup offsets; val segments = - rev rev_segments |> map (fn (span, tr, st') => - {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); + rev rev_segments |> map (fn (span, (st, tr, st')) => + {span = Command_Span.adjust_offsets adjust span, + prev_state = st, command = tr, state = st'}); val presentation_context: Thy_Info.presentation_context = {options = options, diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/PIDE/prover.scala Tue May 18 20:25:19 2021 +0100 @@ -140,7 +140,7 @@ } catch { case _: IOException => finished = Some(false) } } - Time.seconds(0.05).sleep + Time.seconds(0.05).sleep() } (finished.isEmpty || !finished.get, result.toString.trim) } @@ -181,7 +181,7 @@ var count = 10 while (!process_result.is_finished && count > 0) { - Time.seconds(0.1).sleep + Time.seconds(0.1).sleep() count -= 1 } if (!process_result.is_finished) terminate_process() diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/PIDE/session.scala Tue May 18 20:25:19 2021 +0100 @@ -719,7 +719,7 @@ { val snapshot = this.snapshot() if (snapshot.is_outdated) { - output_delay.sleep + output_delay.sleep() await_stable_snapshot() } else snapshot diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Tue May 18 20:25:19 2021 +0100 @@ -421,10 +421,9 @@ (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t) handle exn as ERROR _ => Exn.Exn exn; + fun par_map xs = Par_List.map' {name = "Syntax_Phases.parse_term", sequential = false} xs; val results' = - if parsed_len > 1 then - (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res) - check results + if parsed_len > 1 then (grouped 10 par_map o apsnd o Exn.maps_res) check results else results; val reports' = fst (hd results'); diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/System/bash.scala Tue May 18 20:25:19 2021 +0100 @@ -122,7 +122,7 @@ Isabelle_System.process_signal(group_pid, signal = s) val running = root_process_alive() || Isabelle_System.process_signal(group_pid) if (running) { - Time.seconds(0.1).sleep + Time.seconds(0.1).sleep() signal(s, count - 1) } else false @@ -210,7 +210,7 @@ yield { Future.thread("bash_watchdog") { while (proc.isAlive) { - time.sleep + time.sleep() if (check(this)) interrupt() } } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/System/isabelle_tool.scala Tue May 18 20:25:19 2021 +0100 @@ -209,6 +209,7 @@ Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, + isabelle.mirabelle.Mirabelle.isabelle_tool, isabelle.vscode.TextMate_Grammar.isabelle_tool, isabelle.vscode.Language_Server.isabelle_tool) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/System/scala.scala Tue May 18 20:25:19 2021 +0100 @@ -69,7 +69,7 @@ case _ => error("Malformed argument: " + quote(seconds)) } val t0 = Time.now() - t.sleep + t.sleep() val t1 = Time.now() (t1 - t0).toString } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Thy/export.scala Tue May 18 20:25:19 2021 +0100 @@ -82,7 +82,8 @@ def message(msg: String, theory_name: String, name: String): String = msg + " " + quote(name) + " for theory " + quote(theory_name) - def compound_name(a: String, b: String): String = a + ":" + b + def compound_name(a: String, b: String): String = + if (a.isEmpty) b else a + ":" + b def empty_entry(theory_name: String, name: String): Entry = Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Thy/sessions.scala Tue May 18 20:25:19 2021 +0100 @@ -502,6 +502,9 @@ def dirs: List[Path] = dir :: directories + def timeout_ignored: Boolean = + !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1) + def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) def document_enabled: Boolean = diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue May 18 20:25:19 2021 +0100 @@ -55,8 +55,14 @@ fun merge data : T = Library.merge (eq_snd op =) data; ); +fun sequential_presentation options = + not (Options.bool options \<^system_option>\parallel_presentation\); + fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); + Par_List.map' + {name = "apply_presentation", sequential = sequential_presentation (#options context)} + (fn (f, _) => f context thy) (Presentation.get thy) + |> ignore; fun add_presentation f = Presentation.map (cons (f, stamp ())); @@ -257,7 +263,9 @@ val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord - |> Par_List.map (fn result => Exn.capture (result_present result) ()); + |> Par_List.map' + {name = "present", sequential = sequential_presentation (Options.default ())} + (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures @@ -311,8 +319,9 @@ fun present () = let - val segments = (spans ~~ maps Toplevel.join_results results) - |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); + val segments = + (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) => + {span = span, prev_state = st, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue May 18 20:25:19 2021 +0100 @@ -10,7 +10,9 @@ val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text list val output_source: Proof.context -> string -> Latex.text list - type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state} + type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state} val present_thy: Options.T -> theory -> segment list -> Latex.text list val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T @@ -357,7 +359,9 @@ in -type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}; +type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state}; fun present_thy options thy (segments: segment list) = let diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Tools/build.scala Tue May 18 20:25:19 2021 +0100 @@ -290,7 +290,7 @@ } def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep } + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() } val numa_nodes = new NUMA.Nodes(numa_shuffling) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Tools/build_job.scala Tue May 18 20:25:19 2021 +0100 @@ -507,9 +507,8 @@ private val timeout_request: Option[Event_Timer.Request] = { - if (info.timeout > Time.zero) - Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) - else None + if (info.timeout_ignored) None + else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } def join: (Process_Result, Option[String]) = diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/Tools/server.scala Tue May 18 20:25:19 2021 +0100 @@ -445,7 +445,7 @@ find(db, name) match { case Some(server_info) => using(server_info.connection())(_.write_message("shutdown")) - while(server_info.active) { Time.seconds(0.05).sleep } + while(server_info.active) { Time.seconds(0.05).sleep() } true case None => false } diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Pure/build-jars --- a/src/Pure/build-jars Tue May 18 20:25:08 2021 +0100 +++ b/src/Pure/build-jars Tue May 18 20:25:19 2021 +0100 @@ -11,6 +11,7 @@ declare -a SOURCES=( src/HOL/SPARK/Tools/spark.scala src/HOL/Tools/ATP/system_on_tptp.scala + src/HOL/Tools/Mirabelle/mirabelle.scala src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Tools/Metis/fix_metis_license --- a/src/Tools/Metis/fix_metis_license Tue May 18 20:25:08 2021 +0100 +++ b/src/Tools/Metis/fix_metis_license Tue May 18 20:25:19 2021 +0100 @@ -1,4 +1,5 @@ #!/usr/bin/env bash +unset CDPATH THIS=$(cd "$(dirname "$0")"; echo $PWD) (cd $THIS; perl -p -i~ -w -e 's/MIT license/BSD License/g' Makefile src/*.s* scripts/mlpp) diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Tools/Metis/make_metis --- a/src/Tools/Metis/make_metis Tue May 18 20:25:08 2021 +0100 +++ b/src/Tools/Metis/make_metis Tue May 18 20:25:19 2021 +0100 @@ -6,6 +6,7 @@ # A few other ad hoc transformations are performed to ensure that the sources # compile within Isabelle on Poly/ML and SML/NJ. +unset CDPATH THIS=$(cd "$(dirname "$0")"; echo $PWD) make -f Makefile.FILES refresh_FILES FILES=$(cat "$THIS/FILES") diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue May 18 20:25:19 2021 +0100 @@ -370,7 +370,7 @@ { val snapshot = this.snapshot() if (snapshot.is_outdated) { - PIDE.options.seconds("editor_output_delay").sleep + PIDE.options.seconds("editor_output_delay").sleep() await_stable_snapshot() } else snapshot diff -r 06aeb9054c07 -r 2e3a60ce5a9f src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Tue May 18 20:25:08 2021 +0100 +++ b/src/Tools/jEdit/src/scala_console.scala Tue May 18 20:25:19 2021 +0100 @@ -36,7 +36,7 @@ if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } - Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output + Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output } override def close(): Unit = flush()