Re: [isabelle] skip_proofs in Isabelle2012



On Fri, 27 Jul 2012, Gerwin Klein wrote:

The above should work if you include this as well:

 ML "Goal.parallel_proofs := 0;"

Thanks, I can confirm that this works on our side.


I can't say on the spot what is the reason for this behaviour. A bit too many features have accumulated in the system, and everytime I pass by that part of the Isar toplevel, I wonder which combinations of the various flags actually work.

I had a brief look at that code before I wrote the message and gave up, yes :-)

Included is a changeset exported from the Isabelle repository that also happens to work with Isabelle2012. I can't say that it fixes the problem, because skip_proofs has never worked reliably in its history. It produces an invalid Isar toplevel state that makes many tools crash on it.

More substantial reforms are required ...

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked proofs should be all unified to forked proofs.


	Makarius
# HG changeset patch
# User wenzelm
# Date 1343827988 -7200
# Node ID c9344758080d3e01acbd682ad294d5f2742c1efc
# Parent  21c42b095c841d1a7508c143d6b6e98d95dbfa69
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);

diff -r 21c42b095c84 -r c9344758080d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun May 20 11:34:33 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 01 15:33:08 2012 +0200
@@ -672,31 +672,34 @@
 );
 
 fun proof_result immediate (tr, proof_trs) st =
-  if immediate orelse null proof_trs
-  then fold_map command_result (tr :: proof_trs) st |>> Future.value
-  else
-    let
-      val st' = command tr st;
-      val (body_trs, end_tr) = split_last proof_trs;
-      val finish = Context.Theory o Proof_Context.theory_of;
+  let val st' = command tr st in
+    if immediate orelse null proof_trs orelse not (can proof_of st')
+    then
+      let val (results, st'') = fold_map command_result proof_trs st'
+      in (Future.value ((tr, st') :: results), st'') end
+    else
+      let
+        val (body_trs, end_tr) = split_last proof_trs;
+        val finish = Context.Theory o Proof_Context.theory_of;
 
-      val future_proof = Proof.global_future_proof
-        (fn prf =>
-          Goal.fork_name "Toplevel.future_proof"
-            (fn () =>
-              let val (result, result_state) =
-                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
-                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                |> fold_map command_result body_trs ||> command end_tr;
-              in (result, presentation_context_of result_state) end))
-        #-> Result.put;
+        val future_proof = Proof.global_future_proof
+          (fn prf =>
+            Goal.fork_name "Toplevel.future_proof"
+              (fn () =>
+                let val (result, result_state) =
+                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
+                  |> fold_map command_result body_trs ||> command end_tr;
+                in (result, presentation_context_of result_state) end))
+          #-> Result.put;
 
-      val st'' = st'
-        |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
-      val result =
-        Result.get (presentation_context_of st'')
-        |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
+        val st'' = st'
+          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+        val result =
+          Result.get (presentation_context_of st'')
+          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
 
-    in (result, st'') end;
+      in (result, st'') end
+  end;
 
 end;


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.