# HG changeset patch # User wenzelm # Date 1353353027 -3600 # Node ID 3dec8814917602e123f3e90939206ba96ce8461d # Parent 4319691be975f2a65c06fd1055d9e42b8cb91f6d theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics; diff -r 4319691be975 -r 3dec88149176 NEWS --- a/NEWS Mon Nov 19 18:01:48 2012 +0100 +++ b/NEWS Mon Nov 19 20:23:47 2012 +0100 @@ -6,6 +6,14 @@ *** General *** +* Theorem status about oracles and unfinished/failed future proofs is +no longer printed by default, since it is incompatible with +incremental / parallel checking of the persistent document model. ML +function Thm.peek_status may be used to inspect a snapshot of the +ongoing evaluation process. Note that in batch mode --- notably +isabelle build --- the system ensures that future proofs of all +accessible theorems in the theory context are finished (as before). + * Configuration option show_markup controls direct inlining of markup into the printed representation of formal entities --- notably type and sort constraints. This enables Prover IDE users to retrieve that diff -r 4319691be975 -r 3dec88149176 src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 20:23:47 2012 +0100 @@ -648,6 +648,7 @@ \begin{mldecls} @{index_ML_type thm} \\ @{index_ML proofs: "int Unsynchronized.ref"} \\ + @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\ @{index_ML Thm.transfer: "theory -> thm -> thm"} \\ @{index_ML Thm.assume: "cterm -> thm"} \\ @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\ @@ -670,6 +671,15 @@ \begin{description} + \item @{ML Thm.peek_status}~@{text "thm"} informs about the current + status of the derivation object behind the given theorem. This is a + snapshot of a potentially ongoing (parallel) evaluation of proofs. + The three Boolean values indicate the following: @{verbatim oracle} + if the finished part contains some oracle invocation; @{verbatim + unfinished} if some future proofs are still pending; @{verbatim + failed} if some future proof has failed, rendering the theorem + invalid! + \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification @{text "\a. B"}, where occurrences of the atomic term @{text "a"} in the body proposition @{text "B"} are replaced by bound variables. diff -r 4319691be975 -r 3dec88149176 src/Doc/IsarRef/Proof.thy --- a/src/Doc/IsarRef/Proof.thy Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Doc/IsarRef/Proof.thy Mon Nov 19 20:23:47 2012 +0100 @@ -670,9 +670,9 @@ pretending to solve the pending claim without further ado. This only works in interactive development, or if the @{ML quick_and_dirty} flag is enabled (in ML). Facts emerging from fake - proofs are not the real thing. Internally, each theorem container - is tainted by an oracle invocation, which is indicated as ``@{text - "[!]"}'' in the printed result. + proofs are not the real thing. Internally, the derivation object is + tainted by an oracle invocation, which may be inspected via the + theorem status \cite{isabelle-implementation}. The most important application of @{command "sorry"} is to support experimentation and top-down proof development. diff -r 4319691be975 -r 3dec88149176 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Nov 19 20:23:47 2012 +0100 @@ -963,7 +963,7 @@ val (proved, unproved) = partition_vcs vcs; val _ = Thm.join_proofs (maps (#2 o snd) proved); val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => - exists (#oracle o Thm.status_of) thms) proved + exists (#oracle o Thm.peek_status) thms) proved in (if null unproved then () else (if incomplete then warning else error) diff -r 4319691be975 -r 3dec88149176 src/HOL/ex/Iff_Oracle.thy --- a/src/HOL/ex/Iff_Oracle.thy Mon Nov 19 18:01:48 2012 +0100 +++ b/src/HOL/ex/Iff_Oracle.thy Mon Nov 19 20:23:47 2012 +0100 @@ -34,7 +34,7 @@ ML {* iff_oracle (@{theory}, 2) *} ML {* iff_oracle (@{theory}, 10) *} -ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *} +ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *} text {* These oracle calls had better fail. *} diff -r 4319691be975 -r 3dec88149176 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Nov 19 20:23:47 2012 +0100 @@ -52,7 +52,6 @@ val extern_fact: Proof.context -> string -> xstring val pretty_term_abbrev: Proof.context -> term -> Pretty.T val markup_fact: Proof.context -> string -> Markup.T - val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val read_class: Proof.context -> xstring -> class val read_typ: Proof.context -> string -> typ @@ -343,14 +342,11 @@ fun pretty_fact_name ctxt a = Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"]; -fun pretty_fact_aux ctxt flag ("", ths) = - Display.pretty_thms_aux ctxt flag ths - | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block - [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th] - | pretty_fact_aux ctxt flag (a, ths) = Pretty.block - (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths)); - -fun pretty_fact ctxt = pretty_fact_aux ctxt true; +fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths + | pretty_fact ctxt (a, [th]) = Pretty.block + [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th] + | pretty_fact ctxt (a, ths) = Pretty.block + (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths)); diff -r 4319691be975 -r 3dec88149176 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Pure/Isar/proof_display.ML Mon Nov 19 20:23:47 2012 +0100 @@ -46,10 +46,8 @@ | NONE => Syntax.init_pretty_global thy0); fun pp_thm th = - let - val ctxt = default_context (Thm.theory_of_thm th); - val flags = {quote = true, show_hyps = false, show_status = true}; - in Display.pretty_thm_raw ctxt flags th end; + let val ctxt = default_context (Thm.theory_of_thm th); + in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end; fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T); fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t); @@ -85,7 +83,7 @@ fun pretty_rule ctxt s thm = Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"), - Pretty.fbrk, Display.pretty_thm_aux ctxt false thm]; + Pretty.fbrk, Display.pretty_thm ctxt thm]; val string_of_rule = Pretty.string_of ooo pretty_rule; @@ -138,7 +136,7 @@ fun pretty_facts ctxt = flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o - map (single o Proof_Context.pretty_fact_aux ctxt false); + map (single o Proof_Context.pretty_fact ctxt); in @@ -151,7 +149,7 @@ (Pretty.writeln o Pretty.mark markup) (case facts of [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, - Proof_Context.pretty_fact_aux ctxt false fact]) + Proof_Context.pretty_fact ctxt fact]) | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); diff -r 4319691be975 -r 3dec88149176 src/Pure/display.ML --- a/src/Pure/display.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Pure/display.ML Mon Nov 19 20:23:47 2012 +0100 @@ -18,16 +18,13 @@ signature DISPLAY = sig include BASIC_DISPLAY - val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} -> - thm -> Pretty.T - val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T + val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val pretty_thm_without_context: thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string val string_of_thm_without_context: thm -> string - val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T val pretty_thms: Proof.context -> thm list -> Pretty.T val print_syntax: theory -> unit val pretty_full_theory: bool -> theory -> Pretty.T list @@ -54,20 +51,7 @@ fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; -fun display_status _ false _ = "" - | display_status show_hyps true th = - let - val {oracle = oracle0, unfinished, failed} = Thm.status_of th; - val oracle = oracle0 andalso (not (! quick_and_dirty) orelse show_hyps); - in - if failed then "!!" - else if oracle andalso unfinished then "!?" - else if oracle then "!" - else if unfinished then "?" - else "" - end; - -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th = +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; @@ -82,30 +66,24 @@ val asms = map Thm.term_of (Assumption.all_assms_of ctxt); val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps; - val status = display_status show_hyps show_status th; val hlen = length xshyps + length hyps' + length tpairs; val hsymbs = - if hlen = 0 andalso status = "" then [] + if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ - map (Syntax.pretty_sort ctxt) xshyps @ - (if status = "" then [] else [Pretty.str status]))] - else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; + map (Syntax.pretty_sort ctxt) xshyps)] + else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; -fun pretty_thm_aux ctxt show_status = - pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status}; - -fun pretty_thm ctxt = pretty_thm_aux ctxt true; +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_global thy = - pretty_thm_raw (Syntax.init_pretty_global thy) - {quote = false, show_hyps = false, show_status = true}; + pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; @@ -116,11 +94,8 @@ (* multiple theorems *) -fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th - | pretty_thms_aux ctxt flag ths = - Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths)); - -fun pretty_thms ctxt = pretty_thms_aux ctxt true; +fun pretty_thms ctxt [th] = pretty_thm ctxt th + | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); diff -r 4319691be975 -r 3dec88149176 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Pure/proofterm.ML Mon Nov 19 20:23:47 2012 +0100 @@ -42,7 +42,7 @@ val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a val join_bodies: proof_body list -> unit - val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} + val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} val oracle_ord: oracle * oracle -> order val thm_ord: pthm * pthm -> order @@ -208,7 +208,7 @@ fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies (); -fun status_of bodies = +fun peek_status bodies = let fun status (PBody {oracles, thms, ...}) x = let diff -r 4319691be975 -r 3dec88149176 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Nov 19 18:01:48 2012 +0100 +++ b/src/Pure/thm.ML Mon Nov 19 20:23:47 2012 +0100 @@ -99,7 +99,7 @@ val proof_body_of: thm -> proof_body val proof_of: thm -> proof val join_proofs: thm list -> unit - val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool} + val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool} val future: thm future -> cterm -> thm val derivation_name: thm -> string val name_derivation: string -> thm -> thm @@ -536,12 +536,12 @@ (* derivation status *) -fun status_of (Thm (Deriv {promises, body}, _)) = +fun peek_status (Thm (Deriv {promises, body}, _)) = let val ps = map (Future.peek o snd) promises; val bodies = body :: map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps; - val {oracle, unfinished, failed} = Proofterm.status_of bodies; + val {oracle, unfinished, failed} = Proofterm.peek_status bodies; in {oracle = oracle, unfinished = unfinished orelse exists is_none ps,