Re: [isabelle] Failing afp-2015 build

On 12 Nov 2015, at 19:07, Makarius <makarius at> 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.

peter (resent at Larryâs request)


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