On Thu, 23 Aug 2012, Lawrence Paulson wrote:
Agree. I often looked at these. Though they can be confusing in the presence of
multi-threading.
Right. I used to look at them until 5 years ago, when sequentialism was
discontinued. The main information was the progress of the theory loader,
I usually had something like "tail -f ... | grep Loading", but this is of
limited use since the main source of non-termination are proofs, and they
come later without correlation to what the theory loader said before.
When redoing the build tool from scratch some weeks ago, I've already
considered to include some more formal progress in accordance to the
underlying model of Isabelle since 2008. I did not get to that so far,
because other things sucked up a lot of time (such as doc-src and AFP,
which are both not fully finished yet).
On 23 Aug 2012, at 14:20, Gerwin Klein wrote:
I'd be quite keen to get the old behaviour back.
That is the wrong attitude.
I've invested a lot of time to get beyond the state of the art from 16
years ago. Since it is based on completely different technology it is
natural that certain accidental behaviour from the past is no longer
available by other accidental side conditions.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
