feat: Inline spinner

[pimotte]

We want to add a spinner in the line that is currently being processed to show that a particular line is the problem in processing.

@DikieDick has an initial implementation.

[DikieDick]

The current implementation on the 'loading' branch is very much a work in progress, but the main ideas are there. After a line has been in the processing state for longer than some configured time, we show a simple decorator as seen in the video:

WhatsApp.Video.2026-02-05.at.18.00.40.mp4

This required updates to both waterproof-editor and waterproof-vscode so when testing this out (which I recommend you do), please make sure you have linked the correct branch of waterproof-editor in waterproof-vscode (some instructions can be found here)

The current implementation suffers from some little problems as you can quickly see when testing it out:

1. The indicator is not always updated without interaction from the user. E.g. a mouse click is sometimes necessary to get the indicator to move past the current 'busy' line.
2. The indicator is not always removed correctly and remains present in the last line of the document.

The main change on the waterproof-vscode side is the implementation of the executionInformation lsp notification (also see https://github.com/rocq-community/rocq-lsp/blob/main/etc/doc/PROTOCOL.md#sentence-execution-information) in https://github.com/impermeable/waterproof-vscode/blob/loading/src/lsp-client/client.ts#L139-L156 together with the accompanying lsp server setting.

The waterproof-editor side contains a lot of irrelevant changes that I should have removed a long time ago :). If you look at the diff with main (main...loading) the changes relevant to my approach are the ones regarding the busyIndicator, but feel absolutely free to do something else entirely.

Finally, if you need a Rocq file that has a variable timeout, I have used the one underneath. You can update the 10_000_000 iterations to something even larger if it is not enough to show the effect. The two goals are there to inspect the goal being updated after the timeout has passed.

From Ltac2 Require Import Ltac2.

Ltac2 rec busy (n : int) :=
  if Int.equal n 0 then ()
  else busy (Int.sub n 1).

Ltac2 long_run () :=
  busy 10_000_000.

Goal False.

long_run().

Goal True.