From unknown Tue Sep 09 21:32:53 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#39020] Lean won't work with the emacs mode Resent-From: Arvid Marx Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 07 Jan 2020 19:07:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 39020 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 39020@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.157842400210411 (code B ref -1); Tue, 07 Jan 2020 19:07:01 +0000 Received: (at submit) by debbugs.gnu.org; 7 Jan 2020 19:06:42 +0000 Received: from localhost ([127.0.0.1]:49341 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iouBd-0002hr-Sn for submit@debbugs.gnu.org; Tue, 07 Jan 2020 14:06:42 -0500 Received: from lists.gnu.org ([209.51.188.17]:58866) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iotzH-0002Nd-NU for submit@debbugs.gnu.org; Tue, 07 Jan 2020 13:53:55 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:38538) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iotzG-0002t2-Gu for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:55 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,RCVD_IN_DNSWL_NONE autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iotzF-00020D-KL for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:54 -0500 Received: from mout.kundenserver.de ([212.227.126.187]:51987) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iotzF-0001yA-BC for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:53 -0500 Received: from DESKTOP-KHP2F58 ([93.255.126.7]) by mrelayeu.kundenserver.de (mreue011 [212.227.15.167]) with ESMTPSA (Nemesis) id 1MirX2-1jIRuE1mSK-00eteK for ; Tue, 07 Jan 2020 19:53:50 +0100 Message-ID: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> From: Arvid Marx Date: Tue, 07 Jan 2020 19:53:49 +0100 Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.30.5 (3.30.5-1.fc29) MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Provags-ID: V03:K1:J2ujtxdtya9LyBa3WE3xW6GkRakswRy3hiHf4mwGep+0FW7SVrQ X3VKZXAA2J9jPFG7SYUp0LJdyyzsKvWyQF5soZ8ZePZzyC0d3nSKq9OEgdZPSTvbr/bCMak SfJIbhtS0QEjU4yKwq72K1kwsy4iTBFFq/siggh+CP839oOdAlagfG0fC/DLUXZxPjCo/jL xoLSjy3b9hJdNJT9KpCWw== X-UI-Out-Filterresults: notjunk:1;V03:K0:F9597yLtpuE=:eZSUbnidkCAkyK20hY54I+ OXsGHiR3QFtQpdZN5Xx9Lz/dpN2UA4In4qKaePBAJbdIGo/J7hd78BtcbiGpO3QYDhq4523iC s8KKeBxz1CGps+x24NZkwYya+KCxGJZAYELVzqwXLinDTdM3f9Dv9GQH3GqH1d6+rLXRAl3wu 7a513VE0XOYWuDXbEjwieepYImsSQ9jl4ekZYH5KeXO7DiUN7PvfGfWuSokh8IU0s63FpC15E OAl2dtXUDc+LB8Gj1AIA4fYlXkoqz5KW2FhCMbyAsUi7fbdSV/YcN8SxYoyabsPe/aAcCTwfa d0IruV4U1n3HtpjLP0CHffSaRamlGxJOPEZZaUMCR78yVyfBP0MHhAo59ccX6dt5n2uvGj7+a tXeYCWhNOOwkKHsUhj4XbMRRNxXFSpAddCGrB1QH0kSFD32AflB0LTYvNUYESZmRiKE4wMB9v jbaGWpuRSMDyAJGX5mpzkWQJNaxqY7zQTuI/oy8F5TyxG3hAsbpfiYOW8/F83MMUA9WepwcCS E91hcDXjGvTUwIAEKbexMxYdrsNlZsCId65rgiovmeCumEdbjiewRkhN9kQHRG2Kk35f/f+Hc dYzGzYTMzsJoTmtzmBJASC3p7DMo9gPyfILA6BsprZ7PhwEw4eLv7+KEUSzHjF9FXgbUtsUkM NXlmzjGyy1v1tpz4rlhp+yVeO85cuNqTdHVE3GE7OnW7gClmbVxycb2bjZSUZLYiYJfXGwHZd sBWYD2LMVE/vgCbeO9E4J33Eynjaszdo45OS4ikaHEons5uITcPu3QWfSpRADAl2TYNqAIH/q xIBvHmXusY+eWrG+0zSS4Z0PuA5jofUWHDQRNfbeljCHe6sD60cN3UXxAKMLyz8AM2tKL+1wc 80hBjMhSN8Hno/bATcO7BJtqMqGF+GwaKzqu7j3Lo= X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 212.227.126.187 X-Spam-Score: -2.3 (--) X-Mailman-Approved-At: Tue, 07 Jan 2020 14:06:40 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) The emacs mode for Lean (which doesn't appear to be packaged yet, but of course works via MELPA etc.) expects some sort of root directory for Lean, which is not given simply because binaries and other files are put into separate directories. This of course makes Lean impossible to use as intended. However, I'm not quite sure how this would be fixed in practice, as I'm not aware of any suitable directory hierarchy in such a case. Any ideas? -- Arvid From unknown Tue Sep 09 21:32:53 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#39020] Lean won't work with the emacs mode Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 07 Jan 2020 19:12:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 39020 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: Arvid Marx Cc: 39020@debbugs.gnu.org, bandali@gnu.org Received: via spool by 39020-submit@debbugs.gnu.org id=B39020.157842432010932 (code B ref 39020); Tue, 07 Jan 2020 19:12:02 +0000 Received: (at 39020) by debbugs.gnu.org; 7 Jan 2020 19:12:00 +0000 Received: from localhost ([127.0.0.1]:49358 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iouGm-0002qF-Ht for submit@debbugs.gnu.org; Tue, 07 Jan 2020 14:12:00 -0500 Received: from eggs.gnu.org ([209.51.188.92]:40993) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iouGk-0002q2-HN for 39020@debbugs.gnu.org; Tue, 07 Jan 2020 14:11:59 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:53547) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1iouGf-0002QQ-53; Tue, 07 Jan 2020 14:11:53 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=50720 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1iouGe-0002dm-8Y; Tue, 07 Jan 2020 14:11:52 -0500 From: Brett Gilio References: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> Date: Tue, 07 Jan 2020 13:11:56 -0600 In-Reply-To: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> (Arvid Marx's message of "Tue, 07 Jan 2020 19:53:49 +0100") Message-ID: <87zhezqdxf.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Arvid Marx writes: > The emacs mode for Lean (which doesn't appear to be packaged yet, but > of course works via MELPA etc.) expects some sort of root directory for > Lean, which is not given simply because binaries and other files are > put into separate directories. This of course makes Lean impossible to > use as intended. However, I'm not quite sure how this would be fixed in > practice, as I'm not aware of any suitable directory hierarchy in such > a case. > > Any ideas? > > -- > > Arvid Cc'ing Amin Bandali, who took care of packaging Lean. I am happy to help too, but I want to see what he says first. -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] From unknown Tue Sep 09 21:32:53 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#39020] Lean won't work with the emacs mode Resent-From: Maxim Cournoyer Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 07 Jan 2020 21:40:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 39020 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: Arvid Marx Cc: 39020@debbugs.gnu.org Received: via spool by 39020-submit@debbugs.gnu.org id=B39020.157843318625472 (code B ref 39020); Tue, 07 Jan 2020 21:40:02 +0000 Received: (at 39020) by debbugs.gnu.org; 7 Jan 2020 21:39:46 +0000 Received: from localhost ([127.0.0.1]:49499 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iowZl-0006cm-SR for submit@debbugs.gnu.org; Tue, 07 Jan 2020 16:39:46 -0500 Received: from mail-qt1-f195.google.com ([209.85.160.195]:38564) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iowZj-0006cX-HX for 39020@debbugs.gnu.org; Tue, 07 Jan 2020 16:39:43 -0500 Received: by mail-qt1-f195.google.com with SMTP id n15so1056308qtp.5 for <39020@debbugs.gnu.org>; Tue, 07 Jan 2020 13:39:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=Ud9rbNR8EpGhGHvGtvgw6r7+kxDwM0p4o1ZaAHFJL8Y=; b=BiH0F62TIdpTKjkRD8KzgZZ7tsG437tgMs+hPIW07l45G+Xwyeute+FWoWbx5i2+cq VeAUH7MDsKfXg0jqbnO9e7ZUwB4vgU9rKnAq4JDUZrCrDfaeEbnJHUTyOfVYs4C5lMFD E8d2gQ1JSlYnCYd0t82q1Ja64MqQ+yt99XQTZqZAnvrSq+obC8vt/ZxrsFNQptJctolH YQiOnqrhwP9hzr0JDRcBhOWB75bHV7y67f6M3iL3hMEDwr2pkQXDUMZTLjNhT/WnVQw5 0rqxGkEoRp6FhTiuUwPbRoT2RMVmD5qJ8YKoLYYR5DabGLsf7+YljxACNgv3TBaGwrYX GCzg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=Ud9rbNR8EpGhGHvGtvgw6r7+kxDwM0p4o1ZaAHFJL8Y=; b=YP8sDc2DT3Xd0en1ONU8umCw3lEIeRllfqBXfNHd4NJlodNBVneMvptA7mzX3CJnlw Gb8erRjrhZRP4SKI890DTXRq/put80VVGARV59G5gwZG0nTRZPsEXM/EU+tW5Z/VSC9L 6H3tM+fDz9yZFZ4GkJ3WKJHA3a6P/gtOiJXXVp4qwZP2rDxCuhNDT/jN/wnO5DbBhic6 GG0x6dUnwoodqyfVuWrrp7vbhdLyFjwBTGL/hiZVDlv4FOHRJWiA0c9hQRHsx6EvniNK EBFC+KPaE070B6I0byEpSFM4AmYIwC4exAdDKD9tRpVXcwq0Qpg8ykU74yOKe+R5Iuvf C4cw== X-Gm-Message-State: APjAAAWLKkN1hCS8DXEQb3Dzcmpxgp2aYHxTlsDXbQcGsG+O4/Mrk38r 4EFHbGSXd3rA30IZRGM6AgjyAvPt X-Google-Smtp-Source: APXvYqybT1t7cHc19GgKm36gAJ7sUJOi/j/AWly9HnXwDWxd/6e7UDN0L7mpFc5ep5BX6MKt/tuHuA== X-Received: by 2002:ac8:544f:: with SMTP id d15mr920009qtq.53.1578433177887; Tue, 07 Jan 2020 13:39:37 -0800 (PST) Received: from apteryx (dsl-205-233-125-130.b2b2c.ca. [205.233.125.130]) by smtp.gmail.com with ESMTPSA id w20sm567160qtj.4.2020.01.07.13.39.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 07 Jan 2020 13:39:37 -0800 (PST) From: Maxim Cournoyer References: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> Date: Tue, 07 Jan 2020 16:39:33 -0500 In-Reply-To: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> (Arvid Marx's message of "Tue, 07 Jan 2020 19:53:49 +0100") Message-ID: <87woa3uesq.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hello Arvid, Arvid Marx writes: > The emacs mode for Lean (which doesn't appear to be packaged yet, but > of course works via MELPA etc.) expects some sort of root directory for > Lean, which is not given simply because binaries and other files are > put into separate directories. This of course makes Lean impossible to > use as intended. However, I'm not quite sure how this would be fixed in > practice, as I'm not aware of any suitable directory hierarchy in such > a case. > > Any ideas? When writing the package definition for the Emacs Lead mode, the code could be rewritten to refer to the absolute path of the files/programs it uses from the Lean project, by patching it with `substitute*' uses, for example. If that is not easy to do, another idea would be to create some kind of overlay directory which would flatly collect all the items needed then refer to that (the items would be symlinked to their real location). See the `union-build' procedure of the (guix build union) module of Guix. HTH! Maxim From unknown Tue Sep 09 21:32:53 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#39020] Lean won't work with the emacs mode Resent-From: Arvid Marx Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 08 Jan 2020 14:19:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 39020 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: Maxim Cournoyer Cc: 39020@debbugs.gnu.org Received: via spool by 39020-submit@debbugs.gnu.org id=B39020.157849310528567 (code B ref 39020); Wed, 08 Jan 2020 14:19:01 +0000 Received: (at 39020) by debbugs.gnu.org; 8 Jan 2020 14:18:25 +0000 Received: from localhost ([127.0.0.1]:49910 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ipCAC-0007Qg-Lf for submit@debbugs.gnu.org; Wed, 08 Jan 2020 09:18:24 -0500 Received: from mout.kundenserver.de ([212.227.126.131]:39115) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ipCAB-0007QR-FB for 39020@debbugs.gnu.org; Wed, 08 Jan 2020 09:18:23 -0500 Received: from DESKTOP-KHP2F58 ([93.255.126.7]) by mrelayeu.kundenserver.de (mreue012 [212.227.15.167]) with ESMTPSA (Nemesis) id 1M28O9-1ir86L278D-002Y1S; Wed, 08 Jan 2020 15:18:16 +0100 Message-ID: <235c2b1104ffbc9bc72b777edc61c8caad541a00.camel@logicandtypes.org> From: Arvid Marx Date: Wed, 08 Jan 2020 15:18:14 +0100 In-Reply-To: <87woa3uesq.fsf@gmail.com> References: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> <87woa3uesq.fsf@gmail.com> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.30.5 (3.30.5-1.fc29) MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Provags-ID: V03:K1:HcPuXCO9fMvl2+9I/Ne1MkyzVXtchLMcn5vFkmz0W/4W/xQLVWl JGZs2oK2EYhfEmORYb1tI4efPkJwT+UA+8rZWobjL1uo9w8d2D7uvwkTA2tPY2F1jzt/Cmf vUi8zClNj/2S2Ewg927QyxWJvbWjXuUb9ivWPc0ZK6pJTZXt9A5KolNqgvd3B+Ml+Q5HSV4 TnxAJSLxe4Szxdo6ItIxg== X-Spam-Flag: NO X-UI-Out-Filterresults: notjunk:1;V03:K0:zI6XdwX3Uvo=:P2zw+TGgP8OVwy3/3ypQ/I H0MYCnSgFGnEU+T31MRUyOOzFctlEixZUpUUulnKwj99D9898bawSV7MmHTyrMeSDPrUogDoe TPSFdOz8G+o+BL4IvsKoCK5KQBGGJV5KIiRMHZgqC6f1Gp0HFQDpAOGcv5rg90GoRMEPUplf4 wpLnSwNp76cTqxvSAMPL+19kN9wdfZRghhO/cQx0SH1ZJUnG6T2Lq/WJtEi+CnazOX1SN7jLl 6ngLqeXoAe3SKFl2z4qqawfK2MRxqjqnWNUz+W1QtUp1HENvy8SIIhLK4KeeT5jtgSPLM/HEo Gj87DdCdYlmOwjaeKCKKa9f6c/cJ+HwwsBPVlr0uKZFN5vXacDMtrWLoVPe430TN7/gSuGU1L HwhaY0Q0Frmz1SmDQAtjkOSVGwvU64woLsT6rGrrlw1A+MQp38bfz4ScAvNvvklqN/BPPolBA IHAaxad2yDj7+Zn/LntwAuY7VvBdwPbErItF9mG6PdnHeKVSNdE+3FduXvIcdrOxoRP0fBrDr JCzcy/jGbSwUzuM4vLbv1XCiGgV6kH28d6lO/smh39cT8gv2sH2Gp2aUPxPLqtPkzUF0UjPqA WAdqpWHhuWlaQR1L4f1MtvSmOunPoHY3ptz6rqX+XVcYBmIa1l/dAM5CeGOqEPL/U6/DL9kfo yK79C4KiWxpF43wnK0t6yMrMUDNxZM70RXfMbtTrfWY6aVuQft0q6xBXo0FSmbt/zbzMDCy2J mIsAXeVRj1r9oIq3h2ntATRj+we3fMH72crqGprWpVDqnL8f7rKtMM1P5HvpHf3N2Wp6lZjUh f7+7r2vcMCzzgNMHGo/MQrPOmmG2pMVqtkAIVf5+9KVGHxWvLw3ERxwncHT+ZkgQsSelaHbsI rBVN9tOSzd74qG9e1g6iYcP1aQpjCmHCqUCEmNBPQ= X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Maxim Cournoyer wrote: > Hello Arvid, > > [...] > When writing the package definition for the Emacs Lead mode, the code > could be rewritten to refer to the absolute path of the > files/programs > it uses from the Lean project, by patching it with `substitute*' > uses, > for example. > > If that is not easy to do, another idea would be to create some kind > of > overlay directory which would flatly collect all the items needed > then > refer to that (the items would be symlinked to their real location). > See the `union-build' procedure of the (guix build union) module of > Guix. > > HTH! > > Maxim Hello Maxim, thanks for your response! The second idea is basically what I had in mind, as the Lean mode seems to depend on an actual file tree. Patching the emacs mode however looks quite simple, as all one needed to do is change the definition of lean-get-executable as defined in https://raw.githubusercontent.com/leanprover/lean-mode/master/lean-util.el . I might take a closer look and write a simple patch at some point, but up to that point, it appears that just using ~/.guix-profile as a root directory works as well, or at least doesn't raise any errors when type checking etc. Again, thanks for feedback! -- Arvid From unknown Tue Sep 09 21:32:53 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Arvid Marx Subject: bug#39020: closed (Re: [bug#39020] Lean won't work with the emacs mode) Message-ID: References: <87k15vow4c.fsf@gnu.org> <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> X-Gnu-PR-Message: they-closed 39020 X-Gnu-PR-Package: guix-patches Reply-To: 39020@debbugs.gnu.org Date: Mon, 13 Jan 2020 22:01:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1578952862-12513-1" This is a multi-part message in MIME format... ------------=_1578952862-12513-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #39020: Lean won't work with the emacs mode which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 39020@debbugs.gnu.org. --=20 39020: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D39020 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1578952862-12513-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 39020-done) by debbugs.gnu.org; 13 Jan 2020 22:00:16 +0000 Received: from localhost ([127.0.0.1]:60265 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ir7ku-0003Ef-Bg for submit@debbugs.gnu.org; Mon, 13 Jan 2020 17:00:16 -0500 Received: from eggs.gnu.org ([209.51.188.92]:58208) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ir7kq-0003E9-9u for 39020-done@debbugs.gnu.org; Mon, 13 Jan 2020 17:00:15 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:33110) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ir7kk-00018r-P7; Mon, 13 Jan 2020 17:00:06 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=58224 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ir7kj-0003fF-PX; Mon, 13 Jan 2020 17:00:06 -0500 From: Brett Gilio To: Arvid Marx Subject: Re: [bug#39020] Lean won't work with the emacs mode References: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> <87woa3uesq.fsf@gmail.com> <235c2b1104ffbc9bc72b777edc61c8caad541a00.camel@logicandtypes.org> Date: Mon, 13 Jan 2020 16:00:03 -0600 In-Reply-To: <235c2b1104ffbc9bc72b777edc61c8caad541a00.camel@logicandtypes.org> (Arvid Marx's message of "Wed, 08 Jan 2020 15:18:14 +0100") Message-ID: <87k15vow4c.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 39020-done Cc: 39020-done@debbugs.gnu.org, Maxim Cournoyer X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Arvid Marx writes: > Maxim Cournoyer wrote: >> Hello Arvid, >> >> [...] >> When writing the package definition for the Emacs Lead mode, the code >> could be rewritten to refer to the absolute path of the >> files/programs >> it uses from the Lean project, by patching it with `substitute*' >> uses, >> for example. >> >> If that is not easy to do, another idea would be to create some kind >> of >> overlay directory which would flatly collect all the items needed >> then >> refer to that (the items would be symlinked to their real location). >> See the `union-build' procedure of the (guix build union) module of >> Guix. >> >> HTH! >> >> Maxim > > Hello Maxim, > > thanks for your response! The second idea is basically what I had in > mind, as the Lean mode seems to depend on an actual file tree. Patching > the emacs mode however looks quite simple, as all one needed to do is > change the definition of lean-get-executable as defined in > https://raw.githubusercontent.com/leanprover/lean-mode/master/lean-util.el > . I might take a closer look and write a simple patch at some point, > but up to that point, it appears that just using ~/.guix-profile as a > root directory works as well, or at least doesn't raise any errors when > type checking etc. > > Again, thanks for feedback! > > -- > > Arvid > > > > > Closing. -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE] ------------=_1578952862-12513-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 7 Jan 2020 19:06:42 +0000 Received: from localhost ([127.0.0.1]:49341 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iouBd-0002hr-Sn for submit@debbugs.gnu.org; Tue, 07 Jan 2020 14:06:42 -0500 Received: from lists.gnu.org ([209.51.188.17]:58866) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1iotzH-0002Nd-NU for submit@debbugs.gnu.org; Tue, 07 Jan 2020 13:53:55 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:38538) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iotzG-0002t2-Gu for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:55 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,RCVD_IN_DNSWL_NONE autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iotzF-00020D-KL for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:54 -0500 Received: from mout.kundenserver.de ([212.227.126.187]:51987) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iotzF-0001yA-BC for guix-patches@gnu.org; Tue, 07 Jan 2020 13:53:53 -0500 Received: from DESKTOP-KHP2F58 ([93.255.126.7]) by mrelayeu.kundenserver.de (mreue011 [212.227.15.167]) with ESMTPSA (Nemesis) id 1MirX2-1jIRuE1mSK-00eteK for ; Tue, 07 Jan 2020 19:53:50 +0100 Message-ID: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> Subject: Lean won't work with the emacs mode From: Arvid Marx To: guix-patches@gnu.org Date: Tue, 07 Jan 2020 19:53:49 +0100 Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.30.5 (3.30.5-1.fc29) MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Provags-ID: V03:K1:J2ujtxdtya9LyBa3WE3xW6GkRakswRy3hiHf4mwGep+0FW7SVrQ X3VKZXAA2J9jPFG7SYUp0LJdyyzsKvWyQF5soZ8ZePZzyC0d3nSKq9OEgdZPSTvbr/bCMak SfJIbhtS0QEjU4yKwq72K1kwsy4iTBFFq/siggh+CP839oOdAlagfG0fC/DLUXZxPjCo/jL xoLSjy3b9hJdNJT9KpCWw== X-UI-Out-Filterresults: notjunk:1;V03:K0:F9597yLtpuE=:eZSUbnidkCAkyK20hY54I+ OXsGHiR3QFtQpdZN5Xx9Lz/dpN2UA4In4qKaePBAJbdIGo/J7hd78BtcbiGpO3QYDhq4523iC s8KKeBxz1CGps+x24NZkwYya+KCxGJZAYELVzqwXLinDTdM3f9Dv9GQH3GqH1d6+rLXRAl3wu 7a513VE0XOYWuDXbEjwieepYImsSQ9jl4ekZYH5KeXO7DiUN7PvfGfWuSokh8IU0s63FpC15E OAl2dtXUDc+LB8Gj1AIA4fYlXkoqz5KW2FhCMbyAsUi7fbdSV/YcN8SxYoyabsPe/aAcCTwfa d0IruV4U1n3HtpjLP0CHffSaRamlGxJOPEZZaUMCR78yVyfBP0MHhAo59ccX6dt5n2uvGj7+a tXeYCWhNOOwkKHsUhj4XbMRRNxXFSpAddCGrB1QH0kSFD32AflB0LTYvNUYESZmRiKE4wMB9v jbaGWpuRSMDyAJGX5mpzkWQJNaxqY7zQTuI/oy8F5TyxG3hAsbpfiYOW8/F83MMUA9WepwcCS E91hcDXjGvTUwIAEKbexMxYdrsNlZsCId65rgiovmeCumEdbjiewRkhN9kQHRG2Kk35f/f+Hc dYzGzYTMzsJoTmtzmBJASC3p7DMo9gPyfILA6BsprZ7PhwEw4eLv7+KEUSzHjF9FXgbUtsUkM NXlmzjGyy1v1tpz4rlhp+yVeO85cuNqTdHVE3GE7OnW7gClmbVxycb2bjZSUZLYiYJfXGwHZd sBWYD2LMVE/vgCbeO9E4J33Eynjaszdo45OS4ikaHEons5uITcPu3QWfSpRADAl2TYNqAIH/q xIBvHmXusY+eWrG+0zSS4Z0PuA5jofUWHDQRNfbeljCHe6sD60cN3UXxAKMLyz8AM2tKL+1wc 80hBjMhSN8Hno/bATcO7BJtqMqGF+GwaKzqu7j3Lo= X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 212.227.126.187 X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: submit X-Mailman-Approved-At: Tue, 07 Jan 2020 14:06:40 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) The emacs mode for Lean (which doesn't appear to be packaged yet, but of course works via MELPA etc.) expects some sort of root directory for Lean, which is not given simply because binaries and other files are put into separate directories. This of course makes Lean impossible to use as intended. However, I'm not quite sure how this would be fixed in practice, as I'm not aware of any suitable directory hierarchy in such a case. Any ideas? -- Arvid ------------=_1578952862-12513-1--