*To*: Gerwin Klein <gerwin.klein at nicta.com.au>*Subject*: Re: [isabelle] skip_proofs in Isabelle2012*From*: Makarius <makarius at sketis.net>*Date*: Wed, 1 Aug 2012 16:13:32 +0200 (CEST)*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <C36E6A96-30EF-4D60-8BA1-67385A9F848D@nicta.com.au>*References*: <1DBCF519-87DF-446A-B899-F0D806CAEE26@nicta.com.au> <alpine.LNX.2.00.1207262031050.23425@macbroy21.informatik.tu-muenchen.de> <C36E6A96-30EF-4D60-8BA1-67385A9F848D@nicta.com.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 bittoo many features have accumulated in the system, and everytime I passby that part of the Isar toplevel, I wonder which combinations of thevarious flags actually work.I had a brief look at that code before I wrote the message and gave up,yes :-)

More substantial reforms are required ...

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forkedproofs 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;

- Previous by Date: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Next by Date: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Previous by Thread: [isabelle] Removing a lemma or locale from a theory
- Next by Thread: [isabelle] termination: Low-Level Exception, Last Function Definition
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list