Re: [isabelle] Failing afp-2015 build



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.

cheers,
peter (resent at Larryâs request)

-- 
http://peteg.org/





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