Cancel outstanding tasks on document edit in the language server, second edition

[Kha]

#2648 with one additional fix: while I had reviewed all check_system calls in C++, it turns out there was one explicit call to check_interrupted I had missed and @collares found (and that didn't do anything while check_interrupted was still based on the unused thread class).

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-19 17:34:48) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-22 08:04:53) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-23 09:07:06) View Log
• ❌ Mathlib branch lean-pr-testing-2714 built against this PR, but testing failed. (2023-10-23 17:56:04) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-24 04:55:50) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-24 05:08:53) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-24 05:22:17) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-24 06:50:21) View Log
• 💥 Mathlib branch lean-pr-testing-2714 build failed against this PR. (2023-10-25 19:36:19) View Log
• ✅ Mathlib branch lean-pr-testing-2714 has successfully built against this PR. (2023-10-25 21:02:28) View Log

[semorrison]

@Kha, the failure in Mathlib appears to genuinely be due to this PR, although I don't understand how this PR could be causing it. Is there some subtle way that a timeout could show up as a motive is not type correct???

[Kha]

It is certainly puzzling, we don't even trigger interruption outside the language server. Though as we saw in the first PR, there is always room for subtle breakage like increased heartbeats.

Just to make doubly-sure before I investigate, do we have runs of the same mathlib commit with and without the PR?

[semorrison]

Let me do side-by-side runs tomorrow.

[collares]

I increased the timeout on aux1 in Mathlib/Algebra/Jordan/Basic.lean to test if the timeouts cause the error. If so, feel free to revert my change if you want to investigate why the timeout is reported as is.

[collares]

If I understand correctly, isTypeCorrect (in Lean/Meta/Check.lean) does not distinguish between exception types when returning false.

[collares]

There was another error on the mathlib testing side, but I think the error is only due to extra changes in nightly-testing incompatible with this PR's base and would go away if this PR were to be rebased. Indeed, the error is in test/linarith.lean, and it doesn't occur if you test mathlib master with this PR's toolchain.

[semorrison]

@collares, sorry your comments are too cryptic for me. What effect did increasing the timeout have?

[semorrison]

@collares, I'm not sure if this was intentional, but it seems you've left the lean-pr-testing-2714 branch in a weird broken state. It has lots of things reversed relative to nightly-testing. It's essential that we keep the diff between lean-pr-testing-NNNN and nightly-testing minimal.

I'm going to reset it to match nightly-testing and try again. 🤷‍♀️

[semorrison]

I've just rebased this on master, in the hope of getting a Mathlib compatible toolchain.

[collares]

@semorrison Sorry for the cryptic comments! Here's my attempt to explain what happened. All I did was to push the following commit (no rebase, no force push) whose parent at the time was 38fafe25a2fdbe16558184ab061e581cdc2f7c9a:

commit bd2845a3d558165a06cab4ee3dda627b1ef7d9a4
Author: Mauricio Collares <mauricio@collares.org>
Date:   Mon Oct 23 19:44:14 2023 +0200

    bump timeout in Mathlib.Algebra.Jordan.Basic

diff --git a/Mathlib/Algebra/Jordan/Basic.lean b/Mathlib/Algebra/Jordan/Basic.lean
index 745fedf19a..10b66852e8 100644
--- a/Mathlib/Algebra/Jordan/Basic.lean
+++ b/Mathlib/Algebra/Jordan/Basic.lean
@@ -194,6 +194,7 @@ private theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c
   simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
   abel
 
+set_option maxHeartbeats 300000 in
 private theorem aux1 {a b c : A} :
     ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) +
     2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Then two things happened:

• The heartbeat bump fixed the "motive is not type correct" message. My conjecture is that isTypeCorrect (Lean/Meta/Check.lean) catches every exception and reports it as "motive is not type correct", and it inadvertently caught a max heartbeats exception in this case.
• The last line in tests/linarith.lean started failing. But then I observed that using this PR's toolchain on mathlib master (not nightly-testing) didn't exhibit such a failure, which led me to believe rebasing this PR would help. I see you came to the same conclusion, thanks for the rebase!

This corresponds to the "Mathlib branch lean-pr-testing-2714 built against this PR, but testing failed." run mentioned above by the bot.

[semorrison]

@Kha, unfortunately Mathlib/Lean combined CI is really struggling with the number of breaking changes we have in the air at the moment. I think we understand what is going on here, and Mathlib is easy to patch (by increasing a timeout), so please feel free to proceed with this one, and I'll deal with the Mathlib fallout once it hits a nightly release.

[Kha]

Do we know whether the heartbeat increase is significant? /cc @collares

[collares]

It goes up from 199700 heartbeats (mathlib master, v4.2.0-rc4) to 200745 heartbeats (nightly-testing + this PR).

[collares]

The benchmark run at leanprover-community/mathlib4#7933 seems OK.

[semorrison]

Seems insignificant, and we just got unlucky with something extremely close to the line.

[Kha]

I used this PR for editing core without further problems, so let's put it in stage 0.