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.


	Makarius




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