bug#66759: 30.0.50; Flymake (with Eglot) error cleaning up old overlay

[Richard Copley]

On Thu, 26 Oct 2023 at 14:24, João Távora <joaotavora@gmail.com> wrote:
> And indeed the flymake--diag-overlay slot is not filled in when we get
> this early return.  And indeed the overlays considered for deletion are
> the ones stored in the "state" map, meaning everything the backend
> reported.
>
> So maybe this patch is all that's needed:
>
> diff --git a/lisp/progmodes/flymake.el b/lisp/progmodes/flymake.el
> index b27e6527f81..9be40499d37 100644
> --- a/lisp/progmodes/flymake.el
> +++ b/lisp/progmodes/flymake.el
> @@ -809,6 +809,7 @@ flymake--highlight-line
>                          (flymake--diag-orig-end e))
>                    (flymake--delete-overlay eov)))
>      (setq ov (make-overlay beg end))
> +    (setf (flymake--diag-overlay diagnostic) ov)
>      (when (= (overlay-start ov) (overlay-end ov))
>        ;; Some backends report diagnostics with invalid bounds.  Don't
>        ;; bother.
> @@ -863,7 +864,6 @@ flymake--highlight-line
>      (overlay-put ov 'evaporate t)
>      (overlay-put ov 'flymake-overlay t)
>      (overlay-put ov 'flymake-diagnostic diagnostic)
> -    (setf (flymake--diag-overlay diagnostic) ov)
>      ;; Handle `flymake-show-diagnostics-at-end-of-line'
>      ;;
>      (when flymake-show-diagnostics-at-end-of-line
>
>
> There's a fair chance this fixes the bug effectively, but even if it
> doesn't, it is nevertheless a solid change, so I've pushed it and bumped
> the Flymake ELPA package version.
>
> Please keep an eye out of this bug.

Thanks, will do.

> What language server are you using with Eglot btw?

Lean 4 [1]. There's a supporting Emacs mode [2] based on lsp-mode. I
have a fork which uses Eglot instead [3]. There's nothing missing from
Eglot, but one needs a lot of help from Lean 4 in order to read and
write programs and proofs in Lean 4. Btw, some in the community are
keen for the LSP semantic tokens feature to be implemented (see
[4][5]). The existing `font-lock keywords' in lean4-mode work to a
degree but leave something to be desired, since the language has
user-defined syntax.

[1] https://leanprover-community.github.io/learn.html
[2] https://github.com/leanprover/lean4-mode
[3] https://github.com/bustercopley/lean4-mode
[4] https://github.com/joaotavora/eglot/issues/615
[5] https://github.com/joaotavora/eglot/pull/839

> > A possible fix is to check if `flymake--highlight-line' created an
> > overlay before inserting a diagnostic into `flymake--state-diags',
> > in phase 2.
>
> This could also work, but is slightly more complex.  And it would
> destroy the invariant that that list contains every "domestic"
> diagnostic reported by the backend (even invalid ones).

Ah yes. And risky without a test case.

> João