From unknown Fri Aug 15 04:08:31 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#27195 <27195@debbugs.gnu.org> To: bug#27195 <27195@debbugs.gnu.org> Subject: Status: Add search-paths for coq libraries Reply-To: bug#27195 <27195@debbugs.gnu.org> Date: Fri, 15 Aug 2025 11:08:31 +0000 retitle 27195 Add search-paths for coq libraries reassign 27195 guix-patches submitter 27195 julien lepiller severity 27195 normal thanks From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 02 04:11:47 2017 Received: (at submit) by debbugs.gnu.org; 2 Jun 2017 08:11:47 +0000 Received: from localhost ([127.0.0.1]:50401 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dGhgR-0003om-8U for submit@debbugs.gnu.org; Fri, 02 Jun 2017 04:11:47 -0400 Received: from eggs.gnu.org ([208.118.235.92]:35122) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dGhgP-0003oY-02 for submit@debbugs.gnu.org; Fri, 02 Jun 2017 04:11:45 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dGhgI-00026o-Ef for submit@debbugs.gnu.org; Fri, 02 Jun 2017 04:11:39 -0400 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,T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:53612) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dGhgI-00026Z-Ap for submit@debbugs.gnu.org; Fri, 02 Jun 2017 04:11:38 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:54299) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dGhgH-0001IH-49 for guix-patches@gnu.org; Fri, 02 Jun 2017 04:11:38 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dGhgC-00021R-4A for guix-patches@gnu.org; Fri, 02 Jun 2017 04:11:37 -0400 Received: from dau94-h03-89-91-205-84.dsl.sta.abo.bbox.fr ([89.91.205.84]:46364 helo=skaro.lepiller.eu) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dGhgB-0001xr-La for guix-patches@gnu.org; Fri, 02 Jun 2017 04:11:32 -0400 Received: from localhost (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTP id DF59A81502 for ; Fri, 2 Jun 2017 10:11:27 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1496391087; bh=0c3nQ83MJhBcUk9EVS+mUlrSJLP2/Et5RVU5F+SfM0k=; h=Date:From:To:Subject:From; b=WWEIKQj0uGWVwk0K3Syd2L7Ne/QLgH1hBEbp6le43iRW0bpZwLC36i+sIWqh4HplU 31XsMBo75pR0W4ej7ubM6+JFqu35jnmReDEwezCOJ8mU3hec+q71mqDyG6bLKXcekF QTBkU1IotiplN7v2BAuGjoS++aWo4mBwgO2xG6u8fnmunzARP8GsIdeMr+yklnd2cU VDc58yngYGsv0riobq0lCIXBZ9InGRqZEOxkOrjq5iLUtav2C5vGpQXB5l3yjBmyGJ RPlDYlioMDCLBpWzvF/wY9Sf0kkp+2pdxSckJR75C6nZMnAdF8wa2rckjPI9XNpNqd U3Yl1wm9JXgSnxiOt73ZEj8vyG6ptekXKhx4OCml4guLlQLg8VTzyMUSq3CuH36vgT kd+nbgJeWC4s2gcG9mVGZ63G5S+cHZZKOh1PoY9XGsTzuLIIDTiFmeyfRE1xzd5nC1 XWCQgvOh/jaos6F0LnAMC4b+QeyATBpDJ6g/pwnrRlm11N6bs83/5S9CPnuzDQ1kGK PFVlyEsupd5LfKGM/xCaME4wd0GHPclAb7XXd81Gb/s5sS81NjNXZm+2RMMkZTx8Nh 7LAmSrjLdxcXM0azLh11ETTTGh+H76pc8nShE3EqIPVtMcayRGYiAiDnYcrGZMZzlK 3WgaB6r5gRUC3fV+w0nultsk= X-Virus-Scanned: Debian amavisd-new at lepiller.eu Received: from skaro.lepiller.eu ([127.0.0.1]) by localhost (lepiller.eu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id qdKW11WDWTfw for ; Fri, 2 Jun 2017 10:11:24 +0200 (CEST) Received: from webmail.lepiller.eu (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTPA id C89CF7F9CC for ; Fri, 2 Jun 2017 10:11:23 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1496391083; bh=0c3nQ83MJhBcUk9EVS+mUlrSJLP2/Et5RVU5F+SfM0k=; h=Date:From:To:Subject:From; b=BC+amPIbuJeOlNfrf/9HFhSIFxgMiTPPA1kFYhn2itovbX+XGymWTPJXx2PqKSXsv bvyqg6hTkAQGWe7ZWyx65+Nc0xX9B0cg+TXAfraZ3b+YmT+KfsinTKbVXQthxn7vnp ZxjbRMdLvOTUQI+/tdcGKSVjqSLVvbqy9UWq37eUbNxKlPmp0ePG+8s/vRRwNcGGky 7YKpgwAnZyRX/aeyZ5pSSIKV1PehpZaoAGQiIkF/+cPopQvftkki1bQno7JSUIEg8f OdPAKVYyZEjhZ3KZv3dplU/G2+xYQnGS/mZ3FyvDe139cs3r2HmSSbK44W3+JRi4Sn daB9J+a2tm8Yy4zqhdpbutJSIMssyQsihZRhq+tN3Rd4lRS9KrZkBDy89WqmPxw50M rqIers7IzCw0MroiH+BpKmruxzIDS4AjHbTxNJxdjaMOQNl5GSAlk7q+JJKUj5bpQz usIVnAyi+a+UVx0+uioPcRlJcBgJ69XcPbub/CfRnU3TTgwkJQAzLZ0XMGyR1Cflh4 df779jtDUMET6SI+ew2MgWOqpgw0aXQZ21dBOUBlB934ZihH5I27CGkvH193jMy4Oh Pzg4lBK7+GRZiUwdXKeBW+J1AldLUMRLx/gEL06cP1WWk4nIazPl3E9vQ8+anCyP33 92JmBm+Yf2XcVIxx96O9MpvI= MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=_73ee55eddcbc6109fa1fff0c360a7061" Date: Fri, 02 Jun 2017 10:11:23 +0200 From: julien lepiller To: guix-patches@gnu.org Subject: Add search-paths for coq libraries Message-ID: X-Sender: julien@lepiller.eu User-Agent: Roundcube Webmail/1.2.5 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit 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: -4.0 (----) --=_73ee55eddcbc6109fa1fff0c360a7061 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed Hi, here is a patch to set COQPATH, the environment variable used by coq to find external libraries. --=_73ee55eddcbc6109fa1fff0c360a7061 Content-Transfer-Encoding: base64 Content-Type: text/x-diff; name=0001-gnu-coq-Add-search-paths-for-coq-libraries.patch Content-Disposition: attachment; filename=0001-gnu-coq-Add-search-paths-for-coq-libraries.patch; size=937 RnJvbSA3NDg2YTE2OWJkZmEwZDRjNWYyODc0MDViNmQ1ZmNjZjlkYmNkMWZhIE1vbiBTZXAgMTcg MDA6MDA6MDAgMjAwMQpGcm9tOiBKdWxpZW4gTGVwaWxsZXIgPGp1bGllbkBsZXBpbGxlci5ldT4K RGF0ZTogVGh1LCAxIEp1biAyMDE3IDE3OjUyOjEyICswMjAwClN1YmplY3Q6IFtQQVRDSF0gZ251 OiBjb3E6IEFkZCBzZWFyY2gtcGF0aHMgZm9yIGNvcSBsaWJyYXJpZXMuCgoqIGdudS9wYWNrYWdl cy9vY2FtbC5zY20gKGNvcSlbbmF0aXZlLXNlYXJjaC1wYXRoc106IE5ldyBmaWVsZC4KLS0tCiBn bnUvcGFja2FnZXMvb2NhbWwuc2NtIHwgNCArKysrCiAxIGZpbGUgY2hhbmdlZCwgNCBpbnNlcnRp b25zKCspCgpkaWZmIC0tZ2l0IGEvZ251L3BhY2thZ2VzL29jYW1sLnNjbSBiL2dudS9wYWNrYWdl cy9vY2FtbC5zY20KaW5kZXggODYzZTM2N2E1Li5hMzQ3NWUyYjkgMTAwNjQ0Ci0tLSBhL2dudS9w YWNrYWdlcy9vY2FtbC5zY20KKysrIGIvZ251L3BhY2thZ2VzL29jYW1sLnNjbQpAQCAtNDQ4LDYg KzQ0OCwxMCBAQCB3cml0dGVuIGluIE9iamVjdGl2ZSBDYW1sLiIpCiAgICAgICAgICAgICAgIChz aGEyNTYKICAgICAgICAgICAgICAgIChiYXNlMzIKICAgICAgICAgICAgICAgICAiMHd5eXdpYTBk YXJhazJ6bWM1djByYTlybjBiOXdod2RmaWFocmFsbTh2NXphNDk5czh3MyIpKSkpCisgICAgKG5h dGl2ZS1zZWFyY2gtcGF0aHMKKyAgICAgKGxpc3QgKHNlYXJjaC1wYXRoLXNwZWNpZmljYXRpb24K KyAgICAgICAgICAgICh2YXJpYWJsZSAiQ09RUEFUSCIpCisgICAgICAgICAgICAoZmlsZXMgKGxp c3QgImxpYi9jb3EiICJsaWIvY29xL3VzZXItY29udHJpYiIpKSkpKQogICAgIChidWlsZC1zeXN0 ZW0gZ251LWJ1aWxkLXN5c3RlbSkKICAgICAobmF0aXZlLWlucHV0cwogICAgICBgKCgidGV4bGl2 ZSIgLHRleGxpdmUpCi0tIAoyLjEzLjAKCg== --=_73ee55eddcbc6109fa1fff0c360a7061-- From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 02 11:55:29 2017 Received: (at 27195) by debbugs.gnu.org; 2 Jun 2017 15:55:29 +0000 Received: from localhost ([127.0.0.1]:51752 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dGov5-0008G7-Hu for submit@debbugs.gnu.org; Fri, 02 Jun 2017 11:55:28 -0400 Received: from eggs.gnu.org ([208.118.235.92]:59321) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dGov0-0008Fq-8B for 27195@debbugs.gnu.org; Fri, 02 Jun 2017 11:55:23 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dGouq-0005FI-6n for 27195@debbugs.gnu.org; Fri, 02 Jun 2017 11:55:13 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:57621) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dGouq-0005FD-4A; Fri, 02 Jun 2017 11:55:08 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:37516 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dGoup-0007O9-DG; Fri, 02 Jun 2017 11:55:07 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: julien lepiller Subject: Re: bug#27195: Add search-paths for coq libraries References: X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 14 Prairial an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Fri, 02 Jun 2017 17:55:04 +0200 In-Reply-To: (julien lepiller's message of "Fri, 02 Jun 2017 10:11:23 +0200") Message-ID: <87d1am5qqv.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27195 Cc: 27195@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: -5.0 (-----) julien lepiller skribis: > From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001 > From: Julien Lepiller > Date: Thu, 1 Jun 2017 17:52:12 +0200 > Subject: [PATCH] gnu: coq: Add search-paths for coq libraries. > > * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field. > --- > gnu/packages/ocaml.scm | 4 ++++ > 1 file changed, 4 insertions(+) > > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index 863e367a5..a3475e2b9 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -448,6 +448,10 @@ written in Objective Caml.") > (sha256 > (base32 > "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"))= )) > + (native-search-paths > + (list (search-path-specification > + (variable "COQPATH") > + (files (list "lib/coq" "lib/coq/user-contrib"))))) Is =E2=80=9Clib/coq/user-contrib=E2=80=9D a widespread convention? Looks u= nusual. Apart from that LGTM, thanks! Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Wed Jun 07 04:03:12 2017 Received: (at 27195-done) by debbugs.gnu.org; 7 Jun 2017 08:03:12 +0000 Received: from localhost ([127.0.0.1]:60276 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dIVvr-0000fD-Pi for submit@debbugs.gnu.org; Wed, 07 Jun 2017 04:03:11 -0400 Received: from 89-92-10-219.hfc.dyn.abo.bbox.fr ([89.92.10.219]:50432 helo=skaro.lepiller.eu) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dIVvp-0000ez-M1 for 27195-done@debbugs.gnu.org; Wed, 07 Jun 2017 04:03:10 -0400 Received: from localhost (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTP id 8ED7881665 for <27195-done@debbugs.gnu.org>; Wed, 7 Jun 2017 10:03:02 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1496822582; bh=CXZ4aFqxx1dmkPCBij45V/N325uRJjp1PrDm7AG4P3E=; h=Date:From:To:Subject:In-Reply-To:References:From; b=SCm577hirJENVeKdeQ2purzuiWQTfV/LYxS8bwn3rZJxUhEh/MzuMRFIyMkQ9PykA aIS/c8+erQ8okc45qBLYCDei19bXczOOvr+rH5KQMwWusO61RxmxAQlDYMD9bEjZbv 58kmgKwi65KeUBNT1w679rQPg6ffPRhA6ripDJUdIMLuJEIXccf++I5I2dP9nc9Ye+ jh6dbnrwYAGfWBYWamyt8R6I37TYlmafGBPlEqEf96fcAh2/HS3qfw0ZPB93+pkHHh lEHpwzlCqJq+1Xhftu6jJyCEjdDDXaqMf1pTkB58etZ23yXiz+m0kLpiiMjREAn2dg fc9Syqffaq1Z2dsldxA2eXQHWZNuLrNdZhGT79QPRqisjKLxDKaUW48dF0TyPzitR8 jXCvgTJax7LWGdRwdN5wuXejZfkXCo6g1e0r8f3Y2q6Mr9I1avroxsIu077RpVoclx HZSG4KqXD2R+phgwknkwOfmcZ8HMz7CZmRQXeqjzEaISP8/3r6yE7M/UkttKST0hjE ZOfnbJ0sfZh1W4gJU8n/YFVxk+VC+AE0e6D4VYoMXYAEz7Z9Y7Dugl50r9U4SBlAZ4 AFooCM1bMxX3dNzql566xgiT4pdjax3nKmcp0zuzeWDWCeaONZLUcxO70xruhyyTVg SsY5Vc+sqAursjRgdDgKvHXY= X-Virus-Scanned: Debian amavisd-new at lepiller.eu Received: from skaro.lepiller.eu ([127.0.0.1]) by localhost (lepiller.eu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id XTgz1Q12oqDF for <27195-done@debbugs.gnu.org>; Wed, 7 Jun 2017 10:03:00 +0200 (CEST) Received: from webmail.lepiller.eu (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTPA id 74A557FB3D for <27195-done@debbugs.gnu.org>; Wed, 7 Jun 2017 10:02:59 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1496822579; bh=CXZ4aFqxx1dmkPCBij45V/N325uRJjp1PrDm7AG4P3E=; h=Date:From:To:Subject:In-Reply-To:References:From; b=ir8riM9pK+Nvty5/WJmmyfEoGAcCmx6yE9AxaqEAzlvU3vQjb1grciJwqJah+G5CT gAmerrrxzigtK5LREEU99Er/3xeqizCZ/TchBFf16tUJB355RCw6rffYc0dvZ67a52 8D/7u9QTls0AUUu4/mkPsTHj1GpTRjm0/wuN8jhfsOvEQHiaWlDKjrvoIW29sow8mD 08Uf7dwuzOndVJJK0HUNS76oBgl6C4H2zNTwPLqu88vEabdUE/KaNwoV7bT+8dBXVv ItZMMAzeI2b7JRothpKtylVCGbtNWJ33ee7nb2BtQUeNBW7jog6LPM9XcAMPfMHBtc qR8oTM8UnV5zohYr0RJI59R3dpMCSoOlBVl++G4N7LOe4xtQsWbsx2YKDp2+GRjWZa b5HLMuW2m7gYvr8uKZIzF7iU+uclWiZYkO8tbH64wmWUY2j8IiNnRATeBuSxn3uaMr KJHZywunYYhF6Dqn0V1xXqPS1fmxrdFQuOEYU6mIrY8vRHyy7RqxiNDboIjqLJgz7T Uw4omj9v8XPnFA2WX7qte+DDE7SJuY5R5g0DSiPEaqsxOHwRTDh2L0ayV2skP7vlCm 8ZYHuRZZ0Js1goqtiL2/o6ywjfawGG4WsW0ZJ8LHhdAi+mlAKXBQp49bZG8q2C2yPw hJOcB5uPrbVO0xqskkPNARoA= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Date: Wed, 07 Jun 2017 10:02:59 +0200 From: julien lepiller To: 27195-done@debbugs.gnu.org Subject: Re: bug#27195: Add search-paths for coq libraries In-Reply-To: <87d1am5qqv.fsf@gnu.org> References: <87d1am5qqv.fsf@gnu.org> Message-ID: <6f9bf64ed74ea44aac98f04071d043da@lepiller.eu> X-Sender: julien@lepiller.eu User-Agent: Roundcube Webmail/1.2.5 X-Spam-Score: 4.9 (++++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le 2017-06-02 17:55, ludo@gnu.org a écrit : > julien lepiller skribis: > >> From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001 >> From: Julien Lepiller >> Date: Thu, 1 Jun 2017 17:52:12 +0200 >> Subject: [PATCH] gnu: coq: Add search-paths for coq libraries. >> >> * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field. >> --- >> gnu/packages/ocaml.scm | 4 ++++ >> 1 file changed, 4 insertions(+) >> >> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm >> index 863e367a5..a3475e2b9 100644 >> --- a/gnu/packages/ocaml.scm >> +++ b/gnu/packages/ocaml.scm >> @@ -448,6 +448,10 @@ written in Objective Caml.") >> (sha256 >> (base32 >> >> "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3")))) >> + (native-search-paths >> + (list (search-path-specification >> + (variable "COQPATH") >> + (files (list "lib/coq" "lib/coq/user-contrib"))))) > > Is “lib/coq/user-contrib” a widespread convention? Looks unusual. > > Apart from that LGTM, thanks! > > Ludo’. [...] Content analysis details: (4.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 TVD_RCVD_IP Message was received from an IP address 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [89.92.10.219 listed in zen.spamhaus.org] 0.0 T_DKIM_INVALID DKIM-Signature header exists but is not valid 1.0 KHOP_DYNAMIC Relay looks like a dynamic address 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS X-Debbugs-Envelope-To: 27195-done 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: 4.9 (++++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le 2017-06-02 17:55, ludo@gnu.org a écrit : > julien lepiller skribis: > >> From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001 >> From: Julien Lepiller >> Date: Thu, 1 Jun 2017 17:52:12 +0200 >> Subject: [PATCH] gnu: coq: Add search-paths for coq libraries. >> >> * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field. >> --- >> gnu/packages/ocaml.scm | 4 ++++ >> 1 file changed, 4 insertions(+) >> >> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm >> index 863e367a5..a3475e2b9 100644 >> --- a/gnu/packages/ocaml.scm >> +++ b/gnu/packages/ocaml.scm >> @@ -448,6 +448,10 @@ written in Objective Caml.") >> (sha256 >> (base32 >> >> "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3")))) >> + (native-search-paths >> + (list (search-path-specification >> + (variable "COQPATH") >> + (files (list "lib/coq" "lib/coq/user-contrib"))))) > > Is “lib/coq/user-contrib” a widespread convention? Looks unusual. > > Apart from that LGTM, thanks! > > Ludo’. [...] Content analysis details: (4.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [89.92.10.219 listed in zen.spamhaus.org] 0.0 T_DKIM_INVALID DKIM-Signature header exists but is not valid 1.0 KHOP_DYNAMIC Relay looks like a dynamic address 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS Le 2017-06-02 17:55, ludo@gnu.org a écrit : > julien lepiller skribis: > >> From 7486a169bdfa0d4c5f287405b6d5fccf9dbcd1fa Mon Sep 17 00:00:00 2001 >> From: Julien Lepiller >> Date: Thu, 1 Jun 2017 17:52:12 +0200 >> Subject: [PATCH] gnu: coq: Add search-paths for coq libraries. >> >> * gnu/packages/ocaml.scm (coq)[native-search-paths]: New field. >> --- >> gnu/packages/ocaml.scm | 4 ++++ >> 1 file changed, 4 insertions(+) >> >> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm >> index 863e367a5..a3475e2b9 100644 >> --- a/gnu/packages/ocaml.scm >> +++ b/gnu/packages/ocaml.scm >> @@ -448,6 +448,10 @@ written in Objective Caml.") >> (sha256 >> (base32 >> >> "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3")))) >> + (native-search-paths >> + (list (search-path-specification >> + (variable "COQPATH") >> + (files (list "lib/coq" "lib/coq/user-contrib"))))) > > Is “lib/coq/user-contrib” a widespread convention? Looks unusual. > > Apart from that LGTM, thanks! > > Ludo’. This is what the coq_makefile tool produces by default. I removed the "lib/coq" because this directory is used only for the standard library and it is already found correctly. "lib/coq" also creates a conflict in the build environment, which I cannot reproduce outside, but it seems that "lib/coq/user-contrib" alone works fine: I could build a few coq libraries and I'll send patches this evening. Pushed as 50cbbc9bd439c0db1cce6ba6d6a49de1d1f3bacd. From unknown Fri Aug 15 04:08:31 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 05 Jul 2017 11:24:03 +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