Email Gateway (Aug 22 2022 at 13:53): Email Gateway (Aug 22 2022 at 13:53):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm currently working on refactoring a rather large Isar proof. In
there, I have a small number of short 'apply' scripts. When these break,
I get "Failed to finish proof" as expected on 'done'. However, unlike a
failed 'by' proof, I can't continue with the rest of the proof.
Consider this small example:
lemma
assumes P Q
shows "P ∧ Q"
proof
show P
by rule
next
show Q
sorry
qed
Here, the "show Q" part can be checked as normal. However:
lemma
assumes P Q
shows "P ∧ Q"
proof
show P
apply rule
done
next
show Q
sorry
qed
... everything after 'done' is red.
(I guess this counts as a "feature request".)
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
Just insert a "sorry" after the failing "done" and you can go on.
Andreas
Email Gateway (Aug 22 2022 at 13:54):From: Lars Hupel <hupel@in.tum.de>
Hi Andreas,
Just insert a "sorry" after the failing "done" and you can go on.
of course, that's a possibility, but I don't understand why 'done' and
'by' behave differently there in the first place.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
Neither do I understand why they behave differently. Probably only Makarius knows. The
short forms "." and ".." also behave like done and differently from their long forms "by
this" and "by rule". It looks like "by" is the outsider, because "proof(rule) qed" does
not close the proof block, either.
Andreas
Email Gateway (Aug 22 2022 at 13:54):From: Lars Hupel <hupel@in.tum.de>
Right, I forgot about 'qed'. This one is not as easy to work around
using a single strategically placed 'sorry'.
Email Gateway (Aug 22 2022 at 13:54):From: Makarius <makarius@sketis.net>
After so many years, PIDE document editing still lacks substructural
error-recovery.
The 'by' command is based on a special trick, using
Proof.future_terminal_proof: it pretends to be finished on the toplevel
and forks the actual work.
The 'sorry' and '\<proof>' commands always finish, imitating the same
behaviour.
All other proof commands just work sequentially on the surface.
Only recently, I have started to introduce some formal source structure
for indentation in the editor. More will come eventually, and error
handling in continuous checking should somehow participate.
Makarius
Last updated: Apr 24 2024 at 08:20 UTC