From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Stefan Kangas Newsgroups: gmane.emacs.bugs Subject: bug#66552: 30.0.50; Eglot feature request: handle quirky code actions Date: Wed, 10 Jan 2024 03:06:11 -0800 Message-ID: References: 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="24786"; mail-complaints-to="usenet@ciao.gmane.io" Cc: 66552-done@debbugs.gnu.org, =?UTF-8?Q?Jo=C3=A3o_?= =?UTF-8?Q?T=C3=A1vora?= To: Richard Copley Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane-mx.org@gnu.org Wed Jan 10 12:07:19 2024 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 1rNWQZ-0006Dz-GG for geb-bug-gnu-emacs@m.gmane-mx.org; Wed, 10 Jan 2024 12:07:19 +0100 Original-Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rNWQK-0007ff-FC; Wed, 10 Jan 2024 06:07:04 -0500 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 1rNWQH-0007f0-NY for bug-gnu-emacs@gnu.org; Wed, 10 Jan 2024 06:07:01 -0500 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 1rNWQC-000453-1y for bug-gnu-emacs@gnu.org; Wed, 10 Jan 2024 06:06:57 -0500 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rNWQI-00086A-Bc for bug-gnu-emacs@gnu.org; Wed, 10 Jan 2024 06:07:02 -0500 Resent-From: Stefan Kangas Original-Sender: "Debbugs-submit" Resent-To: bug-gnu-emacs@gnu.org Resent-Date: Wed, 10 Jan 2024 11:07:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: cc-closed 66552 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: notabug Mail-Followup-To: 66552@debbugs.gnu.org, stefankangas@gmail.com, rcopley@gmail.com Original-Received: via spool by 66552-done@debbugs.gnu.org id=D66552.170488478831068 (code D ref 66552); Wed, 10 Jan 2024 11:07:02 +0000 Original-Received: (at 66552-done) by debbugs.gnu.org; 10 Jan 2024 11:06:28 +0000 Original-Received: from localhost ([127.0.0.1]:42160 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rNWPj-000851-RB for submit@debbugs.gnu.org; Wed, 10 Jan 2024 06:06:28 -0500 Original-Received: from mail-ed1-x535.google.com ([2a00:1450:4864:20::535]:46092) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rNWPh-00084m-Cy for 66552-done@debbugs.gnu.org; Wed, 10 Jan 2024 06:06:25 -0500 Original-Received: by mail-ed1-x535.google.com with SMTP id 4fb4d7f45d1cf-555e07761acso4809420a12.0 for <66552-done@debbugs.gnu.org>; Wed, 10 Jan 2024 03:06:17 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1704884772; x=1705489572; darn=debbugs.gnu.org; h=content-transfer-encoding:cc:to:subject:message-id:date :mime-version:references:in-reply-to:from:from:to:cc:subject:date :message-id:reply-to; bh=HatSfqZKRRTqihhdkb8dIj7zwv+sZrqbo7hMhhmtulE=; b=NkWRjN6wGj7qsbade606a83oN4CUcaRFwLH1nnV+HgjW5PgzF0+YzfEV9erRyWgL1c LISj5o7CofdR+NCqcKFQEscmc8CNsSW1b+gWlUJy50MjGPtPGLTTZqdTxnLsW5cDtLY0 ebcy/kvAltuC4pgcypJN424uoEBhlwNztjBvnkIzr1AnsKqy0QyQZx8LL3DN8U/XMJld YgLBQUVi3zz5LR/Zotpe0p0c7rxANU2F3o76pUB+F5SefV9bPjLhJMhgUcS+AlGCIQ7u 9NWv6spc512cm7cnpsAhwM50hpQlK+j2lKv3DIM+gdwjZzG/bcNPhi8jj7yqD6XmMcxa mAFQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1704884772; x=1705489572; h=content-transfer-encoding:cc:to:subject:message-id:date :mime-version:references:in-reply-to:from:x-gm-message-state:from:to :cc:subject:date:message-id:reply-to; bh=HatSfqZKRRTqihhdkb8dIj7zwv+sZrqbo7hMhhmtulE=; b=TxMgOAJVtwTike8U6BMwUWescKhE09SU7Se6R7a8kj637TkRN05j776BsfElYmQ/Ae PlWQktM+5PbvTGsrBLUF4FOtYnnk/1+bWCT19BxFzJn86lF5M7JPxC8vWHz7Xv3goRx5 eCvTnQKedGbHao3HgalKBVetb7FjTZO09zjFvBflLl9GJcOKqIjkPnERZXbXZk9fZdlZ lXZrwKd3W5N97WkUcG3e5MoWOSyU3ju8XPTEQcSAd2wYz4Mj/3Oa2OV62onYwxOBTOw8 u2MEIiXMoyLOLaZvK8kWdbFEqo1b1V0YT0Y7hT0bxzO6vGKC6lAhKYkArgOs6BHTAfVg mOAg== X-Gm-Message-State: AOJu0Yy+e7eQQ1GpUGsbS679b0ierkybdMxZas7sGPhanOG07VCXi1jX MeLtMhTFlH9RTFCZiiOz8pgg0O+nJn4UVy9pglc= X-Google-Smtp-Source: AGHT+IFYjg/s/qrQNYOmANHNcRKe8zHe+tHIe7t88GVzhbxC7E0xiaI83hGpLTGAwMf11gB79g5CpNRt+aMmU1Ph8nM= X-Received: by 2002:aa7:c649:0:b0:553:a3ec:85f5 with SMTP id z9-20020aa7c649000000b00553a3ec85f5mr252536edr.85.1704884772214; Wed, 10 Jan 2024 03:06:12 -0800 (PST) Original-Received: from 753933720722 named unknown by gmailapi.google.com with HTTPREST; Wed, 10 Jan 2024 03:06:11 -0800 In-Reply-To: (Richard Copley's message of "Thu, 26 Oct 2023 15:41:20 +0100") 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:277710 Archived-At: Richard Copley writes: > On Tue, 17 Oct 2023 at 04:11, Jo=C3=A3o T=C3=A1vora wrote: > >> But I really think you should report these two things to the >> language server authors. > > The issue with the incorrect version number in server edits will be > fixed soon. Thanks for the encouragement! > > Core Lean 4 language: #2721 [1] > Standard library: #306 [2] > Mathematics library: #7812 [3] > > [1] https://github.com/leanprover/lean4/pull/2721 > [2] https://github.com/leanprover/std4/pull/306 > [3] https://github.com/leanprover-community/mathlib4/pull/7812 > > I will need to rest and recuperate before advocating for the other > thing to be fixed. Thanks for reporting that upstream. Meanwhile, I don't think it makes sense to keep this bug report open, so I'm closing it now.