Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress
On Tue, 26 Aug 2014, Makarius wrote:
I am presently investigating the reasons for this behaviour of PIDE
document scheduling, which could well be just a normal consequence of
certain heuristics in task priorities that have accumulated over time.
There is nothing special about the Isabelle2014 code base here. The
behaviour is the same in Isabelle2013-2.
It is a not fully finished aspect of parallel PIDE document processing:
some glimpses of that can be seen in my ITP 2014 paper, section 4 on the
"Execution Frontiers", which play on the safe side with linear semantic
concatenation of executions, giving away potential for parallelism.
Apart from some "asynchronous print functions" like Sledgehammer that come
out more sequential than anticipated, the bigger omission is the lack of
forked proofs that consist of more than a single 'by' command.
So the conclusion is that it is not a genuine problem, nor an erratic
breakdown. It just means that further improvements in that area are
postponed to a future release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and