Re: [isabelle] Failing afp-2015 build
On Tue, 17 Nov 2015, Lars Hupel wrote:
(What is the point of running single-threaded these days?)
I only discovered that as part of my investigations into how to reliably
build the AFP. There are essentially two axes for parallelism: Internal
to a session (multi-threaded, e.g. parallel proofs, parallel theories)
and between sessions (multi-process, i.e. independent AFP sessions can
be run in parallel).
Sequentialism is indeed a very atypical situation, more than 10 years of
multicore hardware becoming mainstream.
In the various different isatest configurations for main Isabelle (not
AFP) we do indeed test normal situations, like threads=4 or threads=8,
alongside with abnormal ones like threads=1 or skip_proofs=true.
Such tests provide empirical evidence that the "physics" of a
highly-complex parallel ML and proof engine comes out as reliably
"mathematics", i.e. results are determined. Asking for determinism in
every respect is a bit much.
Gerwin and I suspect that it would be most efficient to exploit the
latter on the cost of the former, since the AFP dependency graph is
What always happens in such situations is that the total runtime converges
to the longest sequential task. That used to be JinjaThreads, now it is
AODV or ConcurrentGC. These take many hours CPU time. With a good
multicore machine of 2015, it should be possible to run all of Isabelle +
AFP in approximately 1h elapsed time, maybe even less after some tweaking.
This archive was generated by a fusion of
Pipermail (Mailman edition) and