From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Richard Copley Newsgroups: gmane.emacs.bugs Subject: bug#66759: 30.0.50; Flymake (with Eglot) error cleaning up old overlay Date: Thu, 26 Oct 2023 15:17:34 +0100 Message-ID: References: <87pm111pkh.fsf@gmail.com> Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="15579"; mail-complaints-to="usenet@ciao.gmane.io" Cc: 66759@debbugs.gnu.org To: =?UTF-8?Q?Jo=C3=A3o_?= =?UTF-8?Q?T=C3=A1vora?= Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Thu Oct 26 16:19:06 2023 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1qw1CT-0003nS-PC for geb-bug-gnu-emacs@m.gmane-mx.org; Thu, 26 Oct 2023 16:19:05 +0200 Original-Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1qw1CB-0000ks-R6; Thu, 26 Oct 2023 10:18:50 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qw1By-0000j3-Qv for bug-gnu-emacs@gnu.org; Thu, 26 Oct 2023 10:18:39 -0400 Original-Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qw1Bv-0005dy-U4 for bug-gnu-emacs@gnu.org; Thu, 26 Oct 2023 10:18:32 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1qw1CQ-0000z7-BF for bug-gnu-emacs@gnu.org; Thu, 26 Oct 2023 10:19:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: Richard Copley Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Thu, 26 Oct 2023 14:19:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 66759 X-GNU-PR-Package: emacs X-Debbugs-Original-Cc: bug-gnu-emacs@gnu.org Original-Received: via spool by submit@debbugs.gnu.org id=B.16983299263762 (code B ref -1); Thu, 26 Oct 2023 14:19:02 +0000 Original-Received: (at submit) by debbugs.gnu.org; 26 Oct 2023 14:18:46 +0000 Original-Received: from localhost ([127.0.0.1]:34292 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qw1C9-0000yc-Mk for submit@debbugs.gnu.org; Thu, 26 Oct 2023 10:18:46 -0400 Original-Received: from lists.gnu.org ([2001:470:142::17]:40106) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qw1C4-0000yL-F1 for submit@debbugs.gnu.org; Thu, 26 Oct 2023 10:18:44 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qw1BT-0000Wd-7H for bug-gnu-emacs@gnu.org; Thu, 26 Oct 2023 10:18:03 -0400 Original-Received: from mail-qt1-x82d.google.com ([2607:f8b0:4864:20::82d]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qw1BR-0005Yv-IS for bug-gnu-emacs@gnu.org; Thu, 26 Oct 2023 10:18:02 -0400 Original-Received: by mail-qt1-x82d.google.com with SMTP id d75a77b69052e-41c157bbd30so6644771cf.0 for ; Thu, 26 Oct 2023 07:18:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1698329880; x=1698934680; darn=gnu.org; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:from:to:cc:subject:date :message-id:reply-to; bh=wuaikln7cU22ACmDVsxUpjSdfohPjo6pvZIBb7ujykU=; b=Bj7Caug5Uu42O9b1HaDf8nvMAKkiEhr2jBctGeOEhLQ0lZ6WU+sXSnEJuGdUCuhudP OntlLd7fsAUWJhqV9OXUrcAIyrOEdTN2iIW5YP3H1/saWeNveRwrP78KA8B1A43HZzED rlL2AJYDdDsj7w2mQVw9UV1rYjOteJSyvoaJ0VNmApRlMTPNNry9EViNoHsbsSsRKSlG s5hJEGGyt9w5lR6iuy1R+YP+sE3I/ZzaiNhfLBF7SREsGbXVowEaFSqy6DnL7K4KONv4 0jShVA3YorLAkGV7mJLHewzkHnblJQXWOrmVPhDSKvOPlP9qqUi56nXTXH9F1BHVKh3w Povg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1698329880; x=1698934680; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=wuaikln7cU22ACmDVsxUpjSdfohPjo6pvZIBb7ujykU=; b=VbGK8Z2EKnxXXlmrlJB3q2AL7RISAD0rYkE7cKARIZvk3f/TcrxfAciXdFepvHvUGV i0ASMDaCAcRtinlHN9Rt8ywCAwJKKr3/I4baiziPdnAMSlyiPsYYnSvuuoh0Olp0NISw 0gA6h1tZ0cLU5CthDMz9Tgdz2aHb+Vl3Y1mjxjrBgLZm6tyY8eqt1AK0EtgJmbEzSc+v ZaQpREYB6IaaQfSC/Q/u+sXx3RKW4Q0/2vJHOuGPHr/024YYOrEM07FS059gU2B8d0Uw I9DFF8/Lc5I4u3Y1xBwVvABv/aaXIHx9z5WaOpdBkT1xewJUfHRkxg8oE8XDap0Wbd4n qRCA== X-Gm-Message-State: AOJu0YyNJ/E4wli03Ic45Gnl6+oLLraTYk0f7X6Nfd8+Cxu9MXIIAbIp ppP7bo7Htgwj0XcLrQnQLVqA0x81C2XkVBZZgOs= X-Google-Smtp-Source: AGHT+IEL7X82tRltUx7hF3KC149m0FcYi15v2jxbmJowyItInGEr4j1ekHIs7jJhdk+XYUsUWbaqj3CVc1xTQmWDGJI= X-Received: by 2002:ac8:59c3:0:b0:41e:196c:3a37 with SMTP id f3-20020ac859c3000000b0041e196c3a37mr16599149qtf.35.1698329880274; Thu, 26 Oct 2023 07:18:00 -0700 (PDT) In-Reply-To: <87pm111pkh.fsf@gmail.com> Received-SPF: pass client-ip=2607:f8b0:4864:20::82d; envelope-from=rcopley@gmail.com; helo=mail-qt1-x82d.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Xref: news.gmane.io gmane.emacs.bugs:273293 Archived-At: On Thu, 26 Oct 2023 at 14:24, Jo=C3=A3o T=C3=A1vora = 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 (=3D (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=C3=A3o