Incremental tactics leading to errors disappearing in proof

[ymherklotz]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

With incremental tactic evaluation, error reporting seems to have become brittle. There are situations where one thinks no errors are being reported, but one is able to prove anything using invalid tactics, because errors are not being reported for that line.

Even when one fixes the error, because the tactics are incremental they don't display errors until one actually modified tactics above them. If one only modifies tactics below, one can get very random behaviour where tactics should fail but seem to solve goals instead.

Context

We were working in a fairly large proof and kept non-deterministically getting into situations where Lean wouldn't report errors any more, and would seem to solve goals when it shouldn't, because we had a malformed statement very low down in the proof. Even after fixing that, we still got erratic behaviour until we finally restarted lean a few times and fixing errors that arose incrementally with every restart.

Steps to Reproduce

Live coding environment of the bug

0. Open up the live coding environment above with a lemma from the builtin List library, with an invalid focus at the end that swallows other errors in the file. Observe that lines 25 and 22 do not report errors.
1. Comment line 28: see no other error appear except that the lemma now states it uses sorry for the definition.
2. Observe that line 25 and line 22 still do not report errors. Also observe that after putting the cursor on line 25, it seems like the invalid exact tactic is solving the goal.
3. Press enter on line 22 to make the errors come back on line 22 (and now line 26).
4. Press enter on line 27 (after the simp) and see the error on line 22 disappear again.

Expected behavior: Errors should always be displayed and should not disappear after making edits. Invalid tactics should also not appear to be modifying the goal (and look like they're solving it).

Actual behavior: Errors disappear when making edits throughout a file, and invalid tactics may seem like they are solving a goal even though they are actually encountering an error.

Versions

5.11.0-nightly-2024-07-01

Additional Information

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[Kha]

Thank you for the detailed report. I can reproduce step 4 but not 1 in the sandbox.

[ymherklotz]

Indeed, thanks for trying to reproduce it. I didn't know that this actually worked if you comment close to the .. If you try and comment the line by putting the cursor at the very start of the line 28, instead of glued to the ., then it should be possible to reproduce step 1 too. It does for me in the sandbox.