Email Gateway (Jan 06 2021 at 14:34): Email Gateway (Jan 06 2021 at 14:34):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Using Isabelle2021-RC1 I am noticing an unexpected behavior that did not occur in previous versions:
editing at the tail end of a proof under construction sometimes seems to trigger re-checking of
material before the point at which editing is occurring. At least, I make some edit and I see
highlighting briefly flash on the text earlier than where I am editing, as if rechecking has been
triggered on that part. I cannot tell how far back the rechecking occurs -- in lemmas I have
just been working on it goes at least back to the beginning of the lemma being proved and perhaps
to previous lemmas. It might be associated with the insertion and deletion of "try", but I am
not sure at this time. Using "try" as a way of verifying statements as I am sketching out a
proof is pretty fundamental to how I do things, so I am constantly taking "try" in and out of
the editing buffer.
This is something that is is hard to describe how to reproduce, other than to say try writing
a proof and keep your eyes open for apparent rechecking before the point of edit. Perhaps this
report is enough to suggest what change might have been made that would cause this.
Email Gateway (Jan 09 2021 at 12:36):From: Fabian Immler via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have seen similar unexpected behavior and found a way to reproduce it somewhat reliably:
Consider the following lemma statement and proof.
Steps to reproduce superfluous rechecking:
1) Have Isabelle check the whole proof.
2) Scroll down such that the first apply (simp …) is out of the visible part of the buffer.
3) Edit the last apply command (e.g., remove eval_nat_numeral)
lemma
"fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5 ∧
fact 6 = (6::nat) * fact 5"
apply (intro conjI)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
apply (simp add: eval_nat_numeral)
done
This rechecking is limited to a single lemma statement, but note that I have seen unexpected rechecking also across lemma statements.
Best wishes,
Fabian
Email Gateway (Jan 10 2021 at 15:58):From: Makarius <makarius@sketis.net>
This should work properly in Isabelle2021-RC2: the relevant change is
https://isabelle.sketis.net/repos/isabelle-release/rev/a8e5d7c9a834
Makarius
Email Gateway (Jan 10 2021 at 15:58):From: Makarius <makarius@sketis.net>
Thank you for the detailed diagnosis.
It should work properly in Isabelle2021-RC2: the relevant change is
https://isabelle.sketis.net/repos/isabelle-release/rev/a8e5d7c9a834
Makarius
Last updated: Jan 04 2025 at 20:18 UTC