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

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

[Richard Copley]

[-- Attachment #1: Type: text/plain, Size: 2182 bytes --]

I'm afraid I'm unable to consistently reproduce this error. I hope you
can see the issue and devise a testcase from the following
description.

The function `flymake--publish-diagnostics' runs in two phases.
In phase 1 it deletes all the overlays referenced by the (now stale)
existing diagnostics. In phase 2 it creates new overlays for the newly
published diagnostics.

Phase 1 invokes `overlay-buffer' on the value of the :overlay property
of each diagnostic. This signals `wrong-type-argument' if the value is
nil.

Phase 2 intends to set the :overlay property of each diagnostic by
calling `flymake--highlight-line'.

The function `flymake--highlight-line' may return without setting the
:overlay property. For example:

    (when (= (overlay-start ov) (overlay-end ov))
      ;; Some backends report diagnostics with invalid bounds.  Don't
      ;; bother.
      (delete-overlay ov)
      (debug) ;; -- SEE BELOW (last line)
      (cl-return-from flymake--highlight-line nil))

This is likely to occur when `flymake-start` is called by the idle
timer, if there was a diagnostic near the end of the file and the user
has just made the file shorter. In that case, phase 2 inserts a
diagnostic with a null overlay into `flymake--state-diags'.

When `flymake--stated-diags' contains a diagnostic with a null
overlay, the next call to `flymake--publish-diagnostics' signals
`wrong-type-argument' during phase 1. If this next call also has
`flymake-start' in its call stack, the signal is caught in
`flymake--run-backend', which disables the backend.

If the backend continues to call its reporting function (as does Eglot
whenever the language server publishes diagnostics), this leads to a
flood of "Unexpected report from disabled backend %s" errors and an
unusable Emacs session.

A possible fix is to check if `flymake--highlight-line' created an
overlay before inserting a diagnostic into `flymake--state-diags',
in phase 2.

Another is to check that the :overlay property is not null before
attempting to examine and delete the overlay, in phase 1.

Attached is a backtrace from a real-life occurrence of the issue,
obtained by inserting `(debug)' (SEE ABOVE (quoted code)).

[-- Attachment #2: backtrace.txt --]
[-- Type: text/plain, Size: 59629 bytes --]

-*- coding: utf-8; -*-
;; Note: (buffer-size) is 4447
Debugger entered: nil
  (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))
  (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil)))
  (let* ((type (or (flymake-diagnostic-type diagnostic) :error)) (beg (let* ((cl-x diagnostic)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 2)))) (end (let* ((cl-x diagnostic)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 3)))) (convert #'(lambda (cell) (flymake-diag-region (current-buffer) (car cell) (cdr cell)))) ov) (cond ((and (consp beg) (not (null end))) (setq beg (car (funcall convert beg))) (if (consp end) (progn (setq end (car (funcall convert end)))))) ((consp beg) (let* ((b (funcall convert beg)) (a (if b (car-safe ...) (signal ... ...)))) (progn (setq beg a) (setq end b))))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 beg))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 end)))) (let* ((--cl-var-- (flymake-diagnostics beg end)) (e nil) (eov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq e (car --cl-var--)) (setq eov (let* ((cl-x e)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 9)))) (if (flymake--equal-diagnostic-p e diagnostic) (progn (if foreign (progn (debug) (throw ... nil)) (progn (let* ... ... ...) (let* ... ... ...)) (flymake--delete-overlay eov)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq ov (make-overlay beg end)) (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 (overlay-start ov)))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 (overlay-end ov))))) (overlay-put ov 'category (flymake--lookup-type-property type 'flymake-category)) (let* ((--cl-var-- (append (reverse (let* (...) (progn ... ...))) (reverse (flymake--lookup-type-property type 'flymake-overlay-control)) (alist-get type flymake-diagnostic-types-alist))) (value nil) (ov-prop nil)) (while (consp --cl-var--) (progn (setq value (car --cl-var--)) (setq ov-prop (car-safe (prog1 value (setq value ...))))) (overlay-put ov ov-prop value) (setq --cl-var-- (cdr --cl-var--))) nil) (let* ((--cl-default-maybe-- #'(lambda (prop value) (if (plist-member ... prop) nil (overlay-put ov prop ...))))) (progn (funcall --cl-default-maybe-- 'face 'flymake-error) (funcall --cl-default-maybe-- 'before-string (flymake--fringe-overlay-spec (flymake--lookup-type-property type 'flymake-bitmap (alist-get 'bitmap (alist-get type flymake-diagnostic-types-alist))))) (funcall --cl-default-maybe-- 'help-echo #'(lambda (window _ov pos) (let (...) (save-current-buffer ...)))) (funcall --cl-default-maybe-- 'severity (warning-numeric-level :error)) (funcall --cl-default-maybe-- 'priority (cons nil (+ 40 (overlay-get ov 'severity)))))) (overlay-put ov 'evaporate t) (overlay-put ov 'flymake-overlay t) (overlay-put ov 'flymake-diagnostic diagnostic) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq (type-of cl-x) cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 9 ov))) (if flymake-show-diagnostics-at-end-of-line (progn (save-excursion (goto-char (overlay-start ov)) (let* ((start (line-end-position)) (end (min ... ...)) (eolov (car ...))) (if eolov (let* (...) (overlay-put v ... ...)) (setq eolov (make-overlay start end nil t nil)) (overlay-put eolov 'flymake-overlay t) (overlay-put eolov 'flymake--eol-overlay t) (overlay-put eolov 'flymake-eol-source-overlays (list ov)) (overlay-put eolov 'evaporate (not ...))) (overlay-put ov 'eol-ov eolov))))) (if ov nil (debug)) ov)
  (catch '--cl-block-flymake--highlight-line-- (let* ((type (or (flymake-diagnostic-type diagnostic) :error)) (beg (let* ((cl-x diagnostic)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 2)))) (end (let* ((cl-x diagnostic)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3)))) (convert #'(lambda (cell) (flymake-diag-region (current-buffer) (car cell) (cdr cell)))) ov) (cond ((and (consp beg) (not (null end))) (setq beg (car (funcall convert beg))) (if (consp end) (progn (setq end (car ...))))) ((consp beg) (let* ((b (funcall convert beg)) (a (if b ... ...))) (progn (setq beg a) (setq end b))))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 beg))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 end)))) (let* ((--cl-var-- (flymake-diagnostics beg end)) (e nil) (eov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq e (car --cl-var--)) (setq eov (let* ((cl-x e)) (progn (or ... ...) (aref cl-x 9)))) (if (flymake--equal-diagnostic-p e diagnostic) (progn (if foreign (progn ... ...) (progn ... ...) (flymake--delete-overlay eov)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq ov (make-overlay beg end)) (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 (overlay-start ov)))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 (overlay-end ov))))) (overlay-put ov 'category (flymake--lookup-type-property type 'flymake-category)) (let* ((--cl-var-- (append (reverse (let* ... ...)) (reverse (flymake--lookup-type-property type ...)) (alist-get type flymake-diagnostic-types-alist))) (value nil) (ov-prop nil)) (while (consp --cl-var--) (progn (setq value (car --cl-var--)) (setq ov-prop (car-safe (prog1 value ...)))) (overlay-put ov ov-prop value) (setq --cl-var-- (cdr --cl-var--))) nil) (let* ((--cl-default-maybe-- #'(lambda (prop value) (if ... nil ...)))) (progn (funcall --cl-default-maybe-- 'face 'flymake-error) (funcall --cl-default-maybe-- 'before-string (flymake--fringe-overlay-spec (flymake--lookup-type-property type 'flymake-bitmap (alist-get ... ...)))) (funcall --cl-default-maybe-- 'help-echo #'(lambda (window _ov pos) (let ... ...))) (funcall --cl-default-maybe-- 'severity (warning-numeric-level :error)) (funcall --cl-default-maybe-- 'priority (cons nil (+ 40 (overlay-get ov ...)))))) (overlay-put ov 'evaporate t) (overlay-put ov 'flymake-overlay t) (overlay-put ov 'flymake-diagnostic diagnostic) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 9 ov))) (if flymake-show-diagnostics-at-end-of-line (progn (save-excursion (goto-char (overlay-start ov)) (let* ((start ...) (end ...) (eolov ...)) (if eolov (let* ... ...) (setq eolov ...) (overlay-put eolov ... t) (overlay-put eolov ... t) (overlay-put eolov ... ...) (overlay-put eolov ... ...)) (overlay-put ov 'eol-ov eolov))))) (if ov nil (debug)) ov))
  flymake--highlight-line(#s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466))
  (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 (cons d (aref v 4))))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode (progn (flymake--highlight-line d ...))) (let* ((cl-x d)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 1 ...)))))) (progn (or (stringp (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (cl--assertion-failed '(stringp (flymake--diag-locus d)))) nil) (let* ((v (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (v (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 5))))) (puthash v (cons d (gethash v v)) v))))
  (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 (cons d (aref v 4))))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode (progn ...)) (let* (...) (or ... ...) (let* ... ...))))) (progn (or (stringp (let* (...) (progn ... ...))) (cl--assertion-failed '(stringp ...))) nil) (let* ((v (let* (...) (progn ... ...))) (v (let* (...) (progn ... ...)))) (puthash v (cons d (gethash v v)) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil))
  (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 (cons d ...)))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode ...) (let* ... ... ...)))) (progn (or (stringp (let* ... ...)) (cl--assertion-failed '...)) nil) (let* ((v (let* ... ...)) (v (let* ... ...))) (puthash v (cons d (gethash v v)) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil)
  (save-restriction (widen) (cond (region (let* ((--cl-var-- (let* (...) (progn ... ...))) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* (...) (progn ... ...))) (if (or (not ...) (flymake--intersects-p ... ... ... ...)) (progn (flymake--delete-overlay ov)) (setq surviving (nconc surviving ...))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 surviving))) nil)) ((not (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 2)))) (let* ((--cl-var-- (let* (...) (progn ... ...))) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* (...) (progn ... ...))) (if ov (progn (flymake--delete-overlay ov))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 ...))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus ...)) (progn (save-current-buffer ... ... ...))) (progn (or (stringp ...) (cl--assertion-failed ...)) nil) (let* ((v ...) (v ...)) (puthash v (cons d ...) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil))
  (progn (let ((tail diags)) (while tail (let ((d (car tail))) (let* ((cl-x d)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 6 backend))) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* ((--cl-var-- (let* ... ...)) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* ... ...)) (if (or ... ...) (progn ...) (setq surviving ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 surviving))) nil)) ((not (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 2)))) (let* ((--cl-var-- (let* ... ...)) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* ... ...)) (if ov (progn ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* (...) (or ... ...) (let* ... ...)) (flymake--highlight-line d)) (t (if (or ... ...) (progn ...)) (progn (or ... ...) nil) (let* (... ...) (puthash v ... v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil)))
  (progn (let ((--cl-keys-- --cl-rest--)) (while --cl-keys-- (cond ((memq (car --cl-keys--) '(:backend :state :region :allow-other-keys)) (if (cdr --cl-keys--) nil (error "Missing argument for %s" (car --cl-keys--))) (setq --cl-keys-- (cdr (cdr --cl-keys--)))) ((car (cdr (memq ... --cl-rest--))) (setq --cl-keys-- nil)) (t (error "Keyword argument %s not one of (:backend :state :region)" (car --cl-keys--)))))) (progn (let ((tail diags)) (while tail (let ((d (car tail))) (let* ((cl-x d)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 6 backend))) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* ((--cl-var-- ...) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag ...) (setq ov ...) (if ... ... ...) (setq --cl-var-- ...) (setq --cl-var-- nil)) (let* (...) (or ... ...) (let* ... ...)) nil)) ((not (let* (...) (progn ... ...))) (let* ((--cl-var-- ...) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag ...) (setq ov ...) (if ov ...) (setq --cl-var-- ...) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* (...) (progn ... ...))) (cond ((eq locus ...) (let* ... ... ...) (flymake--highlight-line d)) (t (if ... ...) (progn ... nil) (let* ... ...))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil))))
  (let* ((backend (car (cdr (plist-member --cl-rest-- ':backend)))) (state (car (cdr (plist-member --cl-rest-- ':state)))) (region (car (cdr (plist-member --cl-rest-- ':region))))) (progn (let ((--cl-keys-- --cl-rest--)) (while --cl-keys-- (cond ((memq (car --cl-keys--) '...) (if (cdr --cl-keys--) nil (error "Missing argument for %s" ...)) (setq --cl-keys-- (cdr ...))) ((car (cdr ...)) (setq --cl-keys-- nil)) (t (error "Keyword argument %s not one of (:backend :state :region)" (car --cl-keys--)))))) (progn (let ((tail diags)) (while tail (let ((d ...)) (let* (...) (or ... ...) (let* ... ...)) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* (... ... ... ... ...) (while ... ... ... ... ... ...) (let* ... ... ...) nil)) ((not (let* ... ...)) (let* (... ... ... ...) (while ... ... ... ... ... ...) nil) (let* (...) (or ... ...) (let* ... ...)) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ... ...)) (cond (... ... ...) (t ... ... ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil)))))
  flymake--publish-diagnostics((#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)) :backend eglot-flymake-backend :state #s(flymake--state :running backend-token2723 :reported-p nil :disabled nil :diags (... ... ... ... ... ...) :foreign-diags #<hash-table eql 0/65 0x49da871081 ...>) :region (1 . 4448))
  (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 1)))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time (time-since flymake-check-start-time)))))))
  (let ((state (or (gethash backend flymake--state) (error "Can't find state for %s in `flymake--state'" backend))) expected-token) (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 1)))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time (time-since flymake-check-start-time))))))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq (type-of cl-x) cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 t))) (if (and flymake-show-diagnostics-at-end-of-line (not (cl-set-difference (flymake-running-backends) (flymake-reporting-backends)))) (progn (flymake--update-eol-overlays))) (flymake--update-diagnostics-listings (current-buffer)))
  (let* ((explanation (car (cdr (plist-member --cl-rest-- ':explanation)))) (force (car (cdr (plist-member --cl-rest-- ':force)))) (region (car (cdr (plist-member --cl-rest-- ':region))))) (let ((state (or (gethash backend flymake--state) (error "Can't find state for %s in `flymake--state'" backend))) expected-token) (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* (...) (progn ... ...))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time ...)))))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 t))) (if (and flymake-show-diagnostics-at-end-of-line (not (cl-set-difference (flymake-running-backends) (flymake-reporting-backends)))) (progn (flymake--update-eol-overlays))) (flymake--update-diagnostics-listings (current-buffer))))
  flymake--handle-report(eglot-flymake-backend backend-token2723 (#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)) :region (1 . 4448))
  apply(flymake--handle-report eglot-flymake-backend backend-token2723 ((#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)) :region (1 . 4448)))
  (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))
  (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args)))
  (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))))
  (closure ((buffer . #<buffer Grades.lean>) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args)))))((#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start ... :end ...) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)) :region (1 . 4448))
  funcall((closure ((buffer . #<buffer Grades.lean>) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply ... backend token args))))) (#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start ... :end ...) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)) :region (1 . 4448))
  (save-restriction (widen) (funcall eglot--current-flymake-report-fn diags :region (cons (point-min) (point-max))))
  eglot--report-to-flymake((#s(flymake--diag :locus #<buffer Grades.lean> :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay #<overlay from 3372 to 3378 in Grades.lean> :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus #<buffer Grades.lean> :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay #<overlay from 3588 to 3591 in Grades.lean> :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n  ih s\nargument\n  s\nhas type\n  ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n  Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay #<overlay from 4269 to 4270 in Grades.lean> :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n  v\nterm has type\n  ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay #<overlay from 4376 to 4379 in Grades.lean> :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n  blade V v\nargument\n  v\nhas type\n  ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n  Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay #<overlay from 4439 to 4440 in Grades.lean> :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus #<buffer Grades.lean> :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n    ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay #<overlay in no buffer> :orig-beg 4462 :orig-end 4466)))
  (cond (eglot--managed-mode (setq eglot--current-flymake-report-fn report-fn) (eglot--report-to-flymake eglot--diagnostics)) (t (funcall report-fn nil)))
  eglot-flymake-backend((closure ((buffer . #<buffer Grades.lean>) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))))) :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043)
  apply(eglot-flymake-backend (closure ((buffer . #<buffer Grades.lean>) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))))) (:recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043))
  (condition-case err (apply backend (flymake-make-report-fn backend run-token) args) ((debug error) (flymake--disable-backend backend err)))
  (let ((run-token (cl-gensym "backend-token"))) (let* ((b backend) (state (or (gethash b flymake--state) (puthash b (let (... ... ... ... ...) (progn ...)) flymake--state)))) (progn (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 1 run-token))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 3 nil))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 nil))))) (condition-case err (apply backend (flymake-make-report-fn backend run-token) args) ((debug error) (flymake--disable-backend backend err))))
  flymake--run-backend(eglot-flymake-backend (:recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043))
  (cond ((and (not force) (let* ((b backend) (state (or (gethash b flymake--state) (puthash b ... flymake--state)))) (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3))))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args)))
  (closure ((backend-args :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043) (force)) (backend) (cond ((and (not force) (let* ((b backend) (state ...)) (let* (...) (progn ... ...)))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil)(eglot-flymake-backend)
  run-hook-wrapped((closure ((backend-args :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043) (force)) (backend) (cond ((and (not force) (let* ((b backend) (state ...)) (let* (...) (progn ... ...)))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil) eglot-flymake-backend)
  (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start (cl-reduce #'min (mapcar #'car flymake--recent-changes)) :changes-end (cl-reduce #'max (mapcar #'cadr flymake--recent-changes)))))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* ((b backend) (state (or ... ...))) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 2 nil)))))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond ((and (not force) (let* ... ...)) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil)))
  (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start (cl-reduce ... ...) :changes-end (cl-reduce ... ...))))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* (... ...) (let* ... ... ...)))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond (... ...) (t ...)) nil)))))
  (let (--cl-start-post-command-- --cl-start-on-display--) (setq --cl-start-post-command-- #'(lambda nil (progn (remove-hook 'post-command-hook --cl-start-post-command-- nil) (if (buffer-live-p buffer) (progn (save-current-buffer ... ...)))))) (setq --cl-start-on-display-- #'(lambda nil (progn (remove-hook 'window-configuration-change-hook --cl-start-on-display-- 'local) (flymake-start (remove 'on-display deferred) force)))) (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start ... :changes-end ...)))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* ... ...))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond ... ...) nil))))))
  (let ((deferred (if (eq t deferred) '(post-command on-display) deferred)) (buffer (current-buffer))) (let (--cl-start-post-command-- --cl-start-on-display--) (setq --cl-start-post-command-- #'(lambda nil (progn (remove-hook 'post-command-hook --cl-start-post-command-- nil) (if (buffer-live-p buffer) (progn ...))))) (setq --cl-start-on-display-- #'(lambda nil (progn (remove-hook 'window-configuration-change-hook --cl-start-on-display-- 'local) (flymake-start (remove ... deferred) force)))) (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes ...))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda ... ...)) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda ... ... nil)))))))
  flymake-start(t)
  (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))
  (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t)))
  (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil))
  (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil)))
  (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil))))
  (closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug ... "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil)))))(#<buffer Grades.lean>)
  apply((closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug ... "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil))))) #<buffer Grades.lean>)
  timer-event-handler([t 0 0 500000 nil (closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn ... ...)) (setq flymake-timer nil))))) (#<buffer Grades.lean>) idle 0 nil])

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

[João Távora]

Richard Copley <rcopley@gmail.com> writes:

> I'm afraid I'm unable to consistently reproduce this error. I hope you
> can see the issue and devise a testcase from the following
> description.

Thanks very much for this report.  This problem could be the same as
https://github.com/joaotavora/eglot/discussions/1311, at least it its
most recent iteration.

Anyway, I think your analysis of the code is excellent and your
conjecture (for at least one possible cause of this problem) is very
promising.  That "don't bother with invalid bounds" was introduced
recently:

   commit 8b1947ffdd9d9eae26a308f0abaac45e06baac22
   Author: João Távora <joaotavora@gmail.com>
   Date:   Thu Sep 21 00:03:32 2023 +0100
    
       Flymake: more fixes to flymake--highlight-line
       
       Make it robust to diagonstics with invalid bounds.
       
       * lisp/progmodes/flymake.el (flymake--highlight-line): Robustify.
    
   diff --git a/lisp/progmodes/flymake.el b/lisp/progmodes/flymake.el
   --- a/lisp/progmodes/flymake.el
   +++ b/lisp/progmodes/flymake.el
   @@ -781,1 +782,5 @@
   -    (setq ov (make-overlay end beg))
   +    (when (= (overlay-start ov) (overlay-end ov))
   +      ;; Some backends report diagnostics with invalid bounds.  Don't
   +      ;; bother.
   +      (delete-overlay ov)
   +      (cl-return-from flymake--highlight-line nil)):


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.

What language server are you using with Eglot btw?

> 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).

João

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

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

[João Távora]

Richard Copley <rcopley@gmail.com> writes:

> On Thu, 26 Oct 2023 at 14:24, João Távora <joaotavora@gmail.com> wrote:
>> Please keep an eye out of this bug.
>
> Thanks, will do.

I've now reproduced the bug consistently.  It happens exactly as you
conjectured.  To test, I temporarily hacked Eglot to take 2 seconds
longer to process each request/notification with this patch:

diff --git a/lisp/progmodes/eglot.el b/lisp/progmodes/eglot.el
index eba66503bf7..48845a889a8 100644
--- a/lisp/progmodes/eglot.el
+++ b/lisp/progmodes/eglot.el
@@ -1488,7 +1488,7 @@ eglot--connect
                      ,@more-initargs)))))
          (spread (lambda (fn) (lambda (server method params)
                                 (let ((eglot--cached-server server))
-                                  (apply fn server method (append params nil))))))
+                                  (run-at-time 2 nil #'apply fn server method (append params nil))))))
          (server
           (apply
            #'make-instance class

And then made sure there was a diagnostic at the end of the file,
changed the file and quickly enough (but only after the changes were
sent to server), deleted the region with the diagnostic at the end of
the file.

Without my fix, I get exactly the (overlayp nil) error you reported.
With the fix, everything works correctly.

So I think with the fix I pushed earlier this bug can be closed, which
I'm doing now.

>> What language server are you using with Eglot btw?

> [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

Yeah I know about these PRs.  If you want can start a new report in the
Emacs bug tracker proper (i.e. here) )and direct people to it.  Write a
summary of the situation if you can, and present this Lean4 use case as
a argument.

This gives visibility to more Emacs maintainers, and allows me to ping
specialists like Eli more easily on the matter.

João