Over the past few weeks, I have reworked a few aspects of parallel
computation in Isabelle/ML and Isabelle/Scala, e.g. to provide
Par_List.map on both sides with more or less the same semantics
(concerning max. threads and cancelation of tasks). As Lars Hupel has
pointed out, Scala .par is
Metis proof reconstruction is already known to have occasional problems
due to polymorphism. E.g. a long-pending question is how to avoid the
various workarounds for Thm.bicompose that can be seen in Brownian motion
here:
changeset: 52225:568b2cd65d50
user:wenzelm
date:Wed
On Tue, 30 Dec 2014, Makarius wrote:
So far this is just an intermediate outline of some reforms that came
about spontaneously. We are right in the middle between two releases,
so more is likely to happen.
Another reason why more parallelism is likely to happen is my new (very
modest)
