1.1 --- a/NEWS Mon Nov 19 18:01:48 2012 +0100
1.2 +++ b/NEWS Mon Nov 19 20:23:47 2012 +0100
1.3 @@ -6,6 +6,14 @@
1.4
1.5 *** General ***
1.6
1.7 +* Theorem status about oracles and unfinished/failed future proofs is
1.8 +no longer printed by default, since it is incompatible with
1.9 +incremental / parallel checking of the persistent document model. ML
1.10 +function Thm.peek_status may be used to inspect a snapshot of the
1.11 +ongoing evaluation process. Note that in batch mode --- notably
1.12 +isabelle build --- the system ensures that future proofs of all
1.13 +accessible theorems in the theory context are finished (as before).
1.14 +
1.15 * Configuration option show_markup controls direct inlining of markup
1.16 into the printed representation of formal entities --- notably type
1.17 and sort constraints. This enables Prover IDE users to retrieve that
2.1 --- a/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 18:01:48 2012 +0100
2.2 +++ b/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 20:23:47 2012 +0100
2.3 @@ -648,6 +648,7 @@
2.4 \begin{mldecls}
2.5 @{index_ML_type thm} \\
2.6 @{index_ML proofs: "int Unsynchronized.ref"} \\
2.7 + @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
2.8 @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
2.9 @{index_ML Thm.assume: "cterm -> thm"} \\
2.10 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
2.11 @@ -670,6 +671,15 @@
2.12
2.13 \begin{description}
2.14
2.15 + \item @{ML Thm.peek_status}~@{text "thm"} informs about the current
2.16 + status of the derivation object behind the given theorem. This is a
2.17 + snapshot of a potentially ongoing (parallel) evaluation of proofs.
2.18 + The three Boolean values indicate the following: @{verbatim oracle}
2.19 + if the finished part contains some oracle invocation; @{verbatim
2.20 + unfinished} if some future proofs are still pending; @{verbatim
2.21 + failed} if some future proof has failed, rendering the theorem
2.22 + invalid!
2.23 +
2.24 \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
2.25 @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
2.26 the body proposition @{text "B"} are replaced by bound variables.
3.1 --- a/src/Doc/IsarRef/Proof.thy Mon Nov 19 18:01:48 2012 +0100
3.2 +++ b/src/Doc/IsarRef/Proof.thy Mon Nov 19 20:23:47 2012 +0100
3.3 @@ -670,9 +670,9 @@
3.4 pretending to solve the pending claim without further ado. This
3.5 only works in interactive development, or if the @{ML
3.6 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
3.7 - proofs are not the real thing. Internally, each theorem container
3.8 - is tainted by an oracle invocation, which is indicated as ``@{text
3.9 - "[!]"}'' in the printed result.
3.10 + proofs are not the real thing. Internally, the derivation object is
3.11 + tainted by an oracle invocation, which may be inspected via the
3.12 + theorem status \cite{isabelle-implementation}.
3.13
3.14 The most important application of @{command "sorry"} is to support
3.15 experimentation and top-down proof development.
4.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Nov 19 18:01:48 2012 +0100
4.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Nov 19 20:23:47 2012 +0100
4.3 @@ -963,7 +963,7 @@
4.4 val (proved, unproved) = partition_vcs vcs;
4.5 val _ = Thm.join_proofs (maps (#2 o snd) proved);
4.6 val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
4.7 - exists (#oracle o Thm.status_of) thms) proved
4.8 + exists (#oracle o Thm.peek_status) thms) proved
4.9 in
4.10 (if null unproved then ()
4.11 else (if incomplete then warning else error)
5.1 --- a/src/HOL/ex/Iff_Oracle.thy Mon Nov 19 18:01:48 2012 +0100
5.2 +++ b/src/HOL/ex/Iff_Oracle.thy Mon Nov 19 20:23:47 2012 +0100
5.3 @@ -34,7 +34,7 @@
5.4
5.5 ML {* iff_oracle (@{theory}, 2) *}
5.6 ML {* iff_oracle (@{theory}, 10) *}
5.7 -ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
5.8 +ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
5.9
5.10 text {* These oracle calls had better fail. *}
5.11
6.1 --- a/src/Pure/Isar/proof_context.ML Mon Nov 19 18:01:48 2012 +0100
6.2 +++ b/src/Pure/Isar/proof_context.ML Mon Nov 19 20:23:47 2012 +0100
6.3 @@ -52,7 +52,6 @@
6.4 val extern_fact: Proof.context -> string -> xstring
6.5 val pretty_term_abbrev: Proof.context -> term -> Pretty.T
6.6 val markup_fact: Proof.context -> string -> Markup.T
6.7 - val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
6.8 val pretty_fact: Proof.context -> string * thm list -> Pretty.T
6.9 val read_class: Proof.context -> xstring -> class
6.10 val read_typ: Proof.context -> string -> typ
6.11 @@ -343,14 +342,11 @@
6.12 fun pretty_fact_name ctxt a =
6.13 Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
6.14
6.15 -fun pretty_fact_aux ctxt flag ("", ths) =
6.16 - Display.pretty_thms_aux ctxt flag ths
6.17 - | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
6.18 - [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
6.19 - | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
6.20 - (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
6.21 -
6.22 -fun pretty_fact ctxt = pretty_fact_aux ctxt true;
6.23 +fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths
6.24 + | pretty_fact ctxt (a, [th]) = Pretty.block
6.25 + [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th]
6.26 + | pretty_fact ctxt (a, ths) = Pretty.block
6.27 + (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths));
6.28
6.29
6.30
7.1 --- a/src/Pure/Isar/proof_display.ML Mon Nov 19 18:01:48 2012 +0100
7.2 +++ b/src/Pure/Isar/proof_display.ML Mon Nov 19 20:23:47 2012 +0100
7.3 @@ -46,10 +46,8 @@
7.4 | NONE => Syntax.init_pretty_global thy0);
7.5
7.6 fun pp_thm th =
7.7 - let
7.8 - val ctxt = default_context (Thm.theory_of_thm th);
7.9 - val flags = {quote = true, show_hyps = false, show_status = true};
7.10 - in Display.pretty_thm_raw ctxt flags th end;
7.11 + let val ctxt = default_context (Thm.theory_of_thm th);
7.12 + in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
7.13
7.14 fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
7.15 fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
7.16 @@ -85,7 +83,7 @@
7.17
7.18 fun pretty_rule ctxt s thm =
7.19 Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
7.20 - Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
7.21 + Pretty.fbrk, Display.pretty_thm ctxt thm];
7.22
7.23 val string_of_rule = Pretty.string_of ooo pretty_rule;
7.24
7.25 @@ -138,7 +136,7 @@
7.26
7.27 fun pretty_facts ctxt =
7.28 flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
7.29 - map (single o Proof_Context.pretty_fact_aux ctxt false);
7.30 + map (single o Proof_Context.pretty_fact ctxt);
7.31
7.32 in
7.33
7.34 @@ -151,7 +149,7 @@
7.35 (Pretty.writeln o Pretty.mark markup)
7.36 (case facts of
7.37 [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
7.38 - Proof_Context.pretty_fact_aux ctxt false fact])
7.39 + Proof_Context.pretty_fact ctxt fact])
7.40 | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
7.41 Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
7.42
8.1 --- a/src/Pure/display.ML Mon Nov 19 18:01:48 2012 +0100
8.2 +++ b/src/Pure/display.ML Mon Nov 19 20:23:47 2012 +0100
8.3 @@ -18,16 +18,13 @@
8.4 signature DISPLAY =
8.5 sig
8.6 include BASIC_DISPLAY
8.7 - val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
8.8 - thm -> Pretty.T
8.9 - val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
8.10 + val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
8.11 val pretty_thm: Proof.context -> thm -> Pretty.T
8.12 val pretty_thm_global: theory -> thm -> Pretty.T
8.13 val pretty_thm_without_context: thm -> Pretty.T
8.14 val string_of_thm: Proof.context -> thm -> string
8.15 val string_of_thm_global: theory -> thm -> string
8.16 val string_of_thm_without_context: thm -> string
8.17 - val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
8.18 val pretty_thms: Proof.context -> thm list -> Pretty.T
8.19 val print_syntax: theory -> unit
8.20 val pretty_full_theory: bool -> theory -> Pretty.T list
8.21 @@ -54,20 +51,7 @@
8.22 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
8.23 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
8.24
8.25 -fun display_status _ false _ = ""
8.26 - | display_status show_hyps true th =
8.27 - let
8.28 - val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
8.29 - val oracle = oracle0 andalso (not (! quick_and_dirty) orelse show_hyps);
8.30 - in
8.31 - if failed then "!!"
8.32 - else if oracle andalso unfinished then "!?"
8.33 - else if oracle then "!"
8.34 - else if unfinished then "?"
8.35 - else ""
8.36 - end;
8.37 -
8.38 -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
8.39 +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
8.40 let
8.41 val show_tags = Config.get ctxt show_tags;
8.42 val show_hyps = Config.get ctxt show_hyps;
8.43 @@ -82,30 +66,24 @@
8.44
8.45 val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
8.46 val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
8.47 - val status = display_status show_hyps show_status th;
8.48
8.49 val hlen = length xshyps + length hyps' + length tpairs;
8.50 val hsymbs =
8.51 - if hlen = 0 andalso status = "" then []
8.52 + if hlen = 0 then []
8.53 else if show_hyps orelse show_hyps' then
8.54 [Pretty.brk 2, Pretty.list "[" "]"
8.55 (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
8.56 - map (Syntax.pretty_sort ctxt) xshyps @
8.57 - (if status = "" then [] else [Pretty.str status]))]
8.58 - else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
8.59 + map (Syntax.pretty_sort ctxt) xshyps)]
8.60 + else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
8.61 val tsymbs =
8.62 if null tags orelse not show_tags then []
8.63 else [Pretty.brk 1, pretty_tags tags];
8.64 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
8.65
8.66 -fun pretty_thm_aux ctxt show_status =
8.67 - pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
8.68 -
8.69 -fun pretty_thm ctxt = pretty_thm_aux ctxt true;
8.70 +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
8.71
8.72 fun pretty_thm_global thy =
8.73 - pretty_thm_raw (Syntax.init_pretty_global thy)
8.74 - {quote = false, show_hyps = false, show_status = true};
8.75 + pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
8.76
8.77 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
8.78
8.79 @@ -116,11 +94,8 @@
8.80
8.81 (* multiple theorems *)
8.82
8.83 -fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
8.84 - | pretty_thms_aux ctxt flag ths =
8.85 - Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
8.86 -
8.87 -fun pretty_thms ctxt = pretty_thms_aux ctxt true;
8.88 +fun pretty_thms ctxt [th] = pretty_thm ctxt th
8.89 + | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
8.90
8.91
8.92
9.1 --- a/src/Pure/proofterm.ML Mon Nov 19 18:01:48 2012 +0100
9.2 +++ b/src/Pure/proofterm.ML Mon Nov 19 20:23:47 2012 +0100
9.3 @@ -42,7 +42,7 @@
9.4 val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
9.5 val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
9.6 val join_bodies: proof_body list -> unit
9.7 - val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
9.8 + val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
9.9
9.10 val oracle_ord: oracle * oracle -> order
9.11 val thm_ord: pthm * pthm -> order
9.12 @@ -208,7 +208,7 @@
9.13
9.14 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
9.15
9.16 -fun status_of bodies =
9.17 +fun peek_status bodies =
9.18 let
9.19 fun status (PBody {oracles, thms, ...}) x =
9.20 let
10.1 --- a/src/Pure/thm.ML Mon Nov 19 18:01:48 2012 +0100
10.2 +++ b/src/Pure/thm.ML Mon Nov 19 20:23:47 2012 +0100
10.3 @@ -99,7 +99,7 @@
10.4 val proof_body_of: thm -> proof_body
10.5 val proof_of: thm -> proof
10.6 val join_proofs: thm list -> unit
10.7 - val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
10.8 + val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
10.9 val future: thm future -> cterm -> thm
10.10 val derivation_name: thm -> string
10.11 val name_derivation: string -> thm -> thm
10.12 @@ -536,12 +536,12 @@
10.13
10.14 (* derivation status *)
10.15
10.16 -fun status_of (Thm (Deriv {promises, body}, _)) =
10.17 +fun peek_status (Thm (Deriv {promises, body}, _)) =
10.18 let
10.19 val ps = map (Future.peek o snd) promises;
10.20 val bodies = body ::
10.21 map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
10.22 - val {oracle, unfinished, failed} = Proofterm.status_of bodies;
10.23 + val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
10.24 in
10.25 {oracle = oracle,
10.26 unfinished = unfinished orelse exists is_none ps,