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.

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

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

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: Sep 25 2021 at 08:21 UTC