Email Gateway (Aug 19 2022 at 16:49): Email Gateway (Aug 19 2022 at 16:49):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hello all,
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.
This isn't a complaint as I realise there are several potential work arounds for this like using an
Isar proof or enabling skip proofs. I was just curious why this doesn't happen.
Thanks,
Matt
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 16:49):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC