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