Re: [isabelle] Failing afp-2015 build



On 17 Nov 2015, at 23:03, Makarius <makarius at sketis.net> wrote:
> 
> The ConcurrentIMP session was added before the Isabelle2015 release, where PARALLEL_ALLGOALS was not yet available as canonical shortcut.  Thus it fell into the gap of the historical confusion of what PARALLEL_GOALS really means.

When would one wish to use PARALLEL_GOALS now? (Why not just change its behaviour to that of PARALLEL_ALLGOALS?)

> So this is just a routine case of updating existing AFP entries. What is less routine is the total run-time of that session, which makes maintenance more difficult.  I have already reduced it a lot by using the newer 'subgoal' Isar command, but that is for the next Isabelle release.

Sorry about that.

I had in mind to revisit it now-ish, but youâve beaten me to it. The idea was to turn vcg_jackhammer into something case-like, so the larger proofs would look like:

proof vcg_jackhammer
  case (statement_label x y z) then show ?thesis
    < existing apply gloop >
â

We talked about this earlier. I now have time to chase up your pointers. I hoped this would yield the kind of parallelism your âsubgoalâs do now, with the advantage that itâd be more maintainable. Perhaps itâs a wash at this stage.

thanks,
peter

-- 
http://peteg.org/





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