[isabelle] [Fwd: Re: Failing afp-2015 build]

--- Begin Message ---
This email got rejected from cl-isabelle-users with the unhelpful message:

> Message rejected by filter rule match

On 12 Nov 2015, at 19:07, Makarius <makarius at sketis.net> wrote:
> Using the dangerous word "fix" means there is a lack of information what is really going on.  Maybe the author of the "vcg_jackhammer" proof method can look again and explain the situation.

I’m not doing anything clever here - my use of PARALLEL_GOALS was intended to have the same semantics as ALLGOALS (IIRC - it’s been a while). As far as I’m concerned it’s just an optimisation, albeit one that was somewhat essential to invariant discovery.

The goals produced by vcg_jackhammer should be completely independent (no schematics etc).

I never tested the single-threaded mode, and don’t see the point in it having an observably-distinct (wrt goal states etc.) semantics from the multi-threaded one. Why would you want that? (What is the point of running single-threaded these days?)

Thanks to everyone for the diagnoses.



--- End Message ---

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