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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and