Re: [isabelle] Failing afp-2015 build
> Why would you want that?
I don't think we want that; I believe it is by accident. From what
you're saying it sounds like your tactic is indeed "uniform", so should
be acceptable for use with PARALLEL_GOALS.
> (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). 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 quite sparse.
This archive was generated by a fusion of
Pipermail (Mailman edition) and