--- a/Admin/components/components.sha1 Sat Sep 23 18:45:19 2023 +0100
+++ b/Admin/components/components.sha1 Sat Sep 23 18:45:28 2023 +0100
@@ -76,8 +76,8 @@
fffaae24da4d274d34b8dc79a76b478b87ec31dd cygwin-20211007.tar.gz
66e16dccd7b177c086ab53013c1b74d09c1893ad cygwin-20220831.tar.gz
6cd34e30e2e650f239d19725c3d15c206fb3a7cf cygwin-20221002.tar.gz
+fe8c541722f2fd6940f9e9948928b55fbc32d14b cygwin-20230711-1.tar.gz
bc634cae08dea80238a830955894919af995cf06 cygwin-20230711.tar.gz
-fe8c541722f2fd6940f9e9948928b55fbc32d14b cygwin-20230711-1.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -169,6 +169,7 @@
7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
cb9f061ccd7c6f90d00c8aa115aeea8679f3f996 isabelle_setup-20221028.tar.gz
f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz
+d30109fe63cec35c31cee9ffd17ae3a13c1e6a33 isabelle_setup-20230922.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
--- a/Admin/components/main Sat Sep 23 18:45:19 2023 +0100
+++ b/Admin/components/main Sat Sep 23 18:45:28 2023 +0100
@@ -11,7 +11,7 @@
foiltex-2.1.4b
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20230206
+isabelle_setup-20230922
jdk-17.0.7
jedit-20211103
jfreechart-1.5.3
--- a/src/Doc/Classes/document/root.tex Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Doc/Classes/document/root.tex Sat Sep 23 18:45:28 2023 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper,fleqn]{article}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
--- a/src/Doc/Implementation/ML.thy Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Doc/Implementation/ML.thy Sat Sep 23 18:45:28 2023 +0100
@@ -1121,7 +1121,8 @@
text \<open>
These indicate arbitrary system events: both the ML runtime system and the
Isabelle/ML infrastructure signal various exceptional situations by raising
- the special \<^ML>\<open>Exn.Interrupt\<close> exception in user code.
+ special exceptions user code, satisfying the predicate
+ \<^ML>\<open>Exn.is_interrupt\<close>.
This is the one and only way that physical events can intrude an Isabelle/ML
program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.certs Sat Sep 23 18:45:28 2023 +0100
@@ -0,0 +1,236 @@
+35b253bd6d27f6991af73e29ed1030cb74b50ab2 11 0
+unsat
+(assume conjecture0 (not (! (= (! (- c$ b$) :named @p_2) a$) :named @p_1)))
+(assume hypothesis1 (! (= c$ (+ a$ b$)) :named @p_6))
+(step t3 (cl (or @p_1 (! (not (! (<= @p_2 a$) :named @p_5)) :named @p_3) (! (not (! (<= a$ @p_2) :named @p_7)) :named @p_4))) :rule la_disequality)
+(step t4 (cl @p_1 @p_3 @p_4) :rule or :premises (t3))
+(step t5 (cl @p_3 @p_4) :rule resolution :premises (t4 conjecture0))
+(step t6 (cl @p_5 (! (not @p_6) :named @p_8)) :rule la_generic :args (1 (- 1)))
+(step t7 (cl @p_5) :rule resolution :premises (t6 hypothesis1))
+(step t8 (cl @p_4) :rule resolution :premises (t5 t7))
+(step t9 (cl @p_7 @p_8) :rule la_generic :args (1 1))
+(step t10 (cl) :rule resolution :premises (t9 hypothesis1 t8))
+882414839a017a484227974e42bc9854cb971d88 49 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x49 (* (- 1) a$)))
+(let ((?x36 (* (- 1) b$)))
+(let ((?x50 (+ c$ ?x36 ?x49)))
+(let (($x92 (= ?x50 0)))
+(let (($x114 (not $x92)))
+(let ((@x128 (rewrite (= (not true) false))))
+(let (($x55 (>= ?x50 0)))
+(let (($x89 (not $x55)))
+(let (($x51 (<= ?x50 0)))
+(let (($x86 (not $x51)))
+(let (($x101 (or $x92 $x86 $x89)))
+(let (($x57 (and $x51 $x55)))
+(let ((@x59 (monotonicity (rewrite (= (<= (+ c$ ?x36) a$) $x51)) (rewrite (= (<= a$ (+ c$ ?x36)) $x55)) (= (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36))) $x57))))
+(let ((?x29 (- c$ b$)))
+(let (($x32 (<= a$ ?x29)))
+(let (($x31 (<= ?x29 a$)))
+(let (($x33 (and $x31 $x32)))
+(let ((@x39 (rewrite (= ?x29 (+ c$ ?x36)))))
+(let ((@x48 (monotonicity (monotonicity @x39 (= $x31 (<= (+ c$ ?x36) a$))) (monotonicity @x39 (= $x32 (<= a$ (+ c$ ?x36)))) (= $x33 (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36)))))))
+(let ((@x64 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x55)))
+(let ((@x132 (monotonicity (iff-true @x64 (= $x55 true)) (= $x89 (not true)))))
+(let ((@x63 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x51)))
+(let ((@x126 (monotonicity (iff-true @x63 (= $x51 true)) (= $x86 (not true)))))
+(let ((@x137 (monotonicity (trans @x126 @x128 (= $x86 false)) (trans @x132 @x128 (= $x89 false)) (= $x101 (or $x92 false false)))))
+(let ((@x141 (trans @x137 (rewrite (= (or $x92 false false) $x92)) (= $x101 $x92))))
+(let ((?x37 (+ c$ ?x36)))
+(let (($x43 (<= a$ ?x37)))
+(let (($x77 (not $x43)))
+(let (($x40 (<= ?x37 a$)))
+(let (($x74 (not $x40)))
+(let (($x80 (or $x74 $x77)))
+(let (($x71 (= ?x37 a$)))
+(let (($x83 (or $x71 $x80)))
+(let ((@x97 (monotonicity (monotonicity (rewrite (= $x40 $x51)) (= $x74 $x86)) (monotonicity (rewrite (= $x43 $x55)) (= $x77 $x89)) (= $x80 (or $x86 $x89)))))
+(let ((@x100 (monotonicity (rewrite (= $x71 $x92)) @x97 (= $x83 (or $x92 (or $x86 $x89))))))
+(let ((@x105 (trans @x100 (rewrite (= (or $x92 (or $x86 $x89)) $x101)) (= $x83 $x101))))
+(let ((@x79 (monotonicity (monotonicity @x39 (= $x32 $x43)) (= (not $x32) $x77))))
+(let ((@x76 (monotonicity (monotonicity @x39 (= $x31 $x40)) (= (not $x31) $x74))))
+(let ((@x85 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (monotonicity @x76 @x79 (= (or (not $x31) (not $x32)) $x80)) (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x83))))
+(let ((@x107 (trans @x85 @x105 (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x101))))
+(let ((@x108 (mp (asserted (or (= ?x29 a$) (or (not $x31) (not $x32)))) @x107 $x101)))
+(let ((@x146 (monotonicity (iff-true (mp @x108 @x141 $x92) (= $x92 true)) (= $x114 (not true)))))
+(let ((@x113 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (= (not (= ?x29 a$)) (not $x71)))))
+(let ((@x118 (trans @x113 (monotonicity (rewrite (= $x71 $x92)) (= (not $x71) $x114)) (= (not (= ?x29 a$)) $x114))))
+(mp (mp (asserted (not (= ?x29 a$))) @x118 $x114) (trans @x146 @x128 (= $x114 false)) false)))))))))))))))))))))))))))))))))))))))))))))))
+
+f2541774823d4fd4ada0de04dcf1ccc81465be15 38 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x69 (* (- 1) a$)))
+(let ((?x41 (* (- 1) b$)))
+(let ((?x70 (+ c$ ?x41 ?x69)))
+(let (($x78 (>= ?x70 0)))
+(let (($x80 (not $x78)))
+(let (($x71 (<= ?x70 0)))
+(let (($x74 (not $x71)))
+(let (($x83 (= ?x70 0)))
+(let (($x92 (or $x83 $x74 $x80)))
+(let (($x97 (not $x92)))
+(let (($x37 (or (= (- c$ b$) a$) (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))))))
+(let (($x38 (not $x37)))
+(let ((?x42 (+ c$ ?x41)))
+(let (($x54 (<= a$ ?x42)))
+(let (($x57 (not $x54)))
+(let (($x48 (<= ?x42 a$)))
+(let (($x51 (not $x48)))
+(let (($x60 (or $x51 $x57)))
+(let (($x45 (= ?x42 a$)))
+(let (($x63 (or $x45 $x60)))
+(let ((@x88 (monotonicity (monotonicity (rewrite (= $x48 $x71)) (= $x51 $x74)) (monotonicity (rewrite (= $x54 $x78)) (= $x57 $x80)) (= $x60 (or $x74 $x80)))))
+(let ((@x91 (monotonicity (rewrite (= $x45 $x83)) @x88 (= $x63 (or $x83 (or $x74 $x80))))))
+(let ((@x96 (trans @x91 (rewrite (= (or $x83 (or $x74 $x80)) $x92)) (= $x63 $x92))))
+(let (($x61 (= (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))) $x60)))
+(let ((@x44 (rewrite (= (- c$ b$) ?x42))))
+(let ((@x59 (monotonicity (monotonicity @x44 (= (<= a$ (- c$ b$)) $x54)) (= (not (<= a$ (- c$ b$))) $x57))))
+(let ((@x53 (monotonicity (monotonicity @x44 (= (<= (- c$ b$) a$) $x48)) (= (not (<= (- c$ b$) a$)) $x51))))
+(let ((@x65 (monotonicity (monotonicity @x44 (= (= (- c$ b$) a$) $x45)) (monotonicity @x53 @x59 $x61) (= $x37 $x63))))
+(let ((@x101 (trans (monotonicity @x65 (= $x38 (not $x63))) (monotonicity @x96 (= (not $x63) $x97)) (= $x38 $x97))))
+(let ((@x102 (mp (asserted $x38) @x101 $x97)))
+(let ((@x106 (not-or-elim @x102 $x78)))
+(let ((@x104 (not-or-elim @x102 (not $x83))))
+(let ((@x105 (not-or-elim @x102 $x71)))
+(unit-resolution ((_ th-lemma arith triangle-eq) $x92) @x105 @x104 @x106 false))))))))))))))))))))))))))))))))))))
+
+38c94308bfb0b4491339a6c117e29fba807f290a 27 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x41 (* (- 1) c$)))
+(let ((?x42 (+ a$ ?x41 b$)))
+(let (($x43 (<= ?x42 0)))
+(let (($x55 (>= ?x42 0)))
+(let (($x69 (and $x55 $x43)))
+(let (($x72 (not $x69)))
+(let ((@x40 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) (<= a$ (+ c$ (* (- 1) b$)))))))
+(let ((@x47 (trans @x40 (rewrite (= (<= a$ (+ c$ (* (- 1) b$))) $x43)) (= (<= a$ (- c$ b$)) $x43))))
+(let ((@x79 (iff-true (mp (asserted (<= a$ (- c$ b$))) @x47 $x43) (= $x43 true))))
+(let ((@x53 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) (<= (+ c$ (* (- 1) b$)) a$)))))
+(let ((@x58 (trans @x53 (rewrite (= (<= (+ c$ (* (- 1) b$)) a$) $x55)) (= (<= (- c$ b$) a$) $x55))))
+(let ((@x81 (iff-true (mp (asserted (<= (- c$ b$) a$)) @x58 $x55) (= $x55 true))))
+(let ((@x88 (trans (monotonicity @x81 @x79 (= $x69 (and true true))) (rewrite (= (and true true) true)) (= $x69 true))))
+(let ((@x95 (trans (monotonicity @x88 (= $x72 (not true))) (rewrite (= (not true) false)) (= $x72 false))))
+(let (($x61 (not (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))))))
+(let ((?x35 (+ c$ (* (- 1) b$))))
+(let (($x38 (<= a$ ?x35)))
+(let (($x51 (<= ?x35 a$)))
+(let (($x63 (and $x51 $x38)))
+(let ((@x71 (monotonicity (rewrite (= $x51 $x55)) (rewrite (= $x38 $x43)) (= $x63 $x69))))
+(let ((@x65 (monotonicity @x53 @x40 (= (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))) $x63))))
+(let ((@x76 (trans (monotonicity @x65 (= $x61 (not $x63))) (monotonicity @x71 (= (not $x63) $x72)) (= $x61 $x72))))
+(mp (mp (asserted $x61) @x76 $x72) @x95 false)))))))))))))))))))))))))
+
+d40f5f06cb71bf04976dfbd768e98729d8a02410 29 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x36 (* (- 1) c$)))
+(let ((?x37 (+ a$ b$ ?x36)))
+(let (($x56 (<= ?x37 0)))
+(let (($x38 (= ?x37 0)))
+(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
+(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
+(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
+(let ((@x96 (trans (monotonicity @x89 (= (or $x56 (not $x38)) (or $x56 false))) (rewrite (= (or $x56 false) $x56)) (= (or $x56 (not $x38)) $x56))))
+(let (($x61 (not $x38)))
+(let (($x64 (or $x56 $x61)))
+(let (($x43 (not (= c$ (+ a$ b$)))))
+(let (($x34 (<= a$ (- c$ b$))))
+(let (($x44 (or $x34 $x43)))
+(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
+(let ((@x66 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) @x63 (= (or (<= a$ (+ (* (- 1) b$) c$)) $x43) $x64))))
+(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= a$ (+ (* (- 1) b$) c$))))))
+(let ((@x55 (monotonicity @x52 (= $x44 (or (<= a$ (+ (* (- 1) b$) c$)) $x43)))))
+(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x56)))
+(let ((@x101 (monotonicity (iff-true @x97 (= $x56 true)) (= (not $x56) (not true)))))
+(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x56) false))))
+(let (($x75 (not $x56)))
+(let ((@x77 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) (= (not (<= a$ (+ (* (- 1) b$) c$))) $x75))))
+(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= a$ (+ (* (- 1) b$) c$)))))))
+(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
+(mp @x80 @x103 false)))))))))))))))))))))))))))
+
+589302410c98bf9494c2b8bba0d198d5d6fb8f30 22 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x58 (= (+ a$ (* (- 1) c$) b$) 0)))
+(let (($x66 (not (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58)))))
+(let (($x36 (not (or (<= a$ (- c$ b$)) (not (= c$ (+ a$ b$)))))))
+(let (($x34 (not (= c$ (+ a$ b$)))))
+(let (($x43 (<= a$ (+ c$ (* (- 1) b$)))))
+(let (($x46 (or $x43 $x34)))
+(let ((@x62 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x58)) (= $x34 (not $x58)))))
+(let ((@x65 (monotonicity (rewrite (= $x43 (<= (+ a$ (* (- 1) c$) b$) 0))) @x62 (= $x46 (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58))))))
+(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) $x43))))
+(let ((@x51 (monotonicity (monotonicity @x45 (= (or (<= a$ (- c$ b$)) $x34) $x46)) (= $x36 (not $x46)))))
+(let ((@x70 (trans @x51 (monotonicity @x65 (= (not $x46) $x66)) (= $x36 $x66))))
+(let ((@x75 (monotonicity (not-or-elim (mp (asserted $x36) @x70 $x66) $x58) (= (<= (+ a$ (* (- 1) c$) b$) 0) (<= 0 0)))))
+(let ((@x81 (trans @x75 (rewrite (= (<= 0 0) true)) (= (<= (+ a$ (* (- 1) c$) b$) 0) true))))
+(let ((@x84 (monotonicity @x81 (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) (not true)))))
+(let ((@x88 (trans @x84 (rewrite (= (not true) false)) (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) false))))
+(let (($x54 (<= (+ a$ (* (- 1) c$) b$) 0)))
+(let (($x72 (not $x54)))
+(mp (not-or-elim (mp (asserted $x36) @x70 $x66) $x72) @x88 false))))))))))))))))))))
+
+a19eb65c252ea63e4442473afd12fc3c9abc7d26 29 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((?x36 (* (- 1) c$)))
+(let ((?x37 (+ a$ b$ ?x36)))
+(let (($x57 (>= ?x37 0)))
+(let (($x38 (= ?x37 0)))
+(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
+(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
+(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
+(let ((@x96 (trans (monotonicity @x89 (= (or $x57 (not $x38)) (or $x57 false))) (rewrite (= (or $x57 false) $x57)) (= (or $x57 (not $x38)) $x57))))
+(let (($x61 (not $x38)))
+(let (($x64 (or $x57 $x61)))
+(let (($x43 (not (= c$ (+ a$ b$)))))
+(let (($x34 (<= (- c$ b$) a$)))
+(let (($x44 (or $x34 $x43)))
+(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
+(let ((@x66 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) @x63 (= (or (<= (+ (* (- 1) b$) c$) a$) $x43) $x64))))
+(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= (+ (* (- 1) b$) c$) a$)))))
+(let ((@x55 (monotonicity @x52 (= $x44 (or (<= (+ (* (- 1) b$) c$) a$) $x43)))))
+(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x57)))
+(let ((@x101 (monotonicity (iff-true @x97 (= $x57 true)) (= (not $x57) (not true)))))
+(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x57) false))))
+(let (($x75 (not $x57)))
+(let ((@x77 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) (= (not (<= (+ (* (- 1) b$) c$) a$)) $x75))))
+(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= (+ (* (- 1) b$) c$) a$))))))
+(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
+(mp @x80 @x103 false)))))))))))))))))))))))))))
+
+4935c5af5b588fd6e477bea2bed6285c3e17b0c6 23 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x63 (<= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
+(let (($x81 (not $x63)))
+(let (($x66 (= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
+(let (($x75 (not (or $x63 (not $x66)))))
+(let (($x36 (not (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))))))
+(let (($x49 (= c$ (+ b$ a$))))
+(let (($x52 (not $x49)))
+(let (($x43 (<= (+ c$ (* (- 1) b$)) a$)))
+(let (($x55 (or $x43 $x52)))
+(let ((@x74 (monotonicity (rewrite (= $x43 $x63)) (monotonicity (rewrite (= $x49 $x66)) (= $x52 (not $x66))) (= $x55 (or $x63 (not $x66))))))
+(let (($x56 (= (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))) $x55)))
+(let ((@x51 (monotonicity (rewrite (= (+ a$ b$) (+ b$ a$))) (= (= c$ (+ a$ b$)) $x49))))
+(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) $x43))))
+(let ((@x57 (monotonicity @x45 (monotonicity @x51 (= (not (= c$ (+ a$ b$))) $x52)) $x56)))
+(let ((@x79 (trans (monotonicity @x57 (= $x36 (not $x55))) (monotonicity @x74 (= (not $x55) $x75)) (= $x36 $x75))))
+(let ((@x84 (monotonicity (not-or-elim (mp (asserted $x36) @x79 $x75) $x66) (= $x63 (<= 0 0)))))
+(let ((@x90 (trans @x84 (rewrite (= (<= 0 0) true)) (= $x63 true))))
+(let ((@x97 (trans (monotonicity @x90 (= $x81 (not true))) (rewrite (= (not true) false)) (= $x81 false))))
+(mp (not-or-elim (mp (asserted $x36) @x79 $x75) $x81) @x97 false)))))))))))))))))))))
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.thy Sat Sep 23 18:45:28 2023 +0100
@@ -0,0 +1,38 @@
+(* Title: src/HOL/Metis_Example/Sledgehammer_Isar_Proofs.thy
+ Author: Martin Desharnais, MPI-INF Saarbruecken
+
+Tests of proof reconstruction (a.k.a. preplay) in Sledgehammer.
+*)
+theory Sledgehammer_Isar_Proofs
+ imports Main
+begin
+
+external_file \<open>Sledgehammer_Isar_Proofs.certs\<close>
+declare [[smt_certificates = "Sledgehammer_Isar_Proofs.certs"]]
+declare [[smt_read_only_certificates = true]]
+
+sledgehammer_params [verit, isar_proof, minimize = false, slices = 1, compress = 1]
+
+lemma
+ fixes a b c :: int
+ shows "a + b = c \<Longrightarrow> c - b = a"
+ sledgehammer [expect = some_preplayed] ()
+proof -
+ assume a1: "a + b = c"
+ have "c - b \<le> a \<or> c \<noteq> a + b"
+ by force
+ then have f2: "c - b \<le> a"
+ using a1 by force
+ have "a \<le> c - b \<or> c \<noteq> a + b"
+ by force
+ then have "a \<le> c - b"
+ using a1 by force
+ then have f3: "c - b \<le> a \<and> a \<le> c - b"
+ using f2 by fastforce
+ have "c - b = a \<or> \<not> c - b \<le> a \<or> \<not> a \<le> c - b"
+ by auto
+ then show ?thesis
+ using f3 by meson
+qed
+
+end
--- a/src/HOL/ROOT Sat Sep 23 18:45:19 2023 +0100
+++ b/src/HOL/ROOT Sat Sep 23 18:45:28 2023 +0100
@@ -394,9 +394,10 @@
Clausification
Message
Proxies
+ Sets
+ Sledgehammer_Isar_Proofs
Tarski
Trans_Closure
- Sets
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
description "
--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Sep 23 18:45:28 2023 +0100
@@ -1049,7 +1049,7 @@
in
if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
else if rc = 2 then TimedOut js
- else if rc = 130 then raise Exn.Interrupt
+ else if rc = 130 then Isabelle_Thread.interrupt_self ()
else Error (if first_error = "" then "Unknown error" else first_error, js)
end
end
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sat Sep 23 18:45:28 2023 +0100
@@ -102,7 +102,7 @@
NONE
else
let
- val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling
+ val _ = List.app (Isabelle_Thread.interrupt_other o #1) canceling
val canceling' = filter (Isabelle_Thread.is_active o #1) canceling
val state' = make_state manager timeout_heap' active canceling' messages
in SOME (map #2 timeout_threads, state') end
--- a/src/Pure/Concurrent/future.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Concurrent/future.ML Sat Sep 23 18:45:28 2023 +0100
@@ -195,13 +195,13 @@
val running = Task_Queue.cancel (! queue) group;
val _ = running |> List.app (fn thread =>
if Isabelle_Thread.is_self thread then ()
- else Isabelle_Thread.interrupt_unsynchronized thread);
+ else Isabelle_Thread.interrupt_other thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
let
val (groups, threads) = Task_Queue.cancel_all (! queue);
- val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
+ val _ = List.app Isabelle_Thread.interrupt_other threads;
in groups end;
fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -419,7 +419,7 @@
(case Position.id_of pos of
NONE => []
| SOME id => [(Markup.exec_idN, id)])
- in Par_Exn.identify exec_id exn end);
+ in Exn_Properties.identify exec_id exn end);
fun assign_result group result res =
let
@@ -450,7 +450,7 @@
Exn.capture (fn () =>
Thread_Attributes.with_attributes atts (fn _ =>
(Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
- else Exn.interrupt_exn;
+ else Isabelle_Thread.interrupt_exn;
in assign_result group result (identify_result pos res) end;
in (result, job) end;
@@ -645,7 +645,7 @@
let
val group = worker_subgroup ();
val result = Single_Assignment.var "promise" : 'a result;
- fun assign () = assign_result group result Exn.interrupt_exn
+ fun assign () = assign_result group result Isabelle_Thread.interrupt_exn
handle Fail _ => true
| exn =>
if Exn.is_interrupt exn
@@ -665,7 +665,8 @@
val group = Task_Queue.group_of_task task;
val pos = Position.thread_data ();
fun job ok =
- assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
+ assign_result group result
+ (if ok then identify_result pos res else Isabelle_Thread.interrupt_exn);
val _ =
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
let
--- a/src/Pure/Concurrent/isabelle_thread.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sat Sep 23 18:45:28 2023 +0100
@@ -20,7 +20,10 @@
val fork: params -> (unit -> unit) -> T
val is_active: T -> bool
val join: T -> unit
- val interrupt_unsynchronized: T -> unit
+ val interrupt: exn
+ val interrupt_exn: 'a Exn.result
+ val interrupt_self: unit -> 'a
+ val interrupt_other: T -> unit
end;
structure Isabelle_Thread: ISABELLE_THREAD =
@@ -53,14 +56,13 @@
val self_var = Thread_Data.var () : T Thread_Data.var;
in
-fun set_self t = Thread_Data.put self_var (SOME t);
+fun init_self args =
+ let val t = make args in Thread_Data.put self_var (SOME t); t end;
fun self () =
(case Thread_Data.get self_var of
SOME t => t
- | NONE =>
- let val t = make {thread = Thread.Thread.self (), name = "", id = make_id ()}
- in set_self t; t end);
+ | NONE => init_self {thread = Thread.Thread.self (), name = "", id = make_id ()});
fun is_self t = equal (t, self ());
@@ -84,11 +86,14 @@
fun fork (params: params) body =
let
- val name = #name params;
- val id = make_id ();
- fun main () = (set_self (make {thread = Thread.Thread.self (), name = name, id = id}); body ());
- val thread = Thread.Thread.fork (main, attributes params);
- in make {thread = thread, name = name, id = id} end;
+ val self = Single_Assignment.var "self";
+ fun main () =
+ let
+ val t = init_self {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
+ val _ = Single_Assignment.assign self t;
+ in body () end;
+ val _ = Thread.Thread.fork (main, attributes params);
+ in Single_Assignment.await self end;
(* join *)
@@ -100,9 +105,14 @@
do OS.Process.sleep (seconds 0.1);
-(* interrupt *)
+(* interrupts *)
-fun interrupt_unsynchronized t =
+val interrupt = Thread.Thread.Interrupt;
+val interrupt_exn = Exn.Exn interrupt;
+
+fun interrupt_self () = raise interrupt;
+
+fun interrupt_other t =
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
end;
--- a/src/Pure/Concurrent/par_exn.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Sat Sep 23 18:45:28 2023 +0100
@@ -7,8 +7,6 @@
signature PAR_EXN =
sig
- val identify: Properties.T -> exn -> exn
- val the_serial: exn -> int
val make: exn list -> exn
val dest: exn -> exn list option
val is_interrupted: 'a Exn.result list -> bool
@@ -19,37 +17,20 @@
structure Par_Exn: PAR_EXN =
struct
-(* identification via serial numbers -- NOT portable! *)
-
-fun identify default_props exn =
- let
- val props = Exn_Properties.get exn;
- val update_serial =
- if Properties.defined props Markup.serialN then []
- else [(Markup.serialN, serial_string ())];
- val update_props = filter_out (Properties.defined props o #1) default_props;
- in Exn_Properties.update (update_serial @ update_props) exn end;
-
-fun the_serial exn =
- Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
-
-val exn_ord = rev_order o int_ord o apply2 the_serial;
-
-
(* parallel exceptions *)
exception Par_Exn of exn list;
- (*non-empty list with unique identified elements sorted by exn_ord;
- no occurrences of Par_Exn or Exn.Interrupt*)
+ (*non-empty list with unique identified elements sorted by Exn_Properties.ord;
+ no occurrences of Par_Exn or Exn.is_interrupt*)
fun par_exns (Par_Exn exns) = exns
- | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
+ | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn];
fun make exns =
let
val exnss = map par_exns exns;
- val exns' = Ord_List.unions exn_ord exnss handle Option.Option => flat exnss;
- in if null exns' then Exn.Interrupt else Par_Exn exns' end;
+ val exns' = Ord_List.unions Exn_Properties.ord exnss handle Option.Option => flat exnss;
+ in if null exns' then Isabelle_Thread.interrupt else Par_Exn exns' end;
fun dest (Par_Exn exns) = SOME exns
| dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
@@ -58,11 +39,11 @@
(* parallel results *)
fun is_interrupted results =
- exists (fn Exn.Exn _ => true | _ => false) results andalso
+ exists Exn.is_exn results andalso
Exn.is_interrupt (make (map_filter Exn.get_exn results));
fun release_all results =
- if forall (fn Exn.Res _ => true | _ => false) results
+ if forall Exn.is_res results
then map Exn.release results
else raise make (map_filter Exn.get_exn results);
--- a/src/Pure/Concurrent/task_queue.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Sat Sep 23 18:45:28 2023 +0100
@@ -296,7 +296,7 @@
fun cancel (Queue {groups, jobs, ...}) group =
let
- val _ = cancel_group group Exn.Interrupt;
+ val _ = cancel_group group Isabelle_Thread.interrupt;
val running =
Tasks.fold (fn task =>
(case get_job jobs task of Running thread => insert Isabelle_Thread.equal thread | _ => I))
@@ -308,7 +308,7 @@
fun cancel_job (task, (job, _)) (groups, running) =
let
val group = group_of_task task;
- val _ = cancel_group group Exn.Interrupt;
+ val _ = cancel_group group Isabelle_Thread.interrupt;
in
(case job of
Running t => (insert eq_group group groups, insert Isabelle_Thread.equal t running)
--- a/src/Pure/Concurrent/timeout.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Concurrent/timeout.ML Sat Sep 23 18:45:28 2023 +0100
@@ -40,7 +40,7 @@
val request =
Event_Timer.request {physical = physical} (start + scale_time timeout)
- (fn () => Isabelle_Thread.interrupt_unsynchronized self);
+ (fn () => Isabelle_Thread.interrupt_other self);
val result =
Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
--- a/src/Pure/General/exn.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/General/exn.ML Sat Sep 23 18:45:28 2023 +0100
@@ -17,6 +17,8 @@
val polyml_location: exn -> PolyML.location option
val reraise: exn -> 'a
datatype 'a result = Res of 'a | Exn of exn
+ val is_res: 'a result -> bool
+ val is_exn: 'a result -> bool
val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
@@ -24,14 +26,11 @@
val map_res: ('a -> 'b) -> 'a result -> 'b result
val maps_res: ('a -> 'b result) -> 'a result -> 'b result
val map_exn: (exn -> exn) -> 'a result -> 'a result
- exception Interrupt
- val interrupt: unit -> 'a
+ val cause: exn -> exn
val is_interrupt: exn -> bool
- val interrupt_exn: 'a result
val is_interrupt_exn: 'a result -> bool
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
- val return_code: exn -> int -> int
- val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
+ val failure_rc: exn -> int
exception EXCEPTIONS of exn list
val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
end;
@@ -63,6 +62,12 @@
Res of 'a |
Exn of exn;
+fun is_res (Res _) = true
+ | is_res _ = false;
+
+fun is_exn (Exn _) = true
+ | is_exn _ = false;
+
fun get_res (Res x) = SOME x
| get_res _ = NONE;
@@ -85,15 +90,13 @@
(* interrupts *)
-exception Interrupt = Thread.Thread.Interrupt;
-
-fun interrupt () = raise Interrupt;
+fun cause (IO.Io {cause = exn, ...}) = cause exn
+ | cause exn = exn;
-fun is_interrupt Interrupt = true
- | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
- | is_interrupt _ = false;
-
-val interrupt_exn = Exn Interrupt;
+fun is_interrupt exn =
+ (case cause exn of
+ Thread.Thread.Interrupt => true
+ | _ => false);
fun is_interrupt_exn (Exn exn) = is_interrupt exn
| is_interrupt_exn _ = false;
@@ -101,14 +104,7 @@
fun interruptible_capture f x =
Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
-
-(* POSIX return code *)
-
-fun return_code exn rc =
- if is_interrupt exn then 130 else rc;
-
-fun capture_exit rc f x =
- f x handle exn => exit (return_code exn rc);
+fun failure_rc exn = if is_interrupt exn then 130 else 2;
(* concatenated exceptions *)
--- a/src/Pure/General/exn.scala Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/General/exn.scala Sat Sep 23 18:45:28 2023 +0100
@@ -53,6 +53,9 @@
case class Res[A](res: A) extends Result[A]
case class Exn[A](exn: Throwable) extends Result[A]
+ def is_res[A](result: Result[A]): Boolean = result.isInstanceOf[Res[A]]
+ def is_exn[A](result: Result[A]): Boolean = result.isInstanceOf[Exn[A]]
+
def the_res[A]: PartialFunction[Result[A], A] = { case Res(res) => res }
def the_exn[A]: PartialFunction[Result[A], Throwable] = { case Exn(exn) => exn }
@@ -75,6 +78,9 @@
/* interrupts */
+ def cause(exn: Throwable): Throwable =
+ isabelle.setup.Exn.cause(exn)
+
def is_interrupt(exn: Throwable): Boolean =
isabelle.setup.Exn.is_interrupt(exn)
--- a/src/Pure/Isar/runtime.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Isar/runtime.ML Sat Sep 23 18:45:28 2023 +0100
@@ -75,9 +75,9 @@
fun identify exn =
let
- val exn' = Par_Exn.identify [] exn;
+ val exn' = Exn_Properties.identify [] exn;
val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
- val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
+ val i = Exn_Properties.the_serial exn' handle Option.Option => serial ();
in ((i, exn'), exec_id) end;
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
--- a/src/Pure/ML/exn_properties.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/ML/exn_properties.ML Sat Sep 23 18:45:28 2023 +0100
@@ -9,7 +9,9 @@
val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
val position: exn -> Position.T
val get: exn -> Properties.T
- val update: Properties.T -> exn -> exn
+ val identify: Properties.T -> exn -> exn
+ val the_serial: exn -> int
+ val ord: exn ord
end;
structure Exn_Properties: EXN_PROPERTIES =
@@ -46,26 +48,43 @@
| SOME loc => props_of_polyml_location loc);
fun update entries exn =
+ let
+ val loc =
+ the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+ (Exn.polyml_location exn);
+ val props = props_of_polyml_location loc;
+ val props' = fold Properties.put entries props;
+ in
+ if props = props' then exn
+ else
+ let
+ val loc' =
+ {file = YXML.string_of_body (XML.Encode.properties props'),
+ startLine = #startLine loc, endLine = #endLine loc,
+ startPosition = #startPosition loc, endPosition = #endPosition loc};
+ in
+ Thread_Attributes.uninterruptible (fn _ => fn () =>
+ PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
+ end
+ end;
+
+
+(* identification via serial numbers *)
+
+fun identify default_props exn =
if Exn.is_interrupt exn then exn
else
let
- val loc =
- the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
- (Exn.polyml_location exn);
- val props = props_of_polyml_location loc;
- val props' = fold Properties.put entries props;
- in
- if props = props' then exn
- else
- let
- val loc' =
- {file = YXML.string_of_body (XML.Encode.properties props'),
- startLine = #startLine loc, endLine = #endLine loc,
- startPosition = #startPosition loc, endPosition = #endPosition loc};
- in
- Thread_Attributes.uninterruptible (fn _ => fn () =>
- PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
- end
- end;
+ val props = get exn;
+ val update_serial =
+ if Properties.defined props Markup.serialN then []
+ else [(Markup.serialN, serial_string ())];
+ val update_props = filter_out (Properties.defined props o #1) default_props;
+ in update (update_serial @ update_props) exn end;
+
+fun the_serial exn =
+ Value.parse_int (the (Properties.get (get exn) Markup.serialN));
+
+val ord = rev_order o int_ord o apply2 the_serial;
end;
--- a/src/Pure/PIDE/command.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/PIDE/command.ML Sat Sep 23 18:45:28 2023 +0100
@@ -241,7 +241,9 @@
let
val _ = status tr Markup.failed;
val _ = status tr Markup.finished;
- val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
+ val _ =
+ if null errs then (status tr Markup.canceled; Isabelle_Thread.interrupt_self ())
+ else ();
in {failed = true, command = tr, state = st} end
| SOME st' =>
let
--- a/src/Pure/PIDE/command.scala Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/PIDE/command.scala Sat Sep 23 18:45:28 2023 +0100
@@ -497,7 +497,7 @@
def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs
def blobs_index: Int = blobs_info.index
- def blobs_ok: Boolean = blobs.forall(Exn.the_res.isDefinedAt)
+ def blobs_ok: Boolean = blobs.forall(Exn.is_res)
def blobs_names: List[Document.Node.Name] =
for (case Exn.Res(blob) <- blobs) yield blob.name
--- a/src/Pure/ROOT.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/ROOT.ML Sat Sep 23 18:45:28 2023 +0100
@@ -121,8 +121,8 @@
ML_file_no_debug "ML/exn_debugger.ML";
ML_file "Concurrent/thread_data_virtual.ML";
+ML_file "Concurrent/single_assignment.ML";
ML_file "Concurrent/isabelle_thread.ML";
-ML_file "Concurrent/single_assignment.ML";
ML_file "Concurrent/par_exn.ML";
ML_file "Concurrent/task_queue.ML";
--- a/src/Pure/System/command_line.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/System/command_line.ML Sat Sep 23 18:45:28 2023 +0100
@@ -16,8 +16,8 @@
Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val rc =
- (restore_attributes body (); 0)
- handle exn => Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
+ (restore_attributes body (); 0) handle exn =>
+ ((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
in exit rc end) ();
end;
--- a/src/Pure/System/isabelle_system.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/System/isabelle_system.ML Sat Sep 23 18:45:28 2023 +0100
@@ -68,7 +68,7 @@
if head = Bash.server_uuid andalso length args = 1 then
loop (SOME (hd args)) s
else if head = Bash.server_interrupt andalso null args then
- raise Exn.Interrupt
+ Isabelle_Thread.interrupt_self ()
else if head = Bash.server_failure andalso length args = 1 then
raise Fail (hd args)
else if head = Bash.server_result andalso length args >= 4 then
--- a/src/Pure/System/scala.ML Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/System/scala.ML Sat Sep 23 18:45:28 2023 +0100
@@ -35,7 +35,7 @@
| ("1", _) => Exn.Res rest
| ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg))
| ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg))
- | ("4", []) => Exn.Exn Exn.Interrupt
+ | ("4", []) => Isabelle_Thread.interrupt_exn
| _ => raise Fail "Malformed Scala.result");
in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end);
@@ -57,7 +57,7 @@
(case Symtab.lookup tab id of
SOME (Exn.Exn Match) => NONE
| SOME result => SOME (result, Symtab.delete id tab)
- | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
+ | NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
in
invoke ();
Exn.release (restore_attributes await_result ())
--- a/src/Pure/Tools/build_cluster.scala Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala Sat Sep 23 18:45:28 2023 +0100
@@ -258,7 +258,7 @@
capture(host, "open") { host.open_session(build_context, progress = progress) },
remote_hosts, thread = true)
- if (attempts.forall(Exn.the_res.isDefinedAt)) {
+ if (attempts.forall(Exn.is_res)) {
_sessions = attempts.map(Exn.the_res)
_sessions
}
--- a/src/Pure/Tools/build_job.scala Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Sep 23 18:45:28 2023 +0100
@@ -391,7 +391,7 @@
val (document_output, document_errors) =
try {
- if (Exn.the_res.isDefinedAt(build_errors) && result0.ok && info.documents.nonEmpty) {
+ if (Exn.is_res(build_errors) && result0.ok && info.documents.nonEmpty) {
using(Export.open_database_context(store, server = server)) { database_context =>
val documents =
using(database_context.open_session(session_background)) {
--- a/src/Tools/Setup/src/Exn.java Sat Sep 23 18:45:19 2023 +0100
+++ b/src/Tools/Setup/src/Exn.java Sat Sep 23 18:45:28 2023 +0100
@@ -16,15 +16,18 @@
{
/* interrupts */
+ public static Throwable cause(Throwable exn)
+ {
+ Throwable e = exn;
+ while (e != null && e.getCause() != null) {
+ e = e.getCause();
+ }
+ return e;
+ }
+
public static boolean is_interrupt(Throwable exn)
{
- boolean found_interrupt = false;
- Throwable e = exn;
- while (!found_interrupt && e != null) {
- found_interrupt = e instanceof InterruptedException;
- e = e.getCause();
- }
- return found_interrupt;
+ return cause(exn) instanceof InterruptedException;
}
public static int failure_rc(Throwable exn)