unofficial mirror of bug-gnu-emacs@gnu.org 
 help / color / mirror / code / Atom feed
* bug#66759: 30.0.50; Flymake (with Eglot) error cleaning up old overlay
@ 2023-10-26 12:09 Richard Copley
  2023-10-26 13:27 ` João Távora
  0 siblings, 1 reply; 4+ messages in thread
From: Richard Copley @ 2023-10-26 12:09 UTC (permalink / raw)
  To: 66759, joaotavora

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

^ permalink raw reply	[flat|nested] 4+ messages in thread
end of thread, other threads:[~2023-10-26 17:10 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-10-26 12:09 bug#66759: 30.0.50; Flymake (with Eglot) error cleaning up old overlay Richard Copley
2023-10-26 13:27 ` João Távora
2023-10-26 14:17   ` Richard Copley
2023-10-26 17:10     ` João Távora

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/emacs.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).