Re: [isabelle] Failing afp-2015 build

> 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.

"Fix" was meant in the sense "make disappear this very instance of the
problem". Actually the described change aligns the behaviour for
threads=1 and threads>1, sacrificing the optimization that is currently
there for threads=1.

However, to general questions remain:

1) Is it intentional/desirable to have the behaviour of PARALLEL_GOALS
depend on the number of threads:
  Pro: This allows the current optimization for threads=1
  Con: This makes debugging of tactics/proofs which use PARALLEL_GOALS
harder, as one has to test for threads=1 and threads>1 separately.

2) Is there any documentation on what are the preconditions of
PARALLEL_GOALS such that it shows no diverging behaviour in the
parallel/sequential case? This information is required by anyone who
wants to use PARALLEL_GOALS in a thread-safe way.


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