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.
peter (resent at Larryâs request)
This archive was generated by a fusion of
Pipermail (Mailman edition) and