From debbugs-submit-bounces@debbugs.gnu.org Tue Jan 07 14:06:42 2020 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 From debbugs-submit-bounces@debbugs.gnu.org Tue Jan 07 14:12:00 2020 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 To: Arvid Marx Subject: Re: [bug#39020] Lean won't work with the emacs mode 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-Debbugs-Envelope-To: 39020 Cc: 39020@debbugs.gnu.org, bandali@gnu.org 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 debbugs-submit-bounces@debbugs.gnu.org Tue Jan 07 16:39:46 2020 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 To: Arvid Marx Subject: Re: [bug#39020] Lean won't work with the emacs mode 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-Debbugs-Envelope-To: 39020 Cc: 39020@debbugs.gnu.org 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 debbugs-submit-bounces@debbugs.gnu.org Wed Jan 08 09:18:24 2020 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> Subject: Re: [bug#39020] Lean won't work with the emacs mode From: Arvid Marx To: Maxim Cournoyer 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-Debbugs-Envelope-To: 39020 Cc: 39020@debbugs.gnu.org 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 debbugs-submit-bounces@debbugs.gnu.org Mon Jan 13 17:00:16 2020 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] From unknown Tue Sep 09 21:33:06 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 11 Feb 2020 12:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator