Re: [isabelle] Parallelising apply-style proofs



On Fri, 12 Dec 2014, Matthew Fernandez wrote:

When working in Isabelle/jEdit with parallel proofs set to 2, "by" does not impede progress through the theory. By which I mean a "by" step can remain purple and being processed while the rest of the theory proceeds. The same does not seem to be true of a proof with many "apply" steps followed by a "done." Is there a fundamental reason this doesn't happen or is this just a design decision? It seems to me that processing could proceed past the proof as soon as the lemma statement itself has been parsed.

That is a long-standing omission in PIDE document processing: the prover merely walks down the sequential arrangement of commands and does only local forks of diagnistic and 'by' commands. Conceptually, whole proofs could be forked recursively, both Isar proof outlines and apply scripts, as is done in batch mode.

There are various practical reasons why the parallel batch mode and the PIDE interaction mode did not yet converge in that respect, but it will happen at some point.

By bringing up this issue, its priority in the pipeline is increased once again.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  1,143,292 people so far
----------------------------------------------------------------------------




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