Re: [isabelle] Failing afp-2015 build



On Thu, 12 Nov 2015, Peter Lammich wrote:

The "vcg_jackhammer" tactic implemented in ConcurrentGC seems to run in one of the cases with different behaviour, and thus triggers the observed error.

In my opinion, the PARALLEL_GOALS-tactics should completely hide the effects of parallelism from the user, even if this means some slowdown in the sequential case (Note: Removing the optimization for the sequential case in PARALLEL_GOALS, and using the same map-reduce approach with retrofitting as in the parallel case, fixes the problem in ConcurrentGC)

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.


	Makarius





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