Re: [isabelle] Failing afp-2015 build

Hello Peter,

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