--- a/src/Pure/Admin/build_polyml.scala Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/Admin/build_polyml.scala Fri Nov 01 18:43:37 2019 +0100
@@ -74,6 +74,10 @@
case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
}
+ if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
+ error("""Missing "chrpath" executable on Linux""")
+ }
+
/* bash */
--- a/src/Pure/PIDE/document.scala Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/PIDE/document.scala Fri Nov 01 18:43:37 2019 +0100
@@ -408,6 +408,7 @@
} yield cmd).toList
def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
+ def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse
def topological_order: List[Node.Name] = graph.topological_order
override def toString: String = topological_order.mkString("Nodes(", ",", ")")
--- a/src/Pure/Proof/proof_syntax.ML Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/Proof/proof_syntax.ML Fri Nov 01 18:43:37 2019 +0100
@@ -7,6 +7,7 @@
signature PROOF_SYNTAX =
sig
val add_proof_syntax: theory -> theory
+ val term_of_proof: proof -> term
val proof_of_term: theory -> bool -> term -> Proofterm.proof
val read_term: theory -> bool -> typ -> string -> term
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
@@ -14,6 +15,7 @@
val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
+ val pretty_proof_boxes_of: Proof.context -> bool -> thm -> Pretty.T
end;
structure Proof_Syntax : PROOF_SYNTAX =
@@ -21,7 +23,7 @@
(**** add special syntax for embedding proof terms ****)
-val proofT = Proofterm.proofT;
+val proofT = Type ("Pure.proof", []);
local
@@ -79,7 +81,60 @@
|> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
-(**** translation between proof terms and pure terms ****)
+
+(** proof terms as pure terms **)
+
+(* term_of_proof *)
+
+local
+
+val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
+val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
+val Hypt = Const ("Pure.Hyp", propT --> proofT);
+val Oraclet = Const ("Pure.Oracle", propT --> proofT);
+val MinProoft = Const ("Pure.MinProof", proofT);
+
+fun AppT T prf =
+ Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
+
+fun OfClasst (T, c) =
+ let val U = Term.itselfT T --> propT
+ in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
+
+fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
+ fold AppT (these Ts)
+ (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
+ | term_of _ (PAxm (name, _, Ts)) =
+ fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
+ | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
+ | term_of _ (PBound i) = Bound i
+ | term_of Ts (Abst (s, opT, prf)) =
+ let val T = the_default dummyT opT in
+ Const ("Pure.Abst", (T --> proofT) --> proofT) $
+ Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
+ end
+ | term_of Ts (AbsP (s, t, prf)) =
+ AbsPt $ the_default Term.dummy_prop t $
+ Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
+ | term_of Ts (prf1 %% prf2) =
+ AppPt $ term_of Ts prf1 $ term_of Ts prf2
+ | term_of Ts (prf % opt) =
+ let
+ val t = the_default Term.dummy opt;
+ val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
+ in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
+ | term_of _ (Hyp t) = Hypt $ t
+ | term_of _ (Oracle (_, t, _)) = Oraclet $ t
+ | term_of _ MinProof = MinProoft;
+
+in
+
+val term_of_proof = term_of [];
+
+end;
+
+
+(* proof_of_term *)
fun proof_of_term thy ty =
let
@@ -193,9 +248,33 @@
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
- (Proofterm.term_of_proof prf);
+ (term_of_proof prf);
fun pretty_standard_proof_of ctxt full thm =
pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
+fun pretty_proof_boxes_of ctxt full thm =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val selection =
+ {included = Proofterm.this_id (Thm.derivation_id thm),
+ excluded = is_some o Global_Theory.lookup_thm_id thy}
+ in
+ Proofterm.proof_boxes selection [Thm.proof_of thm]
+ |> map (fn ({serial = i, pos, prop, ...}, proof) =>
+ let
+ val proof' = proof
+ |> full ? Proofterm.reconstruct_proof thy prop
+ |> Proofterm.forall_intr_variables prop;
+ val prop' = prop
+ |> Proofterm.forall_intr_variables_term;
+ val name = Long_Name.append "thm" (string_of_int i);
+ in
+ Pretty.item
+ [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
+ Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
+ end)
+ |> Pretty.chunks
+ end;
+
end;
--- a/src/Pure/Thy/export_theory.ML Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML Fri Nov 01 18:43:37 2019 +0100
@@ -248,18 +248,19 @@
(* theorems and proof terms *)
- val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs};
-
val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
- fun proof_boxes_of thm thm_id =
+ fun proof_boxes thm thm_id =
let
- val dep_boxes =
- thm |> Thm_Deps.proof_boxes (fn thm_id' =>
- if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
- in dep_boxes @ [thm_id] end;
+ val selection =
+ {included = Proofterm.this_id (SOME thm_id),
+ excluded = is_some o lookup_thm_id};
+ val boxes =
+ map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm])
+ handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm]
+ in boxes @ [thm_id] end;
fun expand_name thm_id (header: Proofterm.thm_header) =
if #serial header = #serial thm_id then ""
@@ -279,16 +280,18 @@
let
val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
val thm = clean_thm (Thm.unconstrainT raw_thm);
- val boxes = proof_boxes_of thm thm_id;
+ val boxes = proof_boxes thm thm_id;
val proof0 =
- if export_standard_proofs then
+ if Proofterm.export_standard_enabled () then
Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
else MinProof;
val (prop, SOME proof) =
standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
- val _ = Proofterm.commit_proof proof;
+ val _ =
+ if Proofterm.export_proof_boxes_required thy
+ then Proofterm.export_proof_boxes [proof] else ();
in
(prop, (deps, (boxes, proof))) |>
let
--- a/src/Pure/global_theory.ML Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/global_theory.ML Fri Nov 01 18:43:37 2019 +0100
@@ -288,10 +288,17 @@
fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
fun apply_facts name_flags1 name_flags2 (b, facts) thy =
- if Binding.is_empty b then app_facts facts thy |-> register_proofs
+ if Binding.is_empty b then
+ let
+ val (thms, thy') = app_facts facts thy;
+ val _ =
+ if Proofterm.export_proof_boxes_required thy' then
+ Proofterm.export_proof_boxes (map Thm.proof_of thms)
+ else ();
+ in register_proofs thms thy' end
else
let
- val name_pos= bind_name thy b;
+ val name_pos = bind_name thy b;
val (thms', thy') = thy
|> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
|>> name_thms name_flags2 name_pos |-> register_proofs;
--- a/src/Pure/proofterm.ML Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/proofterm.ML Fri Nov 01 18:43:37 2019 +0100
@@ -31,6 +31,7 @@
proof: proof}
type oracle = string * term option
type thm = serial * thm_node
+ exception MIN_PROOF of unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
@@ -102,8 +103,6 @@
val prf_subst_bounds: term list -> proof -> proof
val prf_subst_pbounds: proof list -> proof -> proof
val freeze_thaw_prf: proof -> proof * (proof -> proof)
- val proofT: typ
- val term_of_proof: proof -> term
(*proof terms for specific inference rules*)
val trivial_proof: proof
@@ -152,6 +151,8 @@
val add_prf_rrule: proof * proof -> theory -> theory
val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
val set_preproc: (theory -> proof -> proof) -> theory -> theory
+ val forall_intr_variables_term: term -> term
+ val forall_intr_variables: term -> proof -> proof
val no_skel: proof
val normal_skel: proof
val rewrite_proof: theory -> (proof * proof) list *
@@ -172,8 +173,10 @@
val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
val export_enabled: unit -> bool
+ val export_standard_enabled: unit -> bool
+ val export_proof_boxes_required: theory -> bool
+ val export_proof_boxes: proof list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
- val commit_proof: proof -> unit
val thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> string * Position.T -> sort list ->
term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
@@ -188,6 +191,9 @@
val thm_header_id: thm_header -> thm_id
val thm_id: thm -> thm_id
val get_id: sort list -> term list -> term -> proof -> thm_id option
+ val this_id: thm_id option -> thm_id -> bool
+ val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
+ proof list -> (thm_header * proof) list (*exception MIN_PROOF*)
end
structure Proofterm : PROOFTERM =
@@ -228,6 +234,8 @@
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
+exception MIN_PROOF of unit;
+
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -827,58 +835,6 @@
-(** proof terms as pure terms **)
-
-val proofT = Type ("Pure.proof", []);
-
-local
-
-val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
-val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
-val Hypt = Const ("Pure.Hyp", propT --> proofT);
-val Oraclet = Const ("Pure.Oracle", propT --> proofT);
-val MinProoft = Const ("Pure.MinProof", proofT);
-
-fun AppT T prf =
- Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
-
-fun OfClasst (T, c) =
- let val U = Term.itselfT T --> propT
- in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-
-fun term_of _ (PThm ({name, types = Ts, ...}, _)) =
- fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
- | term_of _ (PAxm (name, _, Ts)) =
- fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
- | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
- | term_of _ (PBound i) = Bound i
- | term_of Ts (Abst (s, opT, prf)) =
- let val T = the_default dummyT opT in
- Const ("Pure.Abst", (T --> proofT) --> proofT) $
- Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
- end
- | term_of Ts (AbsP (s, t, prf)) =
- AbsPt $ the_default Term.dummy_prop t $
- Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
- | term_of Ts (prf1 %% prf2) =
- AppPt $ term_of Ts prf1 $ term_of Ts prf2
- | term_of Ts (prf % opt) =
- let
- val t = the_default Term.dummy opt;
- val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
- in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
- | term_of _ (Hyp t) = Hypt $ t
- | term_of _ (Oracle (_, t, _)) = Oraclet $ t
- | term_of _ MinProof = MinProoft;
-
-in
-
-val term_of_proof = term_of [];
-
-end;
-
-
-
(** inference rules **)
(* trivial implication *)
@@ -1628,12 +1584,10 @@
(** reconstruction of partial proof terms **)
-local
+fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop;
+fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
-exception MIN_PROOF of unit;
-
-fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
-fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
+local
fun app_types shift prop Ts prf =
let
@@ -1759,7 +1713,7 @@
NONE => fold_map (mk_tvar o Type.sort_of_atyp) prop_types env
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (prop_types ~~ Ts)
- (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
+ (forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
error ("Wrong number of type arguments for " ^ quote (guess_name prf))
in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
@@ -1919,7 +1873,7 @@
in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
fun prop_of_atom prop Ts =
- subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_vfs prop);
+ subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_variables_term prop);
val head_norm = Envir.head_norm Envir.init;
@@ -1978,7 +1932,7 @@
val prf1 =
thm_body_proof_open thm_body
|> reconstruct_proof thy prop
- |> forall_intr_vfs_prf prop;
+ |> forall_intr_variables prop;
val (seen1, maxidx1, prf2) = expand_init seen prf1
val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2));
in (seen2, maxidx1, prf2) end
@@ -2136,23 +2090,29 @@
(* PThm nodes *)
fun export_enabled () = Options.default_bool "export_proofs";
+fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
-fun commit_proof proof =
+fun export_proof_boxes_required thy =
+ Context.theory_name thy = Context.PureN orelse
+ (export_enabled () andalso not (export_standard_enabled ()));
+
+fun export_proof_boxes proofs =
let
fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
| export_boxes (Abst (_, _, prf)) = export_boxes prf
| export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
| export_boxes (prf % _) = export_boxes prf
- | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
+ | export_boxes (PThm ({serial = i, ...}, thm_body)) =
(fn boxes =>
if Inttab.defined boxes i then boxes
else
let
- val prf = thm_body_proof_raw thm_body;
- val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
- in export_boxes prf boxes' end)
+ val prf' = thm_body_proof_raw thm_body;
+ val export = thm_body_export_proof thm_body;
+ val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export);
+ in export_boxes prf' boxes' end)
| export_boxes _ = I;
- val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
+ val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest;
in List.app (Lazy.force o #2) boxes end;
local
@@ -2203,7 +2163,7 @@
fun export thy i prop prf =
if export_enabled () then
let
- val _ = commit_proof prf;
+ val _ = export_proof_boxes [prf];
val _ = export_proof thy i prop prf;
in () end
else ();
@@ -2320,6 +2280,33 @@
| SOME {name = "", ...} => NONE
| SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
+fun this_id NONE _ = false
+ | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id';
+
+
+(* proof boxes: intermediate PThm nodes *)
+
+fun proof_boxes {included, excluded} proofs =
+ let
+ fun boxes_of (Abst (_, _, prf)) = boxes_of prf
+ | boxes_of (AbsP (_, _, prf)) = boxes_of prf
+ | boxes_of (prf % _) = boxes_of prf
+ | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
+ | boxes_of (PThm (header as {serial = i, ...}, thm_body)) =
+ (fn boxes =>
+ let val thm_id = thm_header_id header in
+ if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id))
+ then boxes
+ else
+ let
+ val prf' = thm_body_proof_open thm_body;
+ val boxes' = Inttab.update (i, (header, prf')) boxes;
+ in boxes_of prf' boxes' end
+ end)
+ | boxes_of MinProof = raise MIN_PROOF ()
+ | boxes_of _ = I;
+ in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end;
+
end;
structure Basic_Proofterm =
--- a/src/Pure/thm_deps.ML Thu Oct 31 09:02:02 2019 +0000
+++ b/src/Pure/thm_deps.ML Fri Nov 01 18:43:37 2019 +0100
@@ -12,7 +12,8 @@
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
val pretty_thm_deps: theory -> thm list -> Pretty.T
- val proof_boxes: (Proofterm.thm_id -> bool) -> thm -> Proofterm.thm_id list
+ val thm_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} ->
+ thm list -> Proofterm.thm_id list
val unused_thms_cmd: theory list * theory list -> (string * thm) list
end;
@@ -80,18 +81,19 @@
in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
-(* proof boxes: undefined PThm nodes *)
+(* thm boxes: intermediate PThm nodes *)
-fun proof_boxes defined thm =
+fun thm_boxes {included, excluded} thms =
let
fun boxes (i, thm_node) res =
let val thm_id = Proofterm.thm_id (i, thm_node) in
- if defined thm_id orelse Inttab.defined res i then res
+ if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id))
+ then res
else
Inttab.update (i, thm_id) res
|> fold boxes (Proofterm.thm_node_thms thm_node)
end;
- in Inttab.fold_rev (cons o #2) (fold boxes (Thm.thm_deps thm) Inttab.empty) [] end;
+ in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end;
(* unused_thms_cmd *)