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.

Cheers
Lars




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