Received: (at 49607) by debbugs.gnu.org; 8 Dec 2022 00:42:52 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Wed Dec 07 19:42:52 2022 Received: from localhost ([127.0.0.1]:53167 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1p34zz-0005BC-SP for submit <at> debbugs.gnu.org; Wed, 07 Dec 2022 19:42:52 -0500 Received: from mail-4018.proton.ch ([185.70.40.18]:51857) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <attila@HIDDEN>) id 1p34zw-0005B6-8v for 49607 <at> debbugs.gnu.org; Wed, 07 Dec 2022 19:42:50 -0500 Date: Thu, 08 Dec 2022 00:42:31 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lendvai.name; s=protonmail2; t=1670460160; x=1670719360; bh=6eNFdMAatCseKY4F10lDG8RWqu2rlM7fjHJSNdJL00E=; h=Date:To:From:Subject:Message-ID:Feedback-ID:From:To:Cc:Date: Subject:Reply-To:Feedback-ID:Message-ID:BIMI-Selector; b=D3hNdwdWtMoVzKJlPX0pcb+1BAL7ntKl0/iKzgaDEZ8pWIRT6nMI9W+oMWzjOSOYD 3TnjEna0E3mTWgwsUw8+myXgKDVXn+/VZ2Pa6Ab2lRYTrV8yMbgKQFqJC+gR7MKVx6 Vq4UqjyP0/nQ8hPc6GnhufyVdjiPeUEn3pedL/JNWfCPgMWcsE1LJMLvJfS4l7hRBG 5+5cw/Lyr7u+Vt/b1I1yaSiyZOKMyjrzFECdutUuggCIEjoZ/0nWRACFDtLUClXcZB DdM18Ra+r2JIhHnPbU42ozZb/iUpdrBPb8XuyJECsAxHM4SVJKURSruNUhpiYx+Xp3 PzygevPiEb44w== To: "49607 <at> debbugs.gnu.org" <49607 <at> debbugs.gnu.org> From: Attila Lendvai <attila@HIDDEN> Subject: idris bootstrap, bailing out Message-ID: <VaTtupJJWSLJcMRYyviOZKsQz9fZTU8NJPSq1-fXMIxgh0muqi9oQh89bEq4qr450xVm94UlbPlUWAofkcb8KY1Da7eLYVpZkBnCsryMH3Y=@lendvai.name> Feedback-ID: 28384833:user:proton MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.0 (-) FTR, i have failed to inspire the idris maintainers with my refactor of the= idris build system, and my setup that enables chain-bootstrapping the enti= re idris language evolution all the way down from GHC. https://github.com/idris-lang/Idris2/pull/1990 i have also lost my initial interest in delving deep into idris, so i will = not pursue my idris related work anymore. i'm happy to help anyone who wants to pick up this work, though! i may even= get involved if there's someone else who steps up to champion the cause. --=20 =E2=80=A2 attila lendvai =E2=80=A2 PGP: 963F 5D5F 45C7 DFCD 0A39 -- =E2=80=9CKnowledge makes a man unfit to be a slave.=E2=80=9D =09=E2=80=94 Frederick Douglass (1818=E2=80=931895), a former slave.
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 23 Aug 2022 12:37:26 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Tue Aug 23 08:37:26 2022 Received: from localhost ([127.0.0.1]:42893 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1oQT9p-0001SF-Nd for submit <at> debbugs.gnu.org; Tue, 23 Aug 2022 08:37:26 -0400 Received: from relay8-d.mail.gandi.net ([217.70.183.201]:51789) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <contact@HIDDEN>) id 1oQT9n-0001S0-Np for 49607 <at> debbugs.gnu.org; Tue, 23 Aug 2022 08:37:24 -0400 Received: (Authenticated sender: contact@HIDDEN) by mail.gandi.net (Postfix) with ESMTPA id 332481BF205 for <49607 <at> debbugs.gnu.org>; Tue, 23 Aug 2022 12:37:16 +0000 (UTC) MIME-Version: 1.0 Date: Tue, 23 Aug 2022 14:37:16 +0200 From: contact@HIDDEN To: 49607 <at> debbugs.gnu.org Subject: Package proposition: Idris2 v0.5.1 Message-ID: <d764852f8ff1019e8e6a96cb0f2dc2f3@HIDDEN> X-Sender: contact@HIDDEN Content-Type: multipart/mixed; boundary="=_d497460153c77fe7175c6bb91c460641" X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.7 (-) --=_d497460153c77fe7175c6bb91c460641 Content-Transfer-Encoding: 8bit Content-Type: text/plain; charset=UTF-8; format=flowed Dear Guixers, This package proposition follows from a discussion which last message was: https://lists.gnu.org/archive/html/help-guix/2022-08/msg00177.html — PHF --=_d497460153c77fe7175c6bb91c460641 Content-Transfer-Encoding: base64 Content-Type: text/x-diff; name=0001-gnu-Add-idris2-v0.5.1.patch Content-Disposition: attachment; filename=0001-gnu-Add-idris2-v0.5.1.patch; size=10349 RnJvbSAwNmQyMGUzZTZhZDJlMDhiMGFjZDI5MWNkNGRlM2VmZWVjNzZkZWI5IE1vbiBTZXAgMTcg MDA6MDA6MDAgMjAwMQpGcm9tOiA9P1VURi04P3E/UGllcnJlLUhlbnJ5PTIwRnI9QzM9QjZocmlu Zz89IDxjb250YWN0QHBoZnJvaHJpbmcuY29tPgpEYXRlOiBUdWUsIDIzIEF1ZyAyMDIyIDE0OjI5 OjIzICswMjAwClN1YmplY3Q6IFtQQVRDSF0gZ251OiBBZGQgaWRyaXMyIHYwLjUuMS4KCiogZ251 L3BhY2thZ2VzL2lkcmlzLnNjbSAoaWRyaXMyKTogTmV3IHZhcmlhYmxlLgotLS0KIGdudS9wYWNr YWdlcy9pZHJpcy5zY20gfCAxODAgKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysrKysr Ky0tLS0KIDEgZmlsZSBjaGFuZ2VkLCAxNjMgaW5zZXJ0aW9ucygrKSwgMTcgZGVsZXRpb25zKC0p CgpkaWZmIC0tZ2l0IGEvZ251L3BhY2thZ2VzL2lkcmlzLnNjbSBiL2dudS9wYWNrYWdlcy9pZHJp cy5zY20KaW5kZXggOGYwOGVkM2EzZS4uMzQ1MTEwMTJlYyAxMDA2NDQKLS0tIGEvZ251L3BhY2th Z2VzL2lkcmlzLnNjbQorKysgYi9nbnUvcGFja2FnZXMvaWRyaXMuc2NtCkBAIC0yMCwyMiArMjAs MzYgQEAKIDs7OyBZb3Ugc2hvdWxkIGhhdmUgcmVjZWl2ZWQgYSBjb3B5IG9mIHRoZSBHTlUgR2Vu ZXJhbCBQdWJsaWMgTGljZW5zZQogOzs7IGFsb25nIHdpdGggR05VIEd1aXguICBJZiBub3QsIHNl ZSA8aHR0cDovL3d3dy5nbnUub3JnL2xpY2Vuc2VzLz4uCiAKLShkZWZpbmUtbW9kdWxlIChnbnUg cGFja2FnZXMgaWRyaXMpCi0gICM6dXNlLW1vZHVsZSAoZ251IHBhY2thZ2VzKQotICAjOnVzZS1t b2R1bGUgKGdudSBwYWNrYWdlcyBoYXNrZWxsLWNoZWNrKQotICAjOnVzZS1tb2R1bGUgKGdudSBw YWNrYWdlcyBoYXNrZWxsLXdlYikKLSAgIzp1c2UtbW9kdWxlIChnbnUgcGFja2FnZXMgaGFza2Vs bC14eXopCi0gICM6dXNlLW1vZHVsZSAoZ251IHBhY2thZ2VzIGxpYmZmaSkKLSAgIzp1c2UtbW9k dWxlIChnbnUgcGFja2FnZXMgbXVsdGlwcmVjaXNpb24pCi0gICM6dXNlLW1vZHVsZSAoZ251IHBh Y2thZ2VzIG5jdXJzZXMpCi0gICM6dXNlLW1vZHVsZSAoZ251IHBhY2thZ2VzIHBlcmwpCi0gICM6 dXNlLW1vZHVsZSAoZ3VpeCBidWlsZC1zeXN0ZW0gZ251KQotICAjOnVzZS1tb2R1bGUgKGd1aXgg YnVpbGQtc3lzdGVtIGhhc2tlbGwpCi0gICM6dXNlLW1vZHVsZSAoZ3VpeCBkb3dubG9hZCkKLSAg Izp1c2UtbW9kdWxlIChndWl4IGdpdC1kb3dubG9hZCkKLSAgIzp1c2UtbW9kdWxlIChndWl4IHV0 aWxzKQotICAjOnVzZS1tb2R1bGUgKChndWl4IGxpY2Vuc2VzKSAjOnByZWZpeCBsaWNlbnNlOikK LSAgIzp1c2UtbW9kdWxlIChndWl4IHBhY2thZ2VzKSkKKyhkZWZpbmUtbW9kdWxlIChnbnUgcGFj a2FnZXMgaWRyaXMpKQorCisodXNlLW1vZHVsZXMKKyAoZ251KQorIChndWl4IGdleHApCisgKGd1 aXggdXRpbHMpCisgKGd1aXggc3RvcmUpCisgKGd1aXggZGVyaXZhdGlvbnMpCisgKGd1aXggcGFj a2FnZXMpCisgKGd1aXggZG93bmxvYWQpCisgKGd1aXggZ2l0LWRvd25sb2FkKQorIChndWl4IGJ1 aWxkLXN5c3RlbSBnbnUpCisgKGd1aXggYnVpbGQtc3lzdGVtIGhhc2tlbGwpCisgKGd1aXggYnVp bGQgdXRpbHMpCisgKChndWl4IGxpY2Vuc2VzKSAjOnByZWZpeCBsaWNlbnNlOikpCisKKyh1c2Ut cGFja2FnZS1tb2R1bGVzCisgaGFza2VsbC1jaGVjaworIGhhc2tlbGwtd2ViCisgaGFza2VsbC14 eXoKKyBsaWJmZmkKKyBuY3Vyc2VzCisgcGVybAorIGdjYworIG11bHRpcHJlY2lzaW9uCisgYmFz aAorIGJhc2UKKyBsaW51eAorIHB5dGhvbgorIGNoZXopCiAKIChkZWZpbmUtcHVibGljIGlkcmlz CiAgIChwYWNrYWdlCkBAIC0xNDYsNiArMTYwLDEzOCBAQCAoZGVmaW5lLXB1YmxpYyBpZHJpcwog RXBpZ3JhbSBhbmQgQWdkYS4iKQogICAgIChsaWNlbnNlIGxpY2Vuc2U6YnNkLTMpKSkKIAorKGRl ZmluZS1wdWJsaWMgaWRyaXMyCisgIChwYWNrYWdlCisgICAgKG5hbWUgImlkcmlzMiIpCisgICAg KHZlcnNpb24gIjAuNS4xIikKKyAgICAoc291cmNlIChvcmlnaW4KKyAgICAgICAgICAgICAgKG1l dGhvZCBnaXQtZmV0Y2gpCisgICAgICAgICAgICAgICh1cmkgKGdpdC1yZWZlcmVuY2UKKyAgICAg ICAgICAgICAgICAgICAgKHVybCAiaHR0cHM6Ly9naXRodWIuY29tL2lkcmlzLWxhbmcvSWRyaXMy IikKKyAgICAgICAgICAgICAgICAgICAgKGNvbW1pdCAoc3RyaW5nLWFwcGVuZCAidiIgdmVyc2lv bikpKSkKKyAgICAgICAgICAgICAgKHNoYTI1NgorICAgICAgICAgICAgICAgKGJhc2UzMgorICAg ICAgICAgICAgICAgICIwOWs1ZnhucGxwNmZ2Mzg3N3luejFsd3E5emFweGN4YnZmdmtuNmc2OHli MGl2cmZmOTc4IikpCisgICAgICAgICAgICAgIChmaWxlLW5hbWUgKGdpdC1maWxlLW5hbWUgbmFt ZSB2ZXJzaW9uKSkpKQorICAgIChidWlsZC1zeXN0ZW0gZ251LWJ1aWxkLXN5c3RlbSkKKyAgICAo YXJndW1lbnRzCisgICAgIChsaXN0ICM6bWFrZS1mbGFncyAjfihsaXN0ICJTQ0hFTUU9Y2hlei1z Y2hlbWUiCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChzdHJpbmctYXBwZW5kICJD Qz0iCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICMkKGNj LWZvci10YXJnZXQpKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAoc3RyaW5nLWFw cGVuZCAiUFJFRklYPSIKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgIyRvdXRwdXQpKQorICAgICAgICAgICAjOnBoYXNlcyAjfihtb2RpZnktcGhhc2VzICVz dGFuZGFyZC1waGFzZXMKKyAgICAgICAgICAgICAgICAgICAgICAgIChhZGQtYWZ0ZXIgJ3NldC1w YXRocyAncGF0Y2gtcGF0aHMKKyAgICAgICAgICAgICAgICAgICAgICAgICAgKGxhbWJkYSogXwor ICAgICAgICAgICAgICAgICAgICAgICAgICAgIChkZWZpbmUgKGFkZCB2YWx1ZSB2YXIpCisgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAobGV0ICgocHJldiAoZ2V0ZW52IHZhcikpKQorICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAoaWYgcHJldgorICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgKHNldGVudiB2YXIKKyAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgKHN0cmluZy1qb2luIChsaXN0IHByZXYgdmFsdWUpICI6IikpCisg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAoc2V0ZW52IHZhciB2YWx1ZSkpKSkK KyAgICAgICAgICAgICAgICAgICAgICAgICAgICAoYWRkIChzdHJpbmctYXBwZW5kICMkb3V0cHV0 ICIvbGliIikKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICJMRF9MSUJSQVJZX1BB VEgiKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgIChhZGQgKHN0cmluZy1hcHBlbmQgIyRv dXRwdXQgIi9iaW4iKSAiUEFUSCIpKSkKKyAgICAgICAgICAgICAgICAgICAgICAgIChhZGQtYWZ0 ZXIgJ3VucGFjayAncGF0Y2gtc2hlYmFuZ3MKKyAgICAgICAgICAgICAgICAgICAgICAgICAgKGxh bWJkYSogKCM6a2V5IGlucHV0cyAjOmFsbG93LW90aGVyLWtleXMpCisgICAgICAgICAgICAgICAg ICAgICAgICAgICAgKHN1YnN0aXR1dGUqICcoInNyYy9Db21waWxlci9TY2hlbWUvQ2hlelNlcC5p ZHIiCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgInNyYy9Db21w aWxlci9TY2hlbWUvQ2hlei5pZHIiCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgInNyYy9Db21waWxlci9TY2hlbWUvUmFja2V0LmlkciIKKyAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAiYm9vdHN0cmFwL2lkcmlzMl9hcHAvaWRyaXMy LnJrdCIKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAiYm9vdHN0 cmFwL2lkcmlzMl9hcHAvaWRyaXMyLnNzIikKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICgoIigjISkgKigvYmluL3NoKSIgXyBzaGViYW5nIGV4ZWMpCisgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgKHN0cmluZy1hcHBlbmQgc2hlYmFuZyAiICIKKyAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAoYXNzb2MtcmVmIGlucHV0cyAiYmFzaC1taW5p bWFsIikKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICBleGVj KSkpKSkKKyAgICAgICAgICAgICAgICAgICAgICAgIChkZWxldGUgJ2Jvb3RzdHJhcCkKKyAgICAg ICAgICAgICAgICAgICAgICAgIChkZWxldGUgJ2NvbmZpZ3VyZSkKKyAgICAgICAgICAgICAgICAg ICAgICAgIChhZGQtYmVmb3JlICdidWlsZCAnYm9vdHN0cmFwCisgICAgICAgICAgICAgICAgICAg ICAgICAgIChsYW1iZGEqICgjOmtleSBtYWtlLWZsYWdzICM6YWxsb3ctb3RoZXIta2V5cykKKyAg ICAgICAgICAgICAgICAgICAgICAgICAgICAoYXBwbHkgaW52b2tlICJtYWtlIiAiYm9vdHN0cmFw IiBtYWtlLWZsYWdzKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgIChhcHBseSBpbnZva2Ug Im1ha2UiICJpbnN0YWxsIiBtYWtlLWZsYWdzKSkpCisgICAgICAgICAgICAgICAgICAgICAgICAo cmVwbGFjZSAnYnVpbGQKKyAgICAgICAgICAgICAgICAgICAgICAgICAgKGxhbWJkYSogKCM6a2V5 IG1ha2UtZmxhZ3MgIzphbGxvdy1vdGhlci1rZXlzKQorICAgICAgICAgICAgICAgICAgICAgICAg ICAgIChhcHBseSBpbnZva2UgIm1ha2UiICJjbGVhbiIgbWFrZS1mbGFncykKKyAgICAgICAgICAg ICAgICAgICAgICAgICAgICAoYXBwbHkgaW52b2tlICJtYWtlIiAiYWxsIiBtYWtlLWZsYWdzKSkp CisgICAgICAgICAgICAgICAgICAgICAgICAoYWRkLWFmdGVyICdpbnN0YWxsICdwYXRjaC0vYmlu L2lkcmlzMgorICAgICAgICAgICAgICAgICAgICAgICAgICAobGFtYmRhKiBfCisgICAgICAgICAg ICAgICAgICAgICAgICAgICAgKGxldCAoKGlkcmlzMiAoc3RyaW5nLWFwcGVuZCAjJG91dHB1dCAi L2Jpbi8iCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAjJG5hbWUpKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChpZHJp czJfYXBwIChzdHJpbmctYXBwZW5kICMkb3V0cHV0CisgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICIvYmluL2lkcmlzMl9hcHAiKSkpCisgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAoZGVsZXRlLWZpbGUgaWRyaXMyKQorICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgKHJlbmFtZS1maWxlIChzdHJpbmctYXBwZW5kIGlkcmlzMl9hcHAKKyAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAiL2lk cmlzMi5zbyIpIGlkcmlzMikKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChkZWxldGUt ZmlsZS1yZWN1cnNpdmVseSBpZHJpczJfYXBwKSkpKQorICAgICAgICAgICAgICAgICAgICAgICAg KGFkZC1hZnRlciAncGF0Y2gtL2Jpbi9pZHJpczIgJ3dyYXAtaWRyaXMyCisgICAgICAgICAgICAg ICAgICAgICAgICAgIChsYW1iZGEqICgjOmtleSBpbnB1dHMgIzphbGxvdy1vdGhlci1rZXlzKQor ICAgICAgICAgICAgICAgICAgICAgICAgICAgIChsZXQqICgoY2hleiAoc3RyaW5nLWFwcGVuZCAo YXNzb2MtcmVmIGlucHV0cworICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgImNoZXotc2NoZW1lIikKKyAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIi9iaW4vY2hlei1zY2hlbWUiKSkKKyAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGlkcmlzMi1wcmVmaXggIyRvdXRwdXQp CisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChpZHJpczItdmVyc2lvbiAoc3Ry aW5nLWFwcGVuZAorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgIGlkcmlzMi1wcmVmaXggIi8iCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgIyRuYW1lICItIgorICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICMkdmVyc2lvbikpCisgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgIChpZHJpczItbGliIChzdHJpbmctYXBwZW5kIGlkcmlzMi12ZXJz aW9uCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICIvbGliIikpCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChp ZHJpczItc3VwcG9ydCAoc3RyaW5nLWFwcGVuZAorICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgIGlkcmlzMi12ZXJzaW9uICIvc3VwcG9ydCIpKQorICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAoaWRyaXMyLWJpbiAoc3RyaW5nLWFwcGVu ZCBpZHJpczItcHJlZml4CisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICIvYmluLyIKKyAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIyRuYW1lKSkpCisgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAod3JhcC1wcm9ncmFtIGlkcmlzMi1iaW4KKyAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGxpc3QgIkNIRVoiCisgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICc9CisgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChsaXN0IGNoZXopKQorICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAobGlzdCAiSURSSVMyX1BSRUZJ WCIKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgJz0K KyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGxpc3Qg aWRyaXMyLXByZWZpeCkpCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgIChsaXN0ICJJRFJJUzJfTElCUyIKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgJ3N1ZmZpeAorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAobGlzdCBpZHJpczItbGliKSkKKyAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgKGxpc3QgIklEUklTMl9EQVRBIgorICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAnc3VmZml4CisgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChsaXN0IGlkcmlzMi1z dXBwb3J0KSkKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGxp c3QgIklEUklTMl9QQUNLQUdFX1BBVEgiCisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICdzdWZmaXgKKyAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgKGxpc3QgaWRyaXMyLXZlcnNpb24pKQorICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAobGlzdCAiTERfTElCUkFSWV9QQVRIIgor ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAnc3VmZml4 CisgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChsaXN0 IGlkcmlzMi1saWIpKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAobGlzdCAiRFlMRF9MSUJSQVJZX1BBVEgiCisgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICdzdWZmaXgKKyAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgKGxpc3QgaWRyaXMyLWxpYikpKSkpKQorICAgICAgICAg ICAgICAgICAgICAgICAgKGFkZC1iZWZvcmUgJ2NoZWNrICdzZXQtSU5URVJBQ1RJVkUtSURSSVMy CisgICAgICAgICAgICAgICAgICAgICAgICAgIChsYW1iZGEqIF8KKyAgICAgICAgICAgICAgICAg ICAgICAgICAgICAoc2V0ZW52ICJJTlRFUkFDVElWRSIgIiIpCisgICAgICAgICAgICAgICAgICAg ICAgICAgICAgKHNldGVudiAiSURSSVMyIgorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgKHN0cmluZy1hcHBlbmQgIyRvdXRwdXQgIi9iaW4vIgorICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIyRuYW1lKSkpKQorICAgICAgICAgICAg ICAgICAgICAgICAgKGFkZC1hZnRlciAnYnVpbGQgJ2J1aWxkLWRvYworICAgICAgICAgICAgICAg ICAgICAgICAgICAobGFtYmRhKiAoIzprZXkgbWFrZS1mbGFncyAjOmFsbG93LW90aGVyLWtleXMp CisgICAgICAgICAgICAgICAgICAgICAgICAgICAgKGFwcGx5IGludm9rZSAibWFrZSIgImluc3Rh bGwtbGliZG9jcyIgbWFrZS1mbGFncykpKSkKKyAgICAgICAgICAgIzp0ZXN0LXRhcmdldCAidGVz dCIKKyAgICAgICAgICAgIzpwYXJhbGxlbC1idWlsZD8gI2YpKQorICAgIChpbnB1dHMgKGxpc3Qg Z2NjLTEyCisgICAgICAgICAgICAgICAgICBjaGV6LXNjaGVtZQorICAgICAgICAgICAgICAgICAg Z21wCisgICAgICAgICAgICAgICAgICBjb3JldXRpbHMKKyAgICAgICAgICAgICAgICAgIGJhc2gt bWluaW1hbAorICAgICAgICAgICAgICAgICAgcHl0aG9uKSkKKyAgICAoaG9tZS1wYWdlICJodHRw czovL3d3dy5pZHJpcy1sYW5nLm9yZy8iKQorICAgIChzeW5vcHNpcworICAgICAiUHJvZ3JhbW1p bmcgbGFuZ3VhZ2UgZGVzaWduZWQgdG8gZW5jb3VyYWdlIFR5cGUtRHJpdmVuIERldmVsb3BtZW50 IikKKyAgICAoZGVzY3JpcHRpb24KKyAgICAgIklkcmlzIGlzIGEgcHJvZ3JhbW1pbmcgbGFuZ3Vh Z2UgZGVzaWduZWQgdG8gZW5jb3VyYWdlIFR5cGUtRHJpdmVuIERldmVsb3BtZW50LgorCitJbiB0 eXBlLWRyaXZlbiBkZXZlbG9wbWVudCwgdHlwZXMgYXJlIHRvb2xzIGZvciBjb25zdHJ1Y3Rpbmcg cHJvZ3JhbXMuICBXZQordHJlYXQgdGhlIHR5cGUgYXMgdGhlIHBsYW4gZm9yIGEgcHJvZ3JhbSwg YW5kIHVzZSB0aGUgY29tcGlsZXIgYW5kIHR5cGUKK2NoZWNrZXIgYXMgb3VyIGFzc2lzdGFudCwg Z3VpZGluZyB1cyB0byBhIGNvbXBsZXRlIHByb2dyYW0gdGhhdCBzYXRpc2ZpZXMgdGhlCit0eXBl LiAgVGhlIG1vcmUgZXhwcmVzc2l2ZSB0aGUgdHlwZSBpcyB0aGF0IHdlIGdpdmUgdXAgZnJvbnQs IHRoZSBtb3JlCitjb25maWRlbmNlIHdlIGNhbiBoYXZlIHRoYXQgdGhlIHJlc3VsdGluZyBwcm9n cmFtIHdpbGwgYmUgY29ycmVjdC4iKQorICAgIChsaWNlbnNlIGxpY2Vuc2U6YnNkLTMpKSkKKwog OzsgSWRyaXMgbW9kdWxlcyB1c2UgdGhlIGdudS1idWlsZC1zeXN0ZW0gc28gdGhhdCB0aGUgSURS SVNfTElCUkFSWV9QQVRIIGlzIHNldC4KIChkZWZpbmUgKGlkcmlzLWRlZmF1bHQtYXJndW1lbnRz IG5hbWUpCiAgIGAoIzptb2R1bGVzICgoZ3VpeCBidWlsZCBnbnUtYnVpbGQtc3lzdGVtKQpAQCAt MTc4LDcgKzMyNCw3IEBAIChkZWZpbmUgKGlkcmlzLWRlZmF1bHQtYXJndW1lbnRzIG5hbWUpCiAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChhbmQgcGF0aCAo bWF0Y2ggKHN0YXQ6dHlwZSAoc3RhdCBwYXRoKSkKICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKCdkaXJlY3RvcnkgI3QpCiAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChfICNm KSkpKQotICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg IGlkcmlzLXBhdGgtZmlsZXMpKQorICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgaWRyaXMtcGF0aC1maWxlcykpCiAgICAgICAgICAgICAgICAgIChpbnN0YWxsLWNt ZCAoY29ucyogaWRyaXMtYmluCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg Ii0taWJjc3ViZGlyIiBpYmNzdWJkaXIKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAiLS1idWlsZCIgaXBrZwotLSAKMi4zNy4yCgo= --=_d497460153c77fe7175c6bb91c460641--
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 11 Jul 2022 10:42:09 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Mon Jul 11 06:42:09 2022 Received: from localhost ([127.0.0.1]:38455 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1oAqrg-0000cG-OX for submit <at> debbugs.gnu.org; Mon, 11 Jul 2022 06:42:08 -0400 Received: from mail-4323.proton.ch ([185.70.43.23]:12256) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <attila@HIDDEN>) id 1oAqre-0000bO-C9 for 49607 <at> debbugs.gnu.org; Mon, 11 Jul 2022 06:42:07 -0400 Date: Mon, 11 Jul 2022 10:41:51 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lendvai.name; s=protonmail; t=1657536119; x=1657795319; bh=U8DnP0qYNbsd4qaOEUojwhS63XjtnQjJzthXpByvdzI=; h=Date:To:From:Reply-To:Subject:Message-ID:Feedback-ID:From:To:Cc: Date:Subject:Reply-To:Feedback-ID:Message-ID; b=VqKHjAiUFbBSzb8zyV+g2hVKtzcdL5PFLyym18WIU78HwHMLpZrIS9+exRi5dl9VN 3F9Hw0a9/kgawAkBWksQT5GBoRfUhqeWLkw6dr0/UmaECU0ug4P8CGpVVM+kOjUiHf aSsasYHbDUmqu63EXqKF5z5NhDIMhKKmvuLoaj0XBaSFmv+4q9EIhgn/pXnxgC8Gem 9eubxaG7uC7Ji0yGOgbrBxcGDpUtd8QdFT3lBkU7cb8ZUOyura2qOcmSo3ZuOGoall Hom+m4oYXxfCvngWYtDifmnG9TX69KwCznF8Ljup6HI7UXIeTPO+lhwI2yEAUpd6On S6NJvBGQmnsrg== To: "49607 <at> debbugs.gnu.org" <49607 <at> debbugs.gnu.org> From: Attila Lendvai <attila@HIDDEN> Subject: why not to propagate gcc as a dependency Message-ID: <0c1ARp_e4AUtOIowwzYPjcMCL5GKNqsM346kXd7jT5ZFCNW-pnkVsxZ-jjk4OmwAAPdZhVjoscDrIgwMkXUbjhwYBfDjL5im2HiANjvVAXY=@lendvai.name> Feedback-ID: 28384833:user:proton MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Reply-To: Attila Lendvai <attila@HIDDEN> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.0 (-) please note this discussion: https://lists.gnu.org/archive/html/guix-devel/2022-07/msg00131.html the conclusion, roughly: it's better if the user can pick whichever c compi= ler they want, but to retain a slick user experience, maybe we should intro= duce an idris-toolchain package that does the propagation. - attila
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 18 May 2022 17:22:49 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Wed May 18 13:22:49 2022 Received: from localhost ([127.0.0.1]:33405 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1nrNNp-00050Q-LW for submit <at> debbugs.gnu.org; Wed, 18 May 2022 13:22:49 -0400 Received: from mail-40136.proton.ch ([185.70.40.136]:42946) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <attila@HIDDEN>) id 1nrNNl-000509-Cz for 49607 <at> debbugs.gnu.org; Wed, 18 May 2022 13:22:47 -0400 Date: Wed, 18 May 2022 17:22:29 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lendvai.name; s=protonmail3; t=1652894557; x=1653153757; bh=E6nv5YlbBQCPFgJPZit24lj1B+eyG40dN/7BKNcbpd4=; h=Date:To:From:Cc:Reply-To:Subject:Message-ID:In-Reply-To: References:Feedback-ID:From:To:Cc:Date:Subject:Reply-To: Feedback-ID:Message-ID; b=QEeesS07ZL+59LjOkz62v3WpyRbtotqkEity2FJtUwHeXdbnSbZauIDBHJ50QEEmr MD7W2/XG9EcukfHao2MhNndQKeslx+7fKue79abskWvQoQkA/meD5Qux/A3b9xyV2C nsKAU7t0PGJ2GX/qkAWUBdzvlaDQtYrAHv/42HjOoK1dN8hHk8xZL7EZ4UYQ3KV8wh E7idBaXvRG6O15A/5LGwCn2LtEFb7rbjE7+5zG3NSKtpvXX1ESWMN5ONWu5dzqZN2z 8gZNYAV/Z8ZyNJ+zFStb+0HOUKc6DJdtwKwidNWssCRcW4DtwFqKJRBZYI13uljV15 cvtCwPMt9LajQ== To: Eric Bavier <bavier@HIDDEN> From: Attila Lendvai <attila@HIDDEN> Subject: Re: [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Message-ID: <hW5tnoYmk2d1VetTjLgy84dE0CunRwTneZ6zQ1XUZTcSfqfl_TCB4tdE6ty9a3unpx7WYZGiH_pM7neOmpDLuXvNP83YOUcsNBZ6NppY-pE=@lendvai.name> In-Reply-To: <a699dba5537656f7047d2b337e87378e325b6943.camel@HIDDEN> References: <ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@HIDDEN> <20220428132801.8629-1-attila@HIDDEN> <a699dba5537656f7047d2b337e87378e325b6943.camel@HIDDEN> Feedback-ID: 28384833:user:proton MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 49607 Cc: 49607 <at> debbugs.gnu.org X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Reply-To: Attila Lendvai <attila@HIDDEN> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.0 (-) > > * gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for > > wrap-program). > > [phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for- > > target). > > --- > > > I believe this would prevent someone from effectively setting > `IDRIS_CC` to a different compiler from within their environment, > correct? I would like to leave that option available to users. Also, good point! and i think you're correct, because wrapper scripts set the val= ue unconditionally. would it work if we set CC instead? idris first tries IDRIS_CC, and then CC= (and then falls back to "cc"). or would you prefer to use substitute* in the build to replace cc =3D "cc" = with a full path to gcc in the source code of idris? > can this be a simple compiler reference, or does it need to be a > "toolchain compiler"? i'm unable to answer that, i don't know the difference. i just noticed that i can't use idris as-is when trying the examples, becau= se it couldn't invoke the c compiler to produce executables. this is my att= empt at fixing this issue. -- =E2=80=A2 attila lendvai =E2=80=A2 PGP: 963F 5D5F 45C7 DFCD 0A39 -- If ethics are pure subjective preference, then rape is just competing prefe= rences.
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 17 May 2022 20:04:37 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Tue May 17 16:04:37 2022 Received: from localhost ([127.0.0.1]:58103 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1nr3Qo-0005py-2t for submit <at> debbugs.gnu.org; Tue, 17 May 2022 16:04:37 -0400 Received: from mout02.posteo.de ([185.67.36.66]:37731) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <bavier@HIDDEN>) id 1nr3Ql-0005ph-OD for 49607 <at> debbugs.gnu.org; Tue, 17 May 2022 16:04:32 -0400 Received: from submission (posteo.de [185.67.36.169]) by mout02.posteo.de (Postfix) with ESMTPS id BF011240107 for <49607 <at> debbugs.gnu.org>; Tue, 17 May 2022 22:04:25 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1652817865; bh=KgHQ9DE9RPjy75vtj6C3+eXEr1ek+nuZBZeUbGiy8Ds=; h=Subject:From:To:Date:From; b=BIvkxEMyucQJsJGf2AfE+BevkF334Hb2dOgcmESZMBvElePp1EKCvTYymTyQHGDiY ougBJGOQQcGnCMSUcaIT2xIMclbEv2OtyPLghQFVAHnb5tbNKij5TaL8pl4YFzVNh1 JAtXl91JZm9iUxBsykmXAsjdvjiHInYCYVEfqEZ2BkCMD/mdpj2OHPW4GWN+owgfVO VfdQGMX7EFCIGpkAph7NqMBcPThWA2//3suUOTdqaT4z7sCQIM13xhgyfufAoBUEmc OH7q9o+RezRv/qdlvDZva5YyfBC5tcV584yIMiyls+bws1pZTyrx23H6nXHDyxEPbc 7dxW3cPJZTlrg== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4L2nBw32Zpz9rxG; Tue, 17 May 2022 22:04:24 +0200 (CEST) Message-ID: <a699dba5537656f7047d2b337e87378e325b6943.camel@HIDDEN> Subject: Re: [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC From: Eric Bavier <bavier@HIDDEN> To: Attila Lendvai <attila@HIDDEN>, 49607 <at> debbugs.gnu.org Date: Tue, 17 May 2022 20:04:06 +0000 In-Reply-To: <20220428132801.8629-1-attila@HIDDEN> References: <ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@HIDDEN> <20220428132801.8629-1-attila@HIDDEN> Content-Type: multipart/signed; micalg="pgp-sha512"; protocol="application/pgp-signature"; boundary="=-0YjEsnH1V5gNXet5yfx4" MIME-Version: 1.0 X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -3.3 (---) --=-0YjEsnH1V5gNXet5yfx4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, On Thu, 2022-04-28 at 15:28 +0200, Attila Lendvai wrote: > Idris requires a C compiler at runtime to generate executables. >=20 > * gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for > wrap-program). > [phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for- > target). > --- I believe this would prevent someone from effectively setting `IDRIS_CC` to a different compiler from within their environment, correct? I would like to leave that option available to users. Also, can this be a simple compiler reference, or does it need to be a "toolchain compiler"? E.g. I usually set `IDRIS_CC` to gcc from a "gcc-toolchain" package. Could we possibly instead override the default C compiler in the compiler's C backend? Either way we'd be embedding a reference to some compiler/toolchain. `~Eric --=-0YjEsnH1V5gNXet5yfx4 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- iQJGBAABCgAwFiEEo6S0GQB0CHyn3laYvEXKZ+L40AcFAmKD/7YSHGJhdmllckBw b3N0ZW8ubmV0AAoJELxFymfi+NAHWC8P/A10ykzbuVaDBwPy6VTFJXrs9l0zy9y7 k9LuIGeefFwLhWPFoe/kvfzAhAtyqiZv3W0kzNSsb+w9jqe+hS2c+3YX1vpzouTm lKLmZGl7dwBth32cE28weOdBalaZaBHas8Ho+xRDb1+EmVrgHk16QAoF/guV/53I Lf/byxC+4m18XyDomduMPo4VtDuQUE1gvUtghOdJFNOh1iGvHo+XKwi4gMoVK5K3 8dn9YwyQXlwXk4+PEJzKe/7SpWg5Bd9Z/2KTdsFSokRMgevzM4xP89ntITHTFaip efDmsTha2zvwN4e1qdb4ESV948p5MKJRyGkM/LOcNF3VzYA9kSbzk4c8hWoz5Due qqyVVxEm257dVb5LETALeo7hMTZmk0PrMZNKXiVt3LgaPNw3DXL6K3sV4tiH/sL1 rc37b5LRzZ076deCE2noUNOezHHIG6LD2SUR2cIFEQjAnvpjZehHS5ksK0mkqasS 2y1jba7uaCBIJLoiU/h9J7TWwHINhhTLlqxc7EnWNoqBwk48akKZVzJfaOxrPoIH EQL+0owsFtukl15sH4U5iIa91oq4kkfbj6ZCU+F4o+Kj2Mc+tV4v693FaHFOpt4Z zJS/HQWgiXIHODsdOQj+JNiaGxq5NrSLPCw2xI/NdbyU7xYOX6z05MHurpmhVd8P mHLHSGuvioc5 =KPqT -----END PGP SIGNATURE----- --=-0YjEsnH1V5gNXet5yfx4--
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Tobias Geerinckx-Rice <me@HIDDEN>
to control <at> debbugs.gnu.org.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 28 Apr 2022 13:30:41 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 28 09:30:40 2022
Received: from localhost ([127.0.0.1]:45798 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1nk4EC-0004s5-7R
for submit <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:40 -0400
Received: from mail-ej1-f54.google.com ([209.85.218.54]:38458)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1nk4E9-0004rs-ON
for 49607 <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:38 -0400
Received: by mail-ej1-f54.google.com with SMTP id r13so9603447ejd.5
for <49607 <at> debbugs.gnu.org>; Thu, 28 Apr 2022 06:30:37 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=aT4qLJdXyHrZftwvCl4zePNz3uvB7nJJ4yk2MCA7LlQ=;
b=ZCzia3LrcbIFG8DM8AUVFov3SuGxBphA0BFbIluaB7GmmcO6pAIAhpJioeA202zwoE
LxbYgN8j7OuwXyW2GTVdLUAtYq3puaUg08/j7e0Ha6MqMvuHscXQW+qndANSNswyqaAJ
ISPrc31hWCMU+zThxzkgRp1s8f8rn0nrmd2CagN8cqT5xE4IDJus7w0zDuo8NbCcbN1E
0lF9bqA45ZDwLcgPc1vdfwe29NCXpM+rCuAcRezcKZ4TdfMjCv9671OO31YExN8LxfNE
EU0+OieYh+6RcO1GHNEuHSKHs4zq+kxW3v3bN7J0DgPKSlCsicQAw5wW6cSz548WqoMG
J9fw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=aT4qLJdXyHrZftwvCl4zePNz3uvB7nJJ4yk2MCA7LlQ=;
b=1++Y2hTGckGY4AEUXeoPzk3QskjonOKryx9+OG57bq1CgUvyU01WDG9ZbfagUozLs5
sF8vRKtMig6A/dJab5FTlaT0uHZRbIRfVilIVUF3i9vjfUnoRh/1mDw7PKBzUQXCd3d7
7y3qx+h51LXb2vVjEX7yDYdRY1IZL07BFj31NFw5CF22eAN6zxN8OGz3EzNWJEBmSEDV
F/O762V5tjIt3TIP/bov06TGw+w5HxN56k3dhgGEiA4wUsLAB3PORkBGwCdKnmTjDl5q
CoZFnbnLEZS/O1lRrLbzrStmzlIINH5dhuzoHhT+0KTRBojJ8W/NuP/ZAyNnqKY9XEnB
DM5g==
X-Gm-Message-State: AOAM53111pZQU793AInonJB17yea1Ctsu3BhZKdYaWcjgnLEGkTJotZC
M50B0sU72VhS2zdD1gr03GNjGVlzFWw=
X-Google-Smtp-Source: ABdhPJz3DludAPm9TPoRSojfUDGuT40OutijS6LJw+GLAMXcf2NfkFFmpn2hgMGQ6Go/XNqIvaBmgA==
X-Received: by 2002:a17:907:8a23:b0:6f0:14b6:33d9 with SMTP id
sc35-20020a1709078a2300b006f014b633d9mr32295955ejc.559.1651152632010;
Thu, 28 Apr 2022 06:30:32 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
d19-20020a170906c21300b006e7f0730353sm8365993ejz.101.2022.04.28.06.30.31
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 28 Apr 2022 06:30:31 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH v3 3/3] gnu: idris: Add doc output and build the html
documentation.
Date: Thu, 28 Apr 2022 15:28:04 +0200
Message-Id: <20220428132801.8629-3-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
In-Reply-To: <20220428132801.8629-1-attila@HIDDEN>
References: <20220428132801.8629-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
* gnu/packages/idris.scm (make-idris-package): Build the html docs and install
it into the doc output.
---
gnu/packages/idris.scm | 23 ++++++++++++++++++++---
1 file changed, 20 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 1488996b6a..e03ca3bfbf 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -50,7 +50,9 @@ (define-module (gnu packages idris)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
#:use-module (gnu packages racket)
+ #:use-module (gnu packages sphinx)
#:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -249,11 +251,17 @@ (define* (make-idris-package source idris-version
chez-scheme
bootstrap-idris)
coreutils which git
- node ; only for the tests
- racket ; only for the tests
- sed))
+ sed
+ ;; Only for the tests
+ node
+ racket
+ ;; Only for the docs
+ python-minimal
+ python-sphinx
+ python-sphinx-rtd-theme))
(inputs
(list bash-minimal chez-scheme gmp))
+ (outputs '("out" "doc"))
(arguments
(list
#:tests? tests?
@@ -276,6 +284,15 @@ (define* (make-idris-package source idris-version
(delete 'bootstrap)
(delete 'configure)
(delete 'check) ; check must happen after install and wrap-program
+ (add-before 'build 'build-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "make" "--directory" "docs/" "html")))
+ (add-after 'build-doc 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((doc (assoc-ref outputs "doc")))
+ (copy-recursively "docs/build/html"
+ (string-append doc "/share/doc/"
+ ,name "-" ,version)))))
(add-after 'unpack 'patch-paths
(lambda* (#:key inputs #:allow-other-keys)
(let ((files-to-patch (filter file-exists?
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 28 Apr 2022 13:30:22 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 28 09:30:22 2022
Received: from localhost ([127.0.0.1]:45794 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1nk4Ds-0004rU-U8
for submit <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:22 -0400
Received: from mail-ej1-f41.google.com ([209.85.218.41]:37524)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1nk4Dq-0004r1-9a
for 49607 <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:19 -0400
Received: by mail-ej1-f41.google.com with SMTP id kq17so9592120ejb.4
for <49607 <at> debbugs.gnu.org>; Thu, 28 Apr 2022 06:30:18 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=FMgvU55wxnrvfMNaXliq4Og8yAflgxcn2VfpzKaTvgE=;
b=e6CimR7tAMcBqMZiXyrKGFii6wwr7lka58ymEIVQFdncnpDqLLLd9rKA5dglRHUZKa
LY0dScQLl1Qpf8hxLRdu8LmTzNsEi6fUi6HBvJAlAKOQEsqPq0rVPO/AUG22YYgbnzZv
0rmrayJ0mBEhGii8ZKp+Uvmtunr+o224ZWotnamGfNkM63+2n6zFtF1FEBsvRyQeDrDN
qnbANPbUDp9PYHWu+UyFaewXFujdZ3YvZElmLapcZVzHdYNbOXEIQuxuCOmX1L0L/WhP
/41HNLd7EJ/AxqGWjrZqvLl0Dk2cMHx+KFz9wo2l2nKk1sKE3f8rf9kiQpJ7e/5Kfv+W
vXag==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=FMgvU55wxnrvfMNaXliq4Og8yAflgxcn2VfpzKaTvgE=;
b=brnoas016Xas8wbv+2hKhjCCtgsQuvOuy8hgL5Z2Zx4wpNT+jcNxPXqh7Py76v3ArH
mNvpWGPedzlTf4pZkUQXMr5FI2LPGCNKSGwY2UlsMEOnj+Yp1ZTd7C7cjqH+T39yl+sU
LPrzNBYbJY5+JmrraiKTi0L+g3RzBwGRvKpiamb/3H8bb913fbzjoxfB4Vl9vOX6/7P0
DI7UlsO6HYZ8ccGV4GvgMIVIBcwbY55M+XokyK1Cc27my6eQWshh1wNjzwkiCbR8A08B
xAhfL6wPF+HtbQ314M9BQN8ziLFFRXwreqlN1M1c0VviJomT9nq5Ye2m+Y5PrxqJTNQ0
QxYA==
X-Gm-Message-State: AOAM530X250DN++rEwuEmvGbcVP+/r9ni8bnLDADAu8ahg4rPtlCWJWC
6QsnP2XH46di85R3KSHIaTE8MicxzQU=
X-Google-Smtp-Source: ABdhPJz3hOwdypw6VGgqKZQI3GEi/Q1ry7UWgUUmlnqgHN4+v64IVZG0ko6yGI/P4qI0anVIbJ4s7Q==
X-Received: by 2002:a17:907:6d96:b0:6f3:8445:5f13 with SMTP id
sb22-20020a1709076d9600b006f384455f13mr23293299ejc.529.1651152612387;
Thu, 28 Apr 2022 06:30:12 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
d19-20020a170906c21300b006e7f0730353sm8365993ejz.101.2022.04.28.06.30.11
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 28 Apr 2022 06:30:11 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1.
Date: Thu, 28 Apr 2022 15:28:02 +0200
Message-Id: <20220428132801.8629-2-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
In-Reply-To: <20220428132801.8629-1-attila@HIDDEN>
References: <20220428132801.8629-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
The extra generality (e.g. the make-idris-package function) is added so that
it becomes possible to bootstrap Idris HEAD all the way down from GHC. Some
of the past releases require patching, which in turn requires importing them
into separate git branches. This work has not been merged into upstream yet,
therefore some of the historical versions in this commit temprorarily point to
my own fork, as noted in the comments.
The historical versions are marked #:substitutable #false (but they are not
hidden), so that they don't load the substitute servers unnecessarily, but at
the same time are installable.
Idris can bootstrap itself from the checked in Scheme files of the ChezScheme
or Racket backends (it can take a so called 'bootstrap shortcut'), therefore
the historical versions are not needed for compiling the latest version. They
are only needed when one wants to run the bootstrap of Idris all the way down
from Haskell (Idris 1 is written in Haskell).
Create binaries with the version in their name, and add a symlink to them;
e.g. rename the upstream's binary to `bin/idris-1.3.4` and symlink it to
`bin/idris`. This helps when multiple versions are installed.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2, idris2-0.1.1, idris2-0.2.1, idris2-0.2.2, idris2-0.3.0, idris2-0.4.0,
idris2-dev): New variables.
---
gnu/packages/idris.scm | 288 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 285 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 61de4883b1..1488996b6a 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -20,26 +20,56 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO:
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This probably needs patching Idris
+;;; because it uses its FFI infrastrucutre to open libidris_support.so, which
+;;; is based on dlopen.
+;;;
+;;; - The reason some of the historical packages point to
+;;; github.com/attila-lendvai-patches is that these versions need some
+;;; patches to make them buildable today, and these branches haven't been
+;;; incorporated into the official repo yet. Once/if that happens, these
+;;; URL's can be changed to point to the official repo.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
#:use-module (gnu packages libffi)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module (guix utils)
#:use-module ((guix licenses) #:prefix license:)
+ #:use-module (guix gexp)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
-(define-public idris
+;;;
+;;; Idris 1
+;;;
+(define-public idris-1.3
(package
(name "idris")
(version "1.3.4")
@@ -141,7 +171,11 @@ (define-public idris
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target))))))))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name)))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -155,6 +189,254 @@ (define-public idris
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3)
+
+;;;
+;;; Idris 2
+;;;
+(define* (make-idris-package source idris-version
+ #:key bootstrap-idris
+ (idris-version-tag #false)
+ (guix-version (string-append
+ idris-version
+ (if idris-version-tag
+ (string-append
+ "-" idris-version-tag)
+ "")))
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (historical? #false)
+ (hidden? #false) ; or (hidden? historical?)
+ (substitutable? (not historical?))
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.rkt"
+ ))
+ (with-bootstrap-shortcut? (not historical?)))
+ "HISTORICAL? means that it's only interesting for historical reasons, e.g. to be
+used as a bootsrapping stage.
+
+WITH-BOOTSTRAP-SHORTCUT? controls whether to use a previous version of Idris to
+build us (which is potentially recursive), or use the captured compiler output
+(Scheme code)."
+ (package
+ (name "idris2")
+ (version guix-version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((or (? git-checkout?)
+ (? local-file?))
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ (list (if with-bootstrap-shortcut?
+ chez-scheme
+ bootstrap-idris)
+ coreutils which git
+ node ; only for the tests
+ racket ; only for the tests
+ sed))
+ (inputs
+ (list bash-minimal chez-scheme gmp))
+ (arguments
+ (list
+ #:tests? tests?
+ #:substitutable? substitutable?
+ #:make-flags
+ #~(list (string-append "CC=" #$(cc-for-target))
+ #$(string-append "IDRIS_VERSION=" idris-version)
+ #$(string-append "IDRIS_VERSION_TAG=" (or idris-version-tag ""))
+ #$(if with-bootstrap-shortcut?
+ #~(string-append "SCHEME="
+ #$(this-package-input "chez-scheme")
+ "/bin/scheme")
+ #~(string-append "BOOTSTRAP_IDRIS="
+ #$bootstrap-idris
+ "/bin/" #$(package-name bootstrap-idris)))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ `(modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (let ((files-to-patch (filter file-exists?
+ ',files-to-patch-for-shell)))
+ (substitute* files-to-patch
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env"))))))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let* ((out (assoc-ref outputs "out"))
+ (image-base (string-append
+ out "/bin/idris2_app/idris2"))
+ (image (if (file-exists? image-base)
+ image-base
+ ;; For v0.5.1 and older.
+ (string-append image-base ".so"))))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file image (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib"))))))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,idris-version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append
+ out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name))))))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (let ((invoke-make
+ (lambda (target)
+ (apply invoke "make"
+ "INTERACTIVE="
+ ;; "THREADS=1" ; for reproducible test output
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ target make-flags))))
+ ;; TODO This is something like how it should be handled, but
+ ;; the Makefile unconditionally invokes the `testenv` target,
+ ;; and thus overwrites the `runtest` script when `make test` is
+ ;; invoked. For now this situation is resolved in the Idris
+ ;; Makefile, by explicitly invoking the Idris `runtest` wrapper
+ ;; script with an sh prefix.
+ ;;
+ ;;(invoke-make "testenv")
+ ;;(patch-shebang "build/stage2/runtests")
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (invoke-make "test"))))))))
+ (properties `((hidden? . ,hidden?)))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+types. It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.1.1
+ ;; branch idris.2
+ ;; This is the first (untagged) Idris2 version that bootstraps off of the
+ ;; Idris1 line. Originally it was in the repo called Idris2-boot.
+ (make-idris-package '("3c2335ee6bc00b7f417ac672a4ab7b73599abeb3"
+ "10w10ggyvlw7m1pazbfxr4sj3wpb6z1ap6rg3lxc0z6f2s3x53cb")
+ "0.1.1"
+ #:bootstrap-idris idris-1.3
+ #:historical? #true
+ #:unwrap? #false
+ ;; TODO `make bootstrap` needs to be backported into the
+ ;; Makefile in this branch. Force the bootstrap
+ ;; shortcut to be turned off.
+ #:with-bootstrap-shortcut? #false))
+
+(define-public idris2-0.2.1
+ ;; branch idris.3
+ (make-idris-package '("257bbc27498808e8cd4155cc06ea3f6a07541537"
+ "0idxplcmd6p13i2n0g49bc2snddny4kdr4wvd8854snzsiwqn7p1"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.1"
+ #:bootstrap-idris idris2-0.1.1
+ #:historical? #true))
+
+(define-public idris2-0.2.2
+ ;; branch idris.4
+ (make-idris-package '("9bc8e6e9834cbc7b52dc6ca2d80d7e96afeb47d1"
+ "0xzl1mb5yxgp6v36rngy00i59cfy67niyiblcpaksllrgmg639p4"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.2"
+ #:bootstrap-idris idris2-0.2.1
+ #:historical? #true))
+
+(define-public idris2-0.3.0
+ ;; branch idris.5
+ (make-idris-package '("025b5cd25b76eae28283a10bd155c384e46fbd82"
+ "00a83paib571ahknipmgw7g9pbym105isk3bz0c1ng41s4kjpsxh"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.3.0"
+ #:bootstrap-idris idris2-0.2.2
+ #:historical? #true))
+
+(define-public idris2-0.4.0
+ ;; branch idris.6
+ (make-idris-package '("v0.4.0"
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g")
+ "0.4.0"
+ #:bootstrap-idris idris2-0.3.0
+ #:ignore-test-failures? #true ; TODO investigate
+ #:historical? #true))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
+;; TODO re build failure: in the build sandbox some parts of the test output
+;; is missing. I cannot reproduce it in a guix shell. My assumption is that
+;; it's an Idris bug that only manifests in certain circumstances. There are
+;; some other issues left with the use of #!/bin/sh, too.
+(define-public idris2-dev
+ (make-idris-package '("4bb12225424d76c7874b176e2bfb8b5550c112eb"
+ "0kb800cgfm0afa83pbyi3x9bpswcl8jz4pr68zy092fs50km3bj7"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.5.1"
+ #:ignore-test-failures? #true
+ #:idris-version-tag "dev"))
+
+(define-public idris2 idris2-0.5.1)
+
+;;;
+;;; Idris apps
+;;;
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 28 Apr 2022 13:30:06 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 28 09:30:05 2022
Received: from localhost ([127.0.0.1]:45791 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1nk4Dd-0004pt-I9
for submit <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:05 -0400
Received: from mail-ed1-f43.google.com ([209.85.208.43]:40931)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1nk4Da-0004p4-UL
for 49607 <at> debbugs.gnu.org; Thu, 28 Apr 2022 09:30:03 -0400
Received: by mail-ed1-f43.google.com with SMTP id p18so5533121edr.7
for <49607 <at> debbugs.gnu.org>; Thu, 28 Apr 2022 06:30:02 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:mime-version
:content-transfer-encoding;
bh=sHv4ZxAZOYzVJZucaEJkhZDG3DhDrFjXJgV7svKxmDA=;
b=k7ERS1IkKoU8Uyj12fFWAWqPwYK7CSdpmqL44uQ7zt6E9CLmDDLhbnBeuZjeAl2QsB
iarXVyUdmzX20cQt8zx+nO3u0/GB6Vabt2bi8pUeU5vjst8IW0OR2Bf7EVkutei3hSmV
OXeclsM5w0BTnKNLnw3pSZAk8UbOfMZjUF8lThJrL8fvlEhUkxgVIaFRM0Y7OfoF8zD5
lK4wbvDAypAS/ZqbBA0qvjyv0l1HlGOmcXJ5WqeVB2A+he17bHjo1AjkRZGnq9dpA0Ii
1v2kyCeGj1Uz03H7Z0I1Ddo/1xOKXsxRjV5J1XQgzkHG3gyNgtWBc/6yC7usCnSzkGGY
rqIQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:mime-version:content-transfer-encoding;
bh=sHv4ZxAZOYzVJZucaEJkhZDG3DhDrFjXJgV7svKxmDA=;
b=B0DLgk91wOmEnp27YGaRrYbEDIk5BhzSP9jlI1DuyvRH+Ru4r2VcPKCIsnh3mouyqP
fhFdxqHMV0x/c0QSn5y5xqZuIafW0bT60E2BF2h36S7MV8scImUrYbobviasOUxAyM3q
bW08pEY8zjGcLxV4HXAQAMXfeMQPnrsBJp0furUTLoPBRZzPFjV2opamIqH1mYqVZUpr
q7lSo+N2rqQs6JNXL+q2ZlKXhdTxwH6CbDbvs2xv/kABJiw4A1HhT5yoRw8xG3YM2TvE
FeeLEZiYRQEABqTHctK0on2TGZgcYkmtACpBWRtyM4QPISIs6fUjAwNr4I26BgDAa//4
06vQ==
X-Gm-Message-State: AOAM531cE/IivdMS9QR+U2g2ih2GUNyAaDC1fOpmqdtP8mpNTypn50uh
q1h2ThfsNN2zQq+dYTL5vz+7ZS1MTcA=
X-Google-Smtp-Source: ABdhPJzkYuWoHXyWCY3vh7rkb5ExsQwDhzYDyVnWKfRYTBu3zN77yuStXMWK5sx4C6TgKwsfoc7kSA==
X-Received: by 2002:a05:6402:4404:b0:426:16f:c0f9 with SMTP id
y4-20020a056402440400b00426016fc0f9mr11740426eda.31.1651152597016;
Thu, 28 Apr 2022 06:29:57 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
d19-20020a170906c21300b006e7f0730353sm8365993ejz.101.2022.04.28.06.29.55
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 28 Apr 2022 06:29:56 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
Date: Thu, 28 Apr 2022 15:28:00 +0200
Message-Id: <20220428132801.8629-1-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for wrap-program).
[phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for-target).
---
v3: i have rebased them to master, i.e. on top of the idris-1.3.4 update.
it also cleans it up a bit more (e.g. got rid of the clang-toolchain dependency).
gnu/packages/idris.scm | 15 ++++++++++++---
1 file changed, 12 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 8f08ed3a3e..61de4883b1 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -22,6 +22,7 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -35,7 +36,8 @@ (define-module (gnu packages idris)
#:use-module (guix git-download)
#:use-module (guix utils)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (guix utils))
(define-public idris
(package
@@ -56,7 +58,8 @@ (define-public idris
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
ghc-tasty-rerun))
(inputs
- (list gmp
+ (list bash-minimal
+ gmp
ncurses
ghc-aeson
ghc-annotated-wl-pprint
@@ -132,7 +135,13 @@ (define-public idris
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))))))))
+ (string-append out filename)))))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target))))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 20 Apr 2022 13:50:31 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Wed Apr 20 09:50:30 2022 Received: from localhost ([127.0.0.1]:45365 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1nhAim-0003qD-Ff for submit <at> debbugs.gnu.org; Wed, 20 Apr 2022 09:50:30 -0400 Received: from mout01.posteo.de ([185.67.36.65]:35117) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <bavier@HIDDEN>) id 1nhAik-0003pi-9j for 49607 <at> debbugs.gnu.org; Wed, 20 Apr 2022 09:50:15 -0400 Received: from submission (posteo.de [185.67.36.169]) by mout01.posteo.de (Postfix) with ESMTPS id A4F96240026 for <49607 <at> debbugs.gnu.org>; Wed, 20 Apr 2022 15:50:08 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1650462608; bh=lrdnHj69tT70FBiPsCbxqgTciBCkNBLnmX9xRCbjekM=; h=Date:From:To:Subject:From; b=sCWgYgbKp2SpMviubrGIVcrGZ6+qAl59hV+K4wBT0+XcVtEu33tmYiSWF/hqjW8lw iyhKwbpXr3XD23kLR4C2ffCT8taHwEU3VWRkQ6I/yMyl981nayk72eP4bWir+TP2HU oAaOIyBH3aWF2ZN5FYsPr1v7Vzdlo6zvU32g6Bbtw0gcrIld6FdrnRmCu/zoG1OJOv hScwikdFOG55a20fpb+jXWRYJ4z9grsZQoCAbY8/SPwIul10vKWWZOLUnUol1+cpEz r2erwcPIWkYHiYVcWWW1fC7NTFQ9PPis2y0gHe81qM8O7/v1bfeIm1Lce68UHvueJG 2Nv6V9LEq/Cmg== Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4Kk29X2Smfz9rxF for <49607 <at> debbugs.gnu.org>; Wed, 20 Apr 2022 15:50:08 +0200 (CEST) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: quoted-printable Date: Wed, 20 Apr 2022 13:50:07 +0000 From: Eric Bavier <bavier@HIDDEN> To: 49607 <at> debbugs.gnu.org Subject: Re: [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4. In-Reply-To: <20220414121612.9815-2-attila@HIDDEN> References: <20220414121612.9815-1-attila@HIDDEN> <20220414121612.9815-2-attila@HIDDEN> Message-ID: <ab9cbd9c49be77db8a5f2f46281662e0@HIDDEN> X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.0 (-) Hi! On Thu, 2022-04-14 at 14:16 +0200, Attila Lendvai wrote: > * gnu/packages/idris.scm (idris-1.3.4): New variable, the latest from > the v1.x > line of Idris at the time of writing. > (make-idris-package): New function to instantiate a package of > Idris2. > (idris2-0.5.1): New variable. > * gnu/packages/patches/idris-build-with-haskeline-0.8.patch: Deleted. > * gnu/packages/patches/idris-build-with-megaparsec-9.patch: Deleted. > * gnu/packages/patches/idris-disable-test.patch: Deleted. > --- > =C2=A0gnu/local.mk=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 |=C2= =A0=C2=A0 3 - > =C2=A0gnu/packages/idris.scm=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 | 307 > +++++++++++++++++- > =C2=A0.../idris-build-with-haskeline-0.8.patch=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 |=C2=A0 85 ----- > =C2=A0.../idris-build-with-megaparsec-9.patch=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0 |=C2=A0 27 -- > =C2=A0gnu/packages/patches/idris-disable-test.patch |=C2=A0 19 -- > =C2=A05 files changed, 293 insertions(+), 148 deletions(-) > =C2=A0delete mode 100644 gnu/packages/patches/idris-build-with-haskeline- > 0.8.patch > =C2=A0delete mode 100644 gnu/packages/patches/idris-build-with-megaparsec= - > 9.patch > =C2=A0delete mode 100644 gnu/packages/patches/idris-disable-test.patch I've pushed the 1.3.4 update portion of this patch in commit 0cf1178a65. I am still reviewing the rest. `~Eric
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.Received: (at 49607) by debbugs.gnu.org; 14 Apr 2022 15:54:16 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 14 11:54:15 2022 Received: from localhost ([127.0.0.1]:57008 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1nf1nT-0003El-M8 for submit <at> debbugs.gnu.org; Thu, 14 Apr 2022 11:54:15 -0400 Received: from mail-4317.proton.ch ([185.70.43.17]:50978) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <attila@HIDDEN>) id 1nf1nR-0003EW-4m for 49607 <at> debbugs.gnu.org; Thu, 14 Apr 2022 11:54:15 -0400 Date: Thu, 14 Apr 2022 15:53:57 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=lendvai.name; s=protonmail3; t=1649951646; bh=23ufbj4bQbREVgkn5fKof11O6+3bZezs7JAwPuntuUM=; h=Date:To:From:Reply-To:Subject:Message-ID:From:To:Cc:Date:Subject: Reply-To:Feedback-ID:Message-ID; b=No/eT/mNl+KUNdEGcSInykz6xcD7ixfBhvOvBa++JZk66iW6z9e/PXMeMxvRvbihs WlD2oCYOEPrOdkpxWSnUb3Ip8Cs+5Wl2X3bzUxG5prYeVjt1wP8kwwCbhQvkqzfXOu /gdy+9f29RMGlKx3Bcw+ZzgqyPeBOLazhYDC1iPbQWUZAz7CbDxD3hzBoUXw0hXPq9 amHkedJhX3Ig7hWHkGoBc0M+OeSrRVp5w/u39pzcHEUEAwqZ3x0Hob0K3Ue5+n4QbM VmSCumcGWzACxcGQlEDGp3xs6zL8y/8QZD5NiDAATfgBc1mGtOdjf8+P2Y60A4JeWa k9dCzGL4QHgtQ== To: "49607 <at> debbugs.gnu.org" <49607 <at> debbugs.gnu.org> From: Attila Lendvai <attila@HIDDEN> Subject: a note Message-ID: <cTInHha1IkYxVmCTrt1bBqpFssrw9suBeTOSpxwkV_ro3QmtCYfYngOLu5q0pten21J1QWJW6B9Bg5QEmhX9JVIUMhEuwa4kQMRsGxEOVkk=@lendvai.name> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 49607 X-BeenThere: debbugs-submit <at> debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: <debbugs-submit.debbugs.gnu.org> List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe> List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/> List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org> List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help> List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe> Reply-To: Attila Lendvai <attila@HIDDEN> Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org> X-Spam-Score: -1.0 (-) note that some of these packages are pointing to my own fork of the Idris2 = repo. if that is an issue, then feel free to comment out those packages for the t= ime being. i'm working on incorporating these branches back into the official Idris2 r= epo. (the current milestone of that process is to get my build system refactor m= erged https://github.com/idris-lang/Idris2/pull/1990) -- =E2=80=A2 attila lendvai =E2=80=A2 PGP: 963F 5D5F 45C7 DFCD 0A39 -- =E2=80=9CJournalism is printing what someone else does not want printed: ev= erything else is public relations.=E2=80=9D =09=E2=80=94 George Orwell (1903=E2=80=931950)
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 14 Apr 2022 12:21:27 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 14 08:21:27 2022
Received: from localhost ([127.0.0.1]:55530 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1neyTX-0001LF-D2
for submit <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:27 -0400
Received: from mail-ej1-f43.google.com ([209.85.218.43]:34782)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1neyTP-0001Ko-B7
for 49607 <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:19 -0400
Received: by mail-ej1-f43.google.com with SMTP id ks6so9725281ejb.1
for <49607 <at> debbugs.gnu.org>; Thu, 14 Apr 2022 05:21:19 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=GwHoW2ZE3/RtBK744gIM7HPJxkEg6js/OAnh1xrZkEc=;
b=IaNjzmsBYT0k/m/GVCvUbJgcSPdrYROja0Zoh7fLN9fBOAEaH3McklYD8VYTbwPIzd
/JfyehcNGYhmv3dmQF0CtQF6vvFNmIGSUefI0yEymiNZ0kRjRGuRQzAdB98rCYDj93HZ
ibEIPiXfz41qX7a0h3N242/AxxLcq7KPcj3gXeqXf67/LrduI2xVMDX2jOI5ptFJKnUr
JPk6LM61o+D8GI9L7RF7Mi3OVER6vK+gUndjCUcE1VdRu8FBXF817VOvN+LMPtOUXNI8
qyby4D8gFpEJF3Pown/kGvzR0PqcRYA4721+FOFYcj7RLtykRoYlK7P6fa88bq7CRzkE
Odew==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=GwHoW2ZE3/RtBK744gIM7HPJxkEg6js/OAnh1xrZkEc=;
b=VxFK6rwuAUlyqD0EMK1/DGC3qdUC94unoNTPUmtZT9tG34BELQ4k5k9WcOUEsWIVCQ
QxtzSSzf1yLftpg8FXSFarPO8Tg4MDiQGjJmJjaWOwOKz0bRJg1/nbhGeUslWWIVK45/
hXRF8OwvRGbm74Af/PwHi3x6Rs6KfVvNo0JZotR23E3SA7AbZZhmv9nW2I/8CCwSG0YJ
PdxhCPOCF4mQyoXRMq/uzRPNxhv1isZV0BT7A2a6ftDe8/wW8ppIPKhWSB6XlRkIljlR
PABMnMdoDPNU/kV6cYzy9YIgFyUkQLgGBlySe/+oLhkNqq0C9CE/bHss3NmhZAem7HDy
Q5ww==
X-Gm-Message-State: AOAM5311e44gCWzupEYlv/qBpsooE7L7+XnOZ1oUIksEsbgiP95DSRXv
HeBtfMp0ND21G8r5gMRkVWqFx6xQw34=
X-Google-Smtp-Source: ABdhPJzETq+NE+3KEp3pXkFLmOQDJqQqn9RK6X/vJv9qTDpl+Wep2gIGmRl4RunL3gLhUmHxrlXWtg==
X-Received: by 2002:a17:906:9b85:b0:6db:ab80:7924 with SMTP id
dd5-20020a1709069b8500b006dbab807924mr2135954ejc.160.1649938873798;
Thu, 14 Apr 2022 05:21:13 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
u3-20020a17090657c300b006d01de78926sm582042ejr.22.2022.04.14.05.21.13
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 14 Apr 2022 05:21:13 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH 3/3] gnu: idris: Add doc output and build the html
documentation.
Date: Thu, 14 Apr 2022 14:16:13 +0200
Message-Id: <20220414121612.9815-3-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
In-Reply-To: <20220414121612.9815-1-attila@HIDDEN>
References: <20220414121612.9815-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
* gnu/packages/idris.scm (make-idris-package): Build the html docs and install
it into the doc output.
---
gnu/packages/idris.scm | 23 ++++++++++++++++++++---
1 file changed, 20 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 28e918a486..b9b309d6d5 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -50,7 +50,9 @@ (define-module (gnu packages idris)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
#:use-module (gnu packages racket)
+ #:use-module (gnu packages sphinx)
#:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -248,11 +250,17 @@ (define* (make-idris-package source idris-version
bootstrap-idris)
clang-toolchain-12 ; older clang-toolchain versions don't have a bin/cc
coreutils which git
- node ; only for the tests
- racket ; only for the tests
- sed))
+ sed
+ ;; Only for the tests
+ node
+ racket
+ ;; Only for the docs
+ python-minimal
+ python-sphinx
+ python-sphinx-rtd-theme))
(inputs
(list bash-minimal chez-scheme gmp))
+ (outputs '("out" "doc"))
(arguments
(list
#:tests? tests?
@@ -275,6 +283,15 @@ (define* (make-idris-package source idris-version
(delete 'bootstrap)
(delete 'configure)
(delete 'check) ; check must happen after install and wrap-program
+ (add-before 'build 'build-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "make" "--directory" "docs/" "html")))
+ (add-after 'build-doc 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((doc (assoc-ref outputs "doc")))
+ (copy-recursively "docs/build/html"
+ (string-append doc "/share/doc/"
+ ,name "-" ,version)))))
(add-after 'unpack 'patch-paths
(lambda* (#:key inputs #:allow-other-keys)
(let ((files-to-patch (filter file-exists?
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 14 Apr 2022 12:21:27 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 14 08:21:27 2022
Received: from localhost ([127.0.0.1]:55527 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1neyTP-0001L0-4k
for submit <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:27 -0400
Received: from mail-ej1-f48.google.com ([209.85.218.48]:42888)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1neyTM-0001Kd-1K
for 49607 <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:17 -0400
Received: by mail-ej1-f48.google.com with SMTP id i27so9663713ejd.9
for <49607 <at> debbugs.gnu.org>; Thu, 14 Apr 2022 05:21:15 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=vr260DYMCgp4CvkcF7hr2uksDPF/5yw4fHHuMiQ0ge8=;
b=Gf8IvSuo2CEc90HnH2FF1SCOY6FMKZ5uX6T3tIyM9dG/bViCqrgbfuHTgGgun+kBdF
CMm5itkcveJb3MRd/Vh5OeiNIyvdibN7TCPr90lJgs1MsB2wEK3sW7Aov7uinYi1KdhV
M2Zp5LPce46J0A2Q4xLZbBhqK9TCYVcAUZBnBAynSij6Y+fqP8XpvC/9zwOK2NAnRK6Q
b7ggzZ+b2mKxFC39uTsub0Yeg68PheGHpQk/tfMVlaNA9IPx2QqX6hhah1Jiw0o0yAea
3DyTPcxg05u4ehrQeXt/T53D6F5S5HMDhrMNNzjy+2StAx2RizMBe78pwk/X+97RGeDy
GUEw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=vr260DYMCgp4CvkcF7hr2uksDPF/5yw4fHHuMiQ0ge8=;
b=pwhzkkshal10kmoRNbMRXvQpgfL3LxB1Va6wGQ3X62e2EWHKx6LbHTKJhW6lyvFbMc
XgWh9VSMYpKUDp77VCJKOiymPd6NEGJIEk66dgCcmTFA5ZCWeS33zGSpGJHa/ciJ+8Gw
Ep/vqKOPpigm0urPmAqCpQodisPCWq6sLi8vkj6hQc4+9tNYJAametiw4BIlZyUp1zjM
wGeCgZdD0mWeYZKGsU6h8oXamsnPhMTuCueFh3l/KnrD27L8kd1Kpa6osyjuMgOBrnBb
yQKUnk2cj9wsi3kHuaPOi3BSM1l1uEbhRcJi6kSz1ViDZWCr5HsaQfBHvsZse5vhe6gz
7SLQ==
X-Gm-Message-State: AOAM531sg1t/zDPEJm/JVhBGndWcfm5RkKxv9jHzSOuMjzRDD1EwUew5
ZKrRV9T3hPfJS0sZWHSkQ++5Z3Q/t0c=
X-Google-Smtp-Source: ABdhPJwyy3TsA+5aAafAOBWX5UvfD9iQm8TXw5KirzREiBIdPuimyz7saD13yXfNQ9kYHhnzV+2geQ==
X-Received: by 2002:a17:907:3e16:b0:6df:b4f0:5cc2 with SMTP id
hp22-20020a1709073e1600b006dfb4f05cc2mr2089218ejc.285.1649938870061;
Thu, 14 Apr 2022 05:21:10 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
u3-20020a17090657c300b006d01de78926sm582042ejr.22.2022.04.14.05.21.09
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 14 Apr 2022 05:21:09 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4.
Date: Thu, 14 Apr 2022 14:16:12 +0200
Message-Id: <20220414121612.9815-2-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
In-Reply-To: <20220414121612.9815-1-attila@HIDDEN>
References: <20220414121612.9815-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
The extra generality is added so that it is possible to bootstrap Idris HEAD
all the way down from GHC. It requires patching past releases, which requires
importing them into separate git branches. This work has not been merged into
upstream yet, therefore the historical versions in this commit temprorarily
point to my own fork, as noted in the comments.
The historical versions are marked #:substitutable #false (but they are not
hidden), so that they don't load the substitute servers. Idris can bootstrap
itself from the checked in Scheme files of the ChezScheme or Racket
backends (it can take a so called 'bootstrap shortcut'), therefore the
historical versions are not necessary for compiling the latest version.
They are only needed when one wants to run the bootstrap of Idris all the
way down from Haskell (Idris 1 is written in Haskell).
Add a symlink to a versioned binary; e.g. rename the upstream's binary to
`bin/idris-1.3.4` and symlink it to `bin/idris`. This helps when multiple
versions are installed.
* gnu/packages/idris.scm (idris-1.3.4): New variable, the latest from the v1.x
line of Idris at the time of writing.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2-0.5.1): New variable.
* gnu/packages/patches/idris-build-with-haskeline-0.8.patch: Deleted.
* gnu/packages/patches/idris-build-with-megaparsec-9.patch: Deleted.
* gnu/packages/patches/idris-disable-test.patch: Deleted.
---
gnu/local.mk | 3 -
gnu/packages/idris.scm | 307 +++++++++++++++++-
.../idris-build-with-haskeline-0.8.patch | 85 -----
.../idris-build-with-megaparsec-9.patch | 27 --
gnu/packages/patches/idris-disable-test.patch | 19 --
5 files changed, 293 insertions(+), 148 deletions(-)
delete mode 100644 gnu/packages/patches/idris-build-with-haskeline-0.8.patch
delete mode 100644 gnu/packages/patches/idris-build-with-megaparsec-9.patch
delete mode 100644 gnu/packages/patches/idris-disable-test.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 70133e6502..4e46b47ad9 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1283,9 +1283,6 @@ dist_patch_DATA = \
%D%/packages/patches/icedtea-7-hotspot-aarch64-use-c++98.patch\
%D%/packages/patches/id3lib-CVE-2007-4460.patch \
%D%/packages/patches/id3lib-UTF16-writing-bug.patch \
- %D%/packages/patches/idris-disable-test.patch \
- %D%/packages/patches/idris-build-with-haskeline-0.8.patch \
- %D%/packages/patches/idris-build-with-megaparsec-9.patch \
%D%/packages/patches/idris-test-ffi008.patch \
%D%/packages/patches/ilmbase-fix-tests.patch \
%D%/packages/patches/imagemagick-CVE-2020-27829.patch \
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index f84431cab9..28e918a486 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -19,9 +19,28 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO:
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This probably needs patching Idris
+;;; because it uses its FFI infrastrucutre to open libidris_support.so, which
+;;; is based on dlopen.
+;;;
+;;; - The reason some of the historical packages point to
+;;; github.com/attila-lendvai-patches is that these versions need some
+;;; patches to make them buildable today, and these branches haven't been
+;;; incorporated into the official repo yet. Once/if that happens, these
+;;; URL's can be changed to point to the official repo.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -29,31 +48,40 @@ (define-module (gnu packages idris)
#:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
+ #:use-module (guix gexp)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
-(define-public idris-1.3.3
+;;;
+;;; Idris 1
+;;;
+(define-public idris-1.3.4
(package
(name "idris")
- (version "1.3.3")
+ (version "1.3.4")
(source (origin
- (method url-fetch)
- (uri (string-append
- "https://hackage.haskell.org/package/"
- "idris-" version "/idris-" version ".tar.gz"))
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris-dev.git")
+ (commit (string-append "v" version))))
(sha256
(base32
- "1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4"))
- (patches (search-patches "idris-disable-test.patch"
- "idris-build-with-haskeline-0.8.patch"
- "idris-build-with-megaparsec-9.patch"
- "idris-test-ffi008.patch"))))
+ "0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
+ (patches (search-patches "idris-test-ffi008.patch"))
+ (file-name (git-file-name "idris" version))))
(build-system haskell-build-system)
(native-inputs ;For tests
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
@@ -141,7 +169,11 @@ (define-public idris-1.3.3
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target))))))))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name)))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -155,7 +187,254 @@ (define-public idris-1.3.3
Epigram and Agda.")
(license license:bsd-3)))
-(define-public idris idris-1.3.3)
+(define-public idris idris-1.3.4)
+
+;;;
+;;; Idris 2
+;;;
+(define* (make-idris-package source idris-version
+ #:key bootstrap-idris
+ (idris-version-tag #false)
+ (guix-version (string-append
+ idris-version
+ (if idris-version-tag
+ (string-append
+ "-" idris-version-tag)
+ "")))
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (historical? #false)
+ (hidden? #false) ; or (hidden? historical?)
+ (substitutable? (not historical?))
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.rkt"
+ ))
+ (with-bootstrap-shortcut? (not historical?)))
+ "HISTORICAL? means that it's only interesting for historical reasons, e.g. to be
+used as a bootsrapping stage.
+
+WITH-BOOTSTRAP-SHORTCUT? controls whether to use a previous version of Idris to
+build us (which is potentially recursive), or use the captured compiler output
+(Scheme code)."
+ (package
+ (name "idris2")
+ (version guix-version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((or (? git-checkout?)
+ (? local-file?))
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ (list (if with-bootstrap-shortcut?
+ chez-scheme
+ bootstrap-idris)
+ clang-toolchain-12 ; older clang-toolchain versions don't have a bin/cc
+ coreutils which git
+ node ; only for the tests
+ racket ; only for the tests
+ sed))
+ (inputs
+ (list bash-minimal chez-scheme gmp))
+ (arguments
+ (list
+ #:tests? tests?
+ #:substitutable? substitutable?
+ #:make-flags
+ #~(list (string-append "CC=" #$(cc-for-target))
+ #$(string-append "IDRIS_VERSION=" idris-version)
+ #$(string-append "IDRIS_VERSION_TAG=" (or idris-version-tag ""))
+ #$(if with-bootstrap-shortcut?
+ #~(string-append "SCHEME="
+ #$(this-package-input "chez-scheme")
+ "/bin/scheme")
+ #~(string-append "BOOTSTRAP_IDRIS="
+ #$bootstrap-idris
+ "/bin/" #$(package-name bootstrap-idris)))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ `(modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (let ((files-to-patch (filter file-exists?
+ ',files-to-patch-for-shell)))
+ (substitute* files-to-patch
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env"))))))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let* ((out (assoc-ref outputs "out"))
+ (image-base (string-append
+ out "/bin/idris2_app/idris2"))
+ (image (if (file-exists? image-base)
+ image-base
+ ;; For v0.5.1 and older.
+ (string-append image-base ".so"))))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file image (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib"))))))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,idris-version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append
+ out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name))))))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (let ((invoke-make
+ (lambda (target)
+ (apply invoke "make"
+ "INTERACTIVE="
+ ;; "THREADS=1" ; for reproducible test output
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ target make-flags))))
+ ;; TODO This is something like how it should be handled, but
+ ;; the Makefile unconditionally invokes the `testenv` target,
+ ;; and thus overwrites the `runtest` script when `make test` is
+ ;; invoked. For now this situation is resolved in the Idris
+ ;; Makefile, by explicitly invoking the Idris `runtest` wrapper
+ ;; script with an sh prefix.
+ ;;
+ ;;(invoke-make "testenv")
+ ;;(patch-shebang "build/stage2/runtests")
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (invoke-make "test"))))))))
+ (properties `((hidden? . ,hidden?)))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+types. It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.1.1
+ ;; branch idris.2
+ ;; This is the first (untagged) Idris2 version that bootstraps off of the
+ ;; Idris1 line. Originally it was in the repo called Idris2-boot.
+ (make-idris-package '("3c2335ee6bc00b7f417ac672a4ab7b73599abeb3"
+ "10w10ggyvlw7m1pazbfxr4sj3wpb6z1ap6rg3lxc0z6f2s3x53cb")
+ "0.1.1"
+ #:bootstrap-idris idris-1.3.4
+ #:historical? #true
+ #:unwrap? #false
+ ;; TODO `make bootstrap` needs to be backported into the
+ ;; Makefile in this branch. Force the bootstrap
+ ;; shortcut to be turned off.
+ #:with-bootstrap-shortcut? #false))
+
+(define-public idris2-0.2.1
+ ;; branch idris.3
+ (make-idris-package '("257bbc27498808e8cd4155cc06ea3f6a07541537"
+ "0idxplcmd6p13i2n0g49bc2snddny4kdr4wvd8854snzsiwqn7p1"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.1"
+ #:bootstrap-idris idris2-0.1.1
+ #:historical? #true))
+
+(define-public idris2-0.2.2
+ ;; branch idris.4
+ (make-idris-package '("9bc8e6e9834cbc7b52dc6ca2d80d7e96afeb47d1"
+ "0xzl1mb5yxgp6v36rngy00i59cfy67niyiblcpaksllrgmg639p4"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.2"
+ #:bootstrap-idris idris2-0.2.1
+ #:historical? #true))
+
+(define-public idris2-0.3.0
+ ;; branch idris.5
+ (make-idris-package '("025b5cd25b76eae28283a10bd155c384e46fbd82"
+ "00a83paib571ahknipmgw7g9pbym105isk3bz0c1ng41s4kjpsxh"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.3.0"
+ #:bootstrap-idris idris2-0.2.2
+ #:historical? #true))
+
+(define-public idris2-0.4.0
+ ;; branch idris.6
+ (make-idris-package '("v0.4.0"
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g")
+ "0.4.0"
+ #:bootstrap-idris idris2-0.3.0
+ #:ignore-test-failures? #true ; TODO investigate
+ #:historical? #true))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
+;; TODO re build failure: in the build sandbox some parts of the test output
+;; is missing. I cannot reproduce it in a guix shell. My assumption is that
+;; it's an Idris bug that only manifests in certain circumstances. There are
+;; some other issues left with the use of #!/bin/sh, too.
+(define-public idris2-dev
+ (make-idris-package '("4bb12225424d76c7874b176e2bfb8b5550c112eb"
+ "0kb800cgfm0afa83pbyi3x9bpswcl8jz4pr68zy092fs50km3bj7"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.5.1"
+ #:ignore-test-failures? #true
+ #:idris-version-tag "dev"))
+
+(define-public idris2 idris2-0.5.1)
+
+;;;
+;;; Idris apps
+;;;
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
diff --git a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch b/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
deleted file mode 100644
index 5d1fec2409..0000000000
--- a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
+++ /dev/null
@@ -1,85 +0,0 @@
-From 89a87cf666eb8b27190c779e72d0d76eadc1bc14 Mon Sep 17 00:00:00 2001
-From: Niklas Larsson <niklas@HIDDEN>
-Date: Sat, 6 Jun 2020 15:29:45 +0200
-Subject: [PATCH] Fix to unblock haskeline-0.8
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4871>
-
- idris.cabal | 2 +-
- src/Idris/Output.hs | 8 --------
- src/Idris/REPL.hs | 12 +++++-------
- 3 files changed, 6 insertions(+), 16 deletions(-)
-
-diff --git a/idris.cabal b/idris.cabal
-index 38359019a9..bc9e265023 100644
---- a/idris.cabal
-+++ b/idris.cabal
-@@ -336,7 +336,7 @@ Library
- , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0
- , filepath < 1.5
- , fingertree >= 0.1.4.1 && < 0.2
-- , haskeline >= 0.7 && < 0.8
-+ , haskeline >= 0.8 && < 0.9
- , ieee754 >= 0.7 && < 0.9
- , megaparsec >= 7.0.4 && < 9
- , mtl >= 2.1 && < 2.3
-diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs
-index 70b4d48a30..6b5d59948c 100644
---- a/src/Idris/Output.hs
-+++ b/src/Idris/Output.hs
-@@ -37,21 +37,13 @@ import Prelude hiding ((<$>))
- #endif
-
- import Control.Arrow (first)
--import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
- import Data.List (intersperse, nub)
- import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
- import qualified Data.Set as S
--import System.Console.Haskeline.MonadException (MonadException(controlIO),
-- RunIO(RunIO))
- import System.FilePath (replaceExtension)
- import System.IO (Handle, hPutStr, hPutStrLn)
- import System.IO.Error (tryIOError)
-
--instance MonadException m => MonadException (ExceptT Err m) where
-- controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
-- run' = RunIO (fmap ExceptT . run . runExceptT)
-- in fmap runExceptT $ f run'
--
- pshow :: IState -> Err -> String
- pshow ist err = displayDecorated (consoleDecorate ist) .
- renderPretty 1.0 80 .
-diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
-index 05587d9672..5e0dc21089 100644
---- a/src/Idris/REPL.hs
-+++ b/src/Idris/REPL.hs
-@@ -122,23 +122,21 @@ repl orig mods efile
- (if colour && not isWindows
- then colourisePrompt theme str
- else str) ++ " "
-- x <- H.catch (H.withInterrupt $ getInputLine prompt)
-- (ctrlC (return $ Just ""))
-+ x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt)
- case x of
- Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
- return ()
- Just input -> -- H.catch
-- do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)
-- (ctrlC (return (Just mods)))
-+ do ms <- H.handleInterrupt (ctrlC (return (Just mods))) (H.withInterrupt $ lift $ processInput input orig mods efile)
- case ms of
- Just mods -> let efile' = fromMaybe efile (listToMaybe mods)
- in repl orig mods efile'
- Nothing -> return ()
- -- ctrlC)
- -- ctrlC
-- where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
-- ctrlC act e = do lift $ iputStrLn (show e)
-- act -- repl orig mods
-+ where ctrlC :: InputT Idris a -> InputT Idris a
-+ ctrlC act = do lift $ iputStrLn "Interrupted"
-+ act -- repl orig mods
-
- showMVs c thm [] = ""
- showMVs c thm ms = "Holes: " ++
diff --git a/gnu/packages/patches/idris-build-with-megaparsec-9.patch b/gnu/packages/patches/idris-build-with-megaparsec-9.patch
deleted file mode 100644
index 6d7ff1d713..0000000000
--- a/gnu/packages/patches/idris-build-with-megaparsec-9.patch
+++ /dev/null
@@ -1,27 +0,0 @@
-From 6ea9bc913877d765048d7cdb7fc5aec60b196fac Mon Sep 17 00:00:00 2001
-From: Felix Yan <felixonmars@HIDDEN>
-Date: Wed, 16 Dec 2020 21:48:32 +0800
-Subject: [PATCH] Fix compatibility with megaparsec 9
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4892>
-
- src/Idris/Parser/Stack.hs | 4 ++++
- 1 file changed, 4 insertions(+)
-
-diff --git a/src/Idris/Parser/Stack.hs b/src/Idris/Parser/Stack.hs
-index fb7b611440..879786f4d2 100644
---- a/src/Idris/Parser/Stack.hs
-+++ b/src/Idris/Parser/Stack.hs
-@@ -84,7 +84,11 @@ instance Message ParseError where
- (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
- #endif
- messageText = PP.text . init . P.parseErrorTextPretty . parseError
-+#if MIN_VERSION_megaparsec(9,0,0)
-+ messageSource err = sline
-+#else
- messageSource err = Just sline
-+#endif
- where
- #if MIN_VERSION_megaparsec(8,0,0)
- (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
diff --git a/gnu/packages/patches/idris-disable-test.patch b/gnu/packages/patches/idris-disable-test.patch
deleted file mode 100644
index ec8c7c8451..0000000000
--- a/gnu/packages/patches/idris-disable-test.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-The "pkg010" test output depends on the version of optparse-applicative being
-used. The expected output requires optparse-applicative >= 0.15.1.0. Skip
-the test for now.
-
---- idris-1.3.3/test/TestData.hs 2021-01-19 23:05:24.238958262 -0600
-+++ idris-1.3.3/test/TestData.hs 2021-01-19 23:10:33.314390997 -0600
-@@ -212,8 +212,10 @@
- ( 5, ANY ),
- ( 6, ANY ),
- ( 7, ANY ),
-- ( 8, ANY ),
-- ( 10, ANY )]),
-+ ( 8, ANY )]),
-+-- FIXME: Expected output depends on optparse-applicative version.
-+-- See https://github.com/idris-lang/Idris-dev/issues/4896
-+-- ( 10, ANY )]),
- ("prelude", "Prelude",
- [ ( 1, ANY )]),
- ("primitives", "Primitive types",
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 14 Apr 2022 12:21:11 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Thu Apr 14 08:21:11 2022
Received: from localhost ([127.0.0.1]:55524 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1neyTG-0001Ke-Pf
for submit <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:11 -0400
Received: from mail-ed1-f46.google.com ([209.85.208.46]:39686)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1neyTF-0001KQ-7v
for 49607 <at> debbugs.gnu.org; Thu, 14 Apr 2022 08:21:09 -0400
Received: by mail-ed1-f46.google.com with SMTP id g20so6102998edw.6
for <49607 <at> debbugs.gnu.org>; Thu, 14 Apr 2022 05:21:09 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:mime-version
:content-transfer-encoding;
bh=5uWmftaN+JM06weGFTVE1BwNmo2pgFzoR3j0YUdtFPo=;
b=GL0G6l1gf4IraQGca5us91WEYP+K5sAH7hz7/OWWqw3Q6vCrdBU6whItu/RWnlPpqn
3C/nc3rZUB/ryGK2GoEDWEz6sqkP/WdgZL0p18R/ZV/OzqfMEcCc9eBDtNZHzlq8BfHT
guMx6hgIVpdUh4V0+Hw/MpH/Ox9JyPelv5iLPQofUNRj3xsgReIfdX4kjjI6qr/dTpvA
66fpS8XLJoPCQ4wAbo0tyalsa47iCWf+0hmmto5HuGcT9D+lZcSWTxkTtz+rPraN6QmC
bQZ2x/yWFYjQQOm9blZhVjrWRg0f/VgzRaeefgfNnh96wrIcMSrPSVPJCZW2sCF3P9kv
P2SA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:mime-version:content-transfer-encoding;
bh=5uWmftaN+JM06weGFTVE1BwNmo2pgFzoR3j0YUdtFPo=;
b=WC+HI/p0OTu5eSEO9KJ8euf+QzvhMPcvEUyin07Wb7qVjkrpAe6SKqKXOnTAANP8nF
0IgG/TSxsu6PixMdHvMBk/n3ayn/TE6fZQ5CL04WBEikxJkIzgMypNw1Bi/IRUw6Q16W
ErIbO6NPzpQoereR4n/E8c7y/RutonNqoL5UyEcv9U9qg14a1zK/MIkBbhCsEiEbaBXb
YO0EKkZuvFLKoEBQoWbtlpSTDgbGWAlWoAN3BRuEl0tXWgY4/RnDP8nSRW2Evp9L4DCN
VLAw5qcJQma/AShyWZ2ZaQ3/XCthrJ3q7bJJGaac1DVESHZskerZSIhIcctRDNJ1bt0d
iF1w==
X-Gm-Message-State: AOAM5326B0vhOa7WJlODORv6Pt8mqIpPHWvBU4eIaI8okLsmglzurgud
mcjTPA3NkcbbiF9XTnPC/AQ9LK+SnoI=
X-Google-Smtp-Source: ABdhPJyYvr5C6qDIg0ZitcyyZR6SEm7LCJBFXtUleUnI+fwJWxiSQIbJ+upiqggpsWhHqsysB+3AzQ==
X-Received: by 2002:a50:ff0a:0:b0:419:4240:3be4 with SMTP id
a10-20020a50ff0a000000b0041942403be4mr2657678edu.304.1649938863152;
Thu, 14 Apr 2022 05:21:03 -0700 (PDT)
Received: from lelap.local (catv-89-132-245-188.catv.fixed.vodafone.hu.
[89.132.245.188]) by smtp.gmail.com with ESMTPSA id
u3-20020a17090657c300b006d01de78926sm582042ejr.22.2022.04.14.05.21.02
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Thu, 14 Apr 2022 05:21:02 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
Date: Thu, 14 Apr 2022 14:16:11 +0200
Message-Id: <20220414121612.9815-1-attila@HIDDEN>
X-Mailer: git-send-email 2.35.1
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.3 to
prepare for adding different versions later on.
[inputs]: Add Clang, and bash-minimal (for wrap-program).
[phases]: use (cc-for-target).
---
i think v2 is ready for inclusion. it can bootstrap idris all the way
from GHC, but it also enables a/the bootstrap shortcut for the latest
version, and disables substitution for the so called historical
versions by default.
a bootstrap shortcut is when the makefile builds a checked in build
output, which is a scheme file, using Chez Scheme.
this way the build farm is not loaded unnecessarily with building a
full chain of bootstrap, but at the same time users can trigger/install
any of the old versions manually.
gnu/packages/idris.scm | 28 ++++++++++++++++++----------
1 file changed, 18 insertions(+), 10 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index cdf76244fb..f84431cab9 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,10 +21,12 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
#:use-module (gnu packages libffi)
+ #:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
@@ -33,9 +35,10 @@ (define-module (gnu packages idris)
#:use-module (guix download)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (guix utils))
-(define-public idris
+(define-public idris-1.3.3
(package
(name "idris")
(version "1.3.3")
@@ -56,7 +59,8 @@ (define-public idris
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
ghc-tasty-rerun))
(inputs
- (list gmp
+ (list bash-minimal
+ gmp
ncurses
ghc-aeson
ghc-annotated-wl-pprint
@@ -95,8 +99,7 @@ (define-public idris
;; This allows us to call the 'idris' binary before installing.
(add-after 'unpack 'set-ld-library-path
(lambda _
- (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))
- #t))
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))))
(add-before 'configure 'update-constraints
(lambda _
(substitute* "idris.cabal"
@@ -104,8 +107,7 @@ (define-public idris
dep))))
(add-before 'configure 'set-cc-command
(lambda _
- (setenv "CC" "gcc")
- #t))
+ (setenv "CC" ,(cc-for-target))))
(add-after 'install 'fix-libs-install-location
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
@@ -122,7 +124,6 @@ (define-public idris
(let ((out (assoc-ref outputs "out")))
(chmod "test/scripts/timeout" #o755) ;must be executable
(setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
- (setenv "IDRIS_CC" "gcc") ;Needed for creating executables
(setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
(apply (assoc-ref %standard-phases 'check) args))))
(add-before 'check 'restore-libidris_rts
@@ -134,8 +135,13 @@ (define-public idris
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))
- #t))))))
+ (string-append out filename)))))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target))))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -149,6 +155,8 @@ (define-public idris
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3.3)
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
--
2.35.1
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 5 Oct 2021 16:47:59 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Oct 05 12:47:59 2021
Received: from localhost ([127.0.0.1]:41745 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1mXnbi-00020X-E1
for submit <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:47:58 -0400
Received: from mail-ed1-f46.google.com ([209.85.208.46]:35378)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1mXnbc-0001zx-Cb
for 49607 <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:47:56 -0400
Received: by mail-ed1-f46.google.com with SMTP id b8so1259276edk.2
for <49607 <at> debbugs.gnu.org>; Tue, 05 Oct 2021 09:47:52 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=3iHNUeVDPh33Vb+Y9J04Uen/qwU4czBRZ9FMfloTa50=;
b=bIc+xH2plV/N7wwJPBgC88HUUzOBHOl2+mhnclwunhTSNXPpopGuZdI739xKvda0pi
CKcyUuJfGVlaF5KUDW7zfeQ6R65ehN5+A/B2esPnuAeW1Qj7XjScKVWB0x8geZnz2t4k
ihgJTOWC5QZsfwJ6M+rEELK+dL6fFoTDr/evo37MkpecJZjQzZ67+pNRk8uA41h7DvoD
+JjbDn+pEwj15ifYawtO6/baVNVmO6fPSdzUa2Ol1rXAMdgIaxQ0xhZZlX/M+8cDXBo7
poxcBBMdQ+hcPYTshGiK2dQwD8vhUT5jHAmwIuuG2nXXf0OU+le1TJpiPSoXVqug+Cm2
SXjA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=3iHNUeVDPh33Vb+Y9J04Uen/qwU4czBRZ9FMfloTa50=;
b=XZh+fD2nZX16dbDlLFC79Fy2d24mAv6R1sk1hVd+m926G30FIYxIUK1DYHHOUgEXt9
SmlahbREQiMM0n0Qf8mP7lc/HXULfrt9zT4JQNI6VyluKSApprSCJ9xXFzsN3m6SnvlM
YeqRvUas5/YYQgXwk/X0EMphR1Uft/TAFZLpHzMeJgJKPYUGYT96wo7DopDtNlPMPBHF
3KnNR6Jcsk5sPHiDLXIyX2zT00gdeGOZpX76XZGijEcIOQi5hpaooT87hudIT3q/TVLQ
7UVW+2XX+U2EtmHCEzS27SLza2dkTOsL+Vr5tJocpI/OHQvlp5aIM/g6jrT/CJutlE+N
tjkg==
X-Gm-Message-State: AOAM533BknAKPI6bAnpbPWA0JwbWz7qqIJPo5yT0IBsVtJKzQD7sdaR3
7Urqh/eYL8vmz4qljCcnIUJ92ssIav8=
X-Google-Smtp-Source: ABdhPJzjqIxrEzi49YptjrbxDCDhFcVxKGmoQx0T0Pvoo982tGfi1BzKlYiqiqcnlp1gUGeiOPy+Ug==
X-Received: by 2002:a17:907:9604:: with SMTP id
gb4mr26423866ejc.142.1633452466496;
Tue, 05 Oct 2021 09:47:46 -0700 (PDT)
Received: from lelap.lan (catv-213-222-131-28.catv.broadband.hu.
[213.222.131.28])
by smtp.gmail.com with ESMTPSA id n6sm8999335eds.10.2021.10.05.09.47.45
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Tue, 05 Oct 2021 09:47:46 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986.
Date: Tue, 5 Oct 2021 18:37:58 +0200
Message-Id: <20211005163757.29637-3-attila@HIDDEN>
X-Mailer: git-send-email 2.33.0
In-Reply-To: <20211005163757.29637-1-attila@HIDDEN>
References: <20211005163757.29637-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
This generality is there because with this it is possible to bootstrap Idris
HEAD all the way down from GHC. It requires patching past releases, which
requires importing them into separate git branches. This has not been merged
into upstream yet, therefore this commit only contains a single use of
MAKE-IDRIS-PACKAGE, but that will change in the future.
Add a symlink to a versioned binary; e.g. add a `bin/idris-1.3.3`.
* gnu/packages/idris.scm (idris-1.3.3-1): New variable, the latest git commit
from the v1.x line of Idris.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2-0.5.1): New variable.
---
gnu/packages/idris.scm | 182 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 179 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 1f6e984a90..4ef18c6da4 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -19,9 +19,22 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This needs patching Idris so that it
+;;; stops using a wrapper script and finds its libidris_support.so
+;;; e.g. relative to the executable.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -29,14 +42,21 @@
#:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
(define-public idris-1.3.3
(package
@@ -148,8 +168,10 @@
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target)))))
- #true)))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #t)))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -165,6 +187,160 @@ Epigram and Agda.")
(define-public idris idris-1.3.3)
+(define-public idris-1.3.3-1
+ ;; This is the current latest from the v1.x branch.
+ (let ((commit "55459867fc3f1ac34527a5dd998c37e72b15d488")
+ (revision "1"))
+ (package
+ (inherit idris-1.3.3)
+ (version (git-version "1.3.3" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/attila-lendvai/Idris2")
+ (commit commit)))
+ (sha256
+ (base32
+ "0qsn1953jy74pgppwkax8yrlswb3v46x541ahbl95rshf666nsj6"))
+ (file-name (git-file-name "idris" version))))
+ (inputs
+ (append (package-inputs idris-1.3.3)
+ `(("ghc-haskeline-0.8" ,ghc-haskeline-0.8)))))))
+
+(define* (make-idris-package source version
+ #:key bootstrap-idris
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"))
+ (with-bootstrap-shortcut? #true))
+ (package
+ (name "idris2")
+ (version version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((? git-checkout?)
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(,@(if with-bootstrap-shortcut?
+ `(("chez-scheme" ,chez-scheme))
+ `(("bootstrap-idris" ,bootstrap-idris)))
+ ("cc" ,clang-toolchain-12) ; clang or older clang-toolchain's don't have a bin/cc
+ ("coreutils" ,coreutils)
+ ("git" ,git)
+ ("node" ,node) ; only for the tests
+ ("racket" ,racket) ; only for the tests
+ ("sed" ,sed)))
+ (inputs
+ `(("bash" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)
+ ("gmp" ,gmp)))
+ (arguments
+ `(#:tests? ,tests?
+ #:make-flags
+ (list (string-append "CC=" ,(cc-for-target))
+ ,@(if with-bootstrap-shortcut?
+ '((string-append "SCHEME="
+ (assoc-ref %build-inputs "chez-scheme")
+ "/bin/scheme"))
+ `((string-append "BOOTSTRAP_IDRIS="
+ (assoc-ref %build-inputs "bootstrap-idris")
+ "/bin/" ,(package-name bootstrap-idris))))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* ',files-to-patch-for-shell
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env")))
+ #true))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let ((out (assoc-ref outputs "out")))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file (string-append out "/bin/idris2_app/idris2.so")
+ (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib")))
+ #true)))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #true))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (apply invoke "make"
+ "INTERACTIVE="
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ "test" make-flags))
+ #true)))))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+types. It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
--
2.33.0
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 5 Oct 2021 16:47:53 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Oct 05 12:47:53 2021
Received: from localhost ([127.0.0.1]:41743 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1mXnbc-00020G-Uh
for submit <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:47:53 -0400
Received: from mail-ed1-f47.google.com ([209.85.208.47]:45794)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1mXnbb-0001zr-I1
for 49607 <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:47:52 -0400
Received: by mail-ed1-f47.google.com with SMTP id r18so1254904edv.12
for <49607 <at> debbugs.gnu.org>; Tue, 05 Oct 2021 09:47:51 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:in-reply-to:references
:mime-version:content-transfer-encoding;
bh=9lmrrjRr9ey1wAA35cKXdhVsPUKS0uzBnApt5UnZsxo=;
b=PkqqmKcg3qWsJPl7H7L8WD83i2giK5Y6Tbvpiv53deUdkm66GgK0CMD4PyaHaKnJ/i
cFdz9oLyQ0XOnWqil5hyf8Ibudi+RTqKu+ezIOrm4o8ACxpIVycrBQggUTo+U7RnDSo4
mRqwsOxiNeHnn+StYF8ZRLsrLHIntf0DFE6fvUBUB4nEjagZCzuoBdDaf/RAEiD0Om/b
0PF+P1uZjzz3LGZOtt9MVLjmkjK8ZTgYLKRu1MqH9I2bYZcFTiqT5G2wz3ybz7oDKdEG
z82ds9x8tUxcY5yI/XALw5GsqeyQ3ikNBf7cWvEpVYS0oM18evnvhH+2dah66S8aI0oD
bMNQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:in-reply-to:references:mime-version:content-transfer-encoding;
bh=9lmrrjRr9ey1wAA35cKXdhVsPUKS0uzBnApt5UnZsxo=;
b=JRsCPlVgxzgYtgd3AaoFfWTbtqqeLtCbHAmKVnhE1b20fBNTbGRTKyNgYeoq5e1J+8
PTPgoiCkoLbqdtC+Wqn2/v2S04FPlj9xHISdOQnCfKXjU39W35bpRyUWglIBsZbb7LSx
GZcdefYUIB7uNTPP5dHsIjkcYd+YVIGcVqOZQX2ohi0yeJALRvHqOEabGSracs+4XXv4
6dsLRStDb1U6b8fanEGitTog+a36IxJSCkGObBDYd/FUYFoXXZ9qzc81g26G1W1dPOXP
tFgVsIwoxhgDVPjFij74LJkSFVUgtCUDadotndDhy8UI2jfJldYOhri4975gxNI2WCfT
kPZw==
X-Gm-Message-State: AOAM531Z5TYuTgJx7zJG6eHpeQfWCyl5ttS2ldUg2Nl3jC0wqT/F0acR
22uo2hOG8Oz9UTz8YnQA53NeRo+txyo=
X-Google-Smtp-Source: ABdhPJzD+lEKLY53ykCLiwEZHHH512+rSbbBBlPVj/an8yX1PZ+AQQRzkXF98NzuMwA0+Ut0jZMYLw==
X-Received: by 2002:a05:6402:3088:: with SMTP id
de8mr27731733edb.76.1633452465842;
Tue, 05 Oct 2021 09:47:45 -0700 (PDT)
Received: from lelap.lan (catv-213-222-131-28.catv.broadband.hu.
[213.222.131.28])
by smtp.gmail.com with ESMTPSA id n6sm8999335eds.10.2021.10.05.09.47.45
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Tue, 05 Oct 2021 09:47:45 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC
Date: Tue, 5 Oct 2021 18:37:57 +0200
Message-Id: <20211005163757.29637-2-attila@HIDDEN>
X-Mailer: git-send-email 2.33.0
In-Reply-To: <20211005163757.29637-1-attila@HIDDEN>
References: <20211005163757.29637-1-attila@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.3 to
prepare for adding different versions later on.
[inputs]: Add Clang, and bash-minimal (for wrap-program).
[phases]: use (cc-for-target).
---
gnu/packages/idris.scm | 31 +++++++++++++++++++++++--------
1 file changed, 23 insertions(+), 8 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 058d679c1f..1f6e984a90 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,10 +21,12 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
#:use-module (gnu packages libffi)
+ #:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
@@ -33,9 +35,10 @@
#:use-module (guix download)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (guix utils))
-(define-public idris
+(define-public idris-1.3.3
(package
(name "idris")
(version "1.3.3")
@@ -51,12 +54,15 @@
(build-system haskell-build-system)
(native-inputs ;For tests
`(("perl" ,perl)
+ ("clang" ,clang) ; the tests want to generate exeutables
("ghc-cheapskate" ,ghc-cheapskate)
("ghc-tasty" ,ghc-tasty)
("ghc-tasty-golden" ,ghc-tasty-golden)
("ghc-tasty-rerun" ,ghc-tasty-rerun)))
(inputs
- `(("gmp" ,gmp)
+ `(("bash" ,bash-minimal)
+ ("clang" ,clang) ; FIXME clang compiles faster than gcc, but (cc-for-target) ignores it
+ ("gmp" ,gmp)
("ncurses" ,ncurses)
("ghc-aeson" ,ghc-aeson)
("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint)
@@ -105,7 +111,7 @@
#t))
(add-before 'configure 'set-cc-command
(lambda _
- (setenv "CC" "gcc")
+ (setenv "CC" ,(cc-for-target))
#t))
(add-after 'install 'fix-libs-install-location
(lambda* (#:key outputs #:allow-other-keys)
@@ -116,14 +122,14 @@
(lambda (module)
(symlink (string-append modules "/" module)
(string-append lib "/" module)))
- '("prelude" "base" "contrib" "effects" "pruviloj")))))
+ '("prelude" "base" "contrib" "effects" "pruviloj")))
+ #t))
(delete 'check) ;Run check later
(add-after 'install 'check
(lambda* (#:key outputs #:allow-other-keys #:rest args)
(let ((out (assoc-ref outputs "out")))
(chmod "test/scripts/timeout" #o755) ;must be executable
(setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
- (setenv "IDRIS_CC" "gcc") ;Needed for creating executables
(setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
(apply (assoc-ref %standard-phases 'check) args))))
(add-before 'check 'restore-libidris_rts
@@ -135,8 +141,15 @@
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))
- #t))))))
+ (string-append out filename)))
+ #t))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target)))))
+ #true)))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -150,6 +163,8 @@ can be specified precisely in the type. The language is closely related to
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3.3)
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
--
2.33.0
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at 49607) by debbugs.gnu.org; 5 Oct 2021 16:46:51 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Oct 05 12:46:51 2021
Received: from localhost ([127.0.0.1]:41738 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1mXnad-0001wY-Je
for submit <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:46:51 -0400
Received: from mail-ed1-f50.google.com ([209.85.208.50]:41854)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <attila.lendvai@HIDDEN>) id 1mXnac-0001wL-Jp
for 49607 <at> debbugs.gnu.org; Tue, 05 Oct 2021 12:46:50 -0400
Received: by mail-ed1-f50.google.com with SMTP id z1so1201620edb.8
for <49607 <at> debbugs.gnu.org>; Tue, 05 Oct 2021 09:46:50 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=sender:from:to:cc:subject:date:message-id:mime-version
:content-transfer-encoding;
bh=1I5BaeTqHvYeDiG6IdLQWke8UtWz86e+BvGeVIoTFAQ=;
b=lLwP7H8VDcC1iVjwsBpEK/btd8zBLBW2+WfqrcRhUI2j7Ovg402eNQWuvHLJLmnE3V
qP0t9FCIfyaK7J9nL1v0ke4ts4H3Jxt9peKqYmhZrELdWqUeVs36jjgl2qRtLnGSIOfd
y9VOJEu5zZSGkMx6manuM7Fn21XujQiE4NH/SirxHaMd8u+6p7IQxyEHj36Oov9lG49h
1OjdSKlE0v55rcgRL33BMN8qRqqR+Iuw0dwTXZ6gvI8flQm0kY6mzjN60uWxvdHG28TG
AqYJ/oEaSkq41CMhQdXSTXiQe+4XcZ3139EKH4XtLVqIE/wN01sxLZS4NtV9L5TI/BW2
1+/w==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:sender:from:to:cc:subject:date:message-id
:mime-version:content-transfer-encoding;
bh=1I5BaeTqHvYeDiG6IdLQWke8UtWz86e+BvGeVIoTFAQ=;
b=40/H3S8OtyAbj1LtYneXUSsiUGg9PknEm2GqYR3A95kRoR2H6Tk1jE4VGaJ+vl9xti
TxD2oIEjcCsw9Js4KC18p5hcPzKs7OisxeyuMgpdvLVeCPSVUJ0fD2s7xJ736C+pJU58
qckcgkPU39SWQqaCT2TrU1CC5446hADm2Uaz1JcpTVDx4gmeN7yjtTYWTqAs7GQj31Pe
N1KmaDGorjFXvUZXpLeKMlmMMHS/epRhHFiH55Dih88Ed+LjfDegxElm7SOSslqjkPp5
+GuQtN7duGM3hksjyNM+m+dqyjsyGH401y9YzohENQ6Ue5/Oto+vKJSks1K+tXKXuP4E
xFVg==
X-Gm-Message-State: AOAM531QR1mGxB6E3kC3YQlKANPLWmtrz1irCN0IyboKJfQd/hjFLyZ/
Bt6v7ZYljcBt5AJydvBUIltMYjWydDQ=
X-Google-Smtp-Source: ABdhPJyHCOkx7Q0IvDJA71ToAuXrwL3bulKdObPVzt/l0jy9KP6/scL637uSfgTjB50Cc6HhzN+kig==
X-Received: by 2002:a17:906:f2cd:: with SMTP id
gz13mr18290827ejb.278.1633452404534;
Tue, 05 Oct 2021 09:46:44 -0700 (PDT)
Received: from lelap.lan (catv-213-222-131-28.catv.broadband.hu.
[213.222.131.28])
by smtp.gmail.com with ESMTPSA id n6sm8999335eds.10.2021.10.05.09.46.43
(version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
Tue, 05 Oct 2021 09:46:43 -0700 (PDT)
From: Attila Lendvai <attila@HIDDEN>
To: 49607 <at> debbugs.gnu.org
Subject: [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2
Date: Tue, 5 Oct 2021 18:37:56 +0200
Message-Id: <20211005163757.29637-1-attila@HIDDEN>
X-Mailer: git-send-email 2.33.0
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: 0.5 (/)
X-Debbugs-Envelope-To: 49607
Cc: Attila Lendvai <attila@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.5 (/)
* gnu/packages/haskell-xyz.scm (ghc-cheapskate): Update to 0.1.1.2
* gnu/packages/idris.scm (idris-1.3.3): Delete now unnecessary substitute
---
i have many plans for further changes, but i thought i'll
send this meanwhile, so that everyone can have a fresh
idris on their guix.
this doesn't build/install the docs. may add it later.
gnu/packages/haskell-xyz.scm | 4 ++--
gnu/packages/idris.scm | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index f421458e15..87ebe4f3b6 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -1966,7 +1966,7 @@ Partial and Infinite Values\"}.")
(define-public ghc-cheapskate
(package
(name "ghc-cheapskate")
- (version "0.1.1.1")
+ (version "0.1.1.2")
(source
(origin
(method url-fetch)
@@ -1976,7 +1976,7 @@ Partial and Infinite Values\"}.")
".tar.gz"))
(sha256
(base32
- "0qnyd8bni2rby6b02ff4bvfdhm1hwc8vzpmnms84jgrlg1lly3fm"))))
+ "17n6laihqrjn62l8qw4565nf77zkvrl68bjmc3vzr4ckqfblhdzd"))))
(build-system haskell-build-system)
(inputs
`(("ghc-blaze-html" ,ghc-blaze-html)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..058d679c1f 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -100,8 +100,8 @@
(add-after 'unpack 'update-constraints
(lambda _
(substitute* "idris.cabal"
- (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10")
- (("cheapskate >= 0\\.1\\.1\\.2 && < 0\\.2") "cheapskate >= 0.1.1.1 && < 0.2"))
+ ;; This is only needed for v1.3.3, later it got relaxed upstream
+ (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10"))
#t))
(add-before 'configure 'set-cc-command
(lambda _
--
2.33.0
guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
Received: (at submit) by debbugs.gnu.org; 17 Jul 2021 15:43:12 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sat Jul 17 11:43:12 2021
Received: from localhost ([127.0.0.1]:54572 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1m4mT2-0006cT-Qs
for submit <at> debbugs.gnu.org; Sat, 17 Jul 2021 11:43:12 -0400
Received: from lists.gnu.org ([209.51.188.17]:55888)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <public@HIDDEN>) id 1m4mT0-0006cL-Bk
for submit <at> debbugs.gnu.org; Sat, 17 Jul 2021 11:43:04 -0400
Received: from eggs.gnu.org ([2001:470:142:3::10]:45012)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <public@HIDDEN>)
id 1m4mT0-0000zO-3I
for guix-patches@HIDDEN; Sat, 17 Jul 2021 11:43:02 -0400
Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:55680
helo=mail.yoctocell.xyz)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <public@HIDDEN>)
id 1m4mSw-0007i1-O5
for guix-patches@HIDDEN; Sat, 17 Jul 2021 11:43:01 -0400
From: Xinglu Chen <public@HIDDEN>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz;
s=mail; t=1626536576;
bh=RR8ek8J5ILPEZ5m2GHpfTLuXJ5nvRlxabbqwFyKUQz4=;
h=From:To:Cc:Subject:Date;
b=EXWNI9GjkyJfx/BQrjDN51uMZWDaIcUOg9ETHQ8mTtMUAC/NmNhbcUPyFgq5B6UoA
jEA+SUTMIbVYppDK1tdxpvjb3vaf07nwNly2s+eJdWbo+Ome1iBiiOmtvXFAtW4m78
Eux31gQEWkQgFx/Y51q0X75F+O6iyTfNAF3SbxW4=
To: guix-patches@HIDDEN
Subject: [PATCH] gnu: Add Idris 2.
Message-Id: <ee2e60c3f133981cc5695ef93e1b4e87dff87c04.1626536112.git.public@HIDDEN>
Date: Sat, 17 Jul 2021 17:42:55 +0200
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Received-SPF: pass client-ip=87.96.130.155; envelope-from=public@HIDDEN;
helo=mail.yoctocell.xyz
X-Spam_score_int: 23
X-Spam_score: 2.3
X-Spam_bar: ++
X-Spam_report: (2.3 / 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, FROM_SUSPICIOUS_NTLD=0.499,
FROM_SUSPICIOUS_NTLD_FP=0.903, PDS_OTHER_BAD_TLD=1.997,
PDS_RDNS_DYNAMIC_FP=0.001, RDNS_DYNAMIC=0.982, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 2.1 (++)
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: From: raingloom <raingloom@HIDDEN> *
gnu/packages/idris.scm
(idris2): New variable. Co-authored-by: Xinglu Chen <public@HIDDEN>
--- Based a previous patch by raingloom[1].
Content analysis details: (2.1 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
-2.3 RCVD_IN_DNSWL_MED RBL: Sender listed at https://www.dnswl.org/,
medium trust [209.51.188.17 listed in list.dnswl.org]
1.0 SPF_SOFTFAIL SPF: sender does not match SPF record (softfail)
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.0 RCVD_IN_MSPIKE_H4 RBL: Very Good reputation (+4)
[209.51.188.17 listed in wl.mailspike.net]
0.0 RCVD_IN_MSPIKE_WL Mailspike good senders
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
0.9 FROM_SUSPICIOUS_NTLD_FP From abused NTLD
X-Debbugs-Envelope-To: submit
Cc: raingloom <raingloom@HIDDEN>
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 2.5 (++)
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: From: raingloom <raingloom@HIDDEN> * gnu/packages/idris.scm
(idris2): New variable. Co-authored-by: Xinglu Chen <public@HIDDEN>
--- Based a previous patch by raingloom[1].
Content analysis details: (2.5 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
1.0 SPF_SOFTFAIL SPF: sender does not match SPF record (softfail)
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs
[URI: yoctocell.xyz (xyz)]
0.5 FROM_SUSPICIOUS_NTLD From abused NTLD
-1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list
manager
From: raingloom <raingloom@HIDDEN>
* gnu/packages/idris.scm (idris2): New variable.
Co-authored-by: Xinglu Chen <public@HIDDEN>
---
Based a previous patch by raingloom[1].
Some changes I made:
* Tests are enabled, but only the Chez backend is enabled since that=E2=80=
=99s
the only backend we have for now.
* Some environment have been set, which should make it possible to
import third-party packages.
* The bin/idris2_app directory has been removed, see the comment in the
code below.
* The executable is wrapped so some environment variables can be set.
* I also changed the synopsis to the one on their GitHub page, and added
a copyright line for raingloom.
[1]: https://issues.guix.gnu.org/46124#1
gnu/packages/idris.scm | 120 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 119 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..64cb4f37f5 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -3,6 +3,8 @@
;;; Copyright =C2=A9 2016, 2017 David Craven <david@HIDDEN>
;;; Copyright =C2=A9 2018 Alex ter Weele <alex.ter.weele@HIDDEN>
;;; Copyright =C2=A9 2019, 2021 Eric Bavier <bavier@HIDDEN>
+;;; Copyrignt =C2=A9 2021 raingloom <raingloom@HIDDEN>
+;;; Copyright =C2=A9 2021 Xinglu Chen <public@HIDDEN>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -21,6 +23,8 @@
=20
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -28,12 +32,16 @@
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
+ #:use-module (gnu packages sphinx)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (guix utils)
+ #:use-module (ice-9 regex))
=20
(define-public idris
(package
@@ -150,6 +158,116 @@ can be specified precisely in the type. The language=
is closely related to
Epigram and Agda.")
(license license:bsd-3)))
=20
+;; TODO: Add other backends?
+(define-public idris2
+ (package
+ (name "idris2")
+ (version "0.4.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris2")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:test-target "bootstrap-test"
+ #:phases
+ (modify-phases
+ %standard-phases
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (substitute* "config.mk"
+ ((,(regexp-quote "PREFIX ?=3D $(HOME)/.idris2"))
+ (string-append "PREFIX =3D "
+ (assoc-ref outputs "out"))))
+ (substitute* '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss")
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash")
+ "/bin/sh")))))
+ ;; This is not the kind of bootstrap we want to run
+ (delete 'bootstrap)
+ (delete 'configure) ; no configure script
+ (replace 'build
+ (lambda _
+ (invoke "make" "bootstrap"
+ "SCHEME=3Dscheme"
+ ;; TODO: detect toolchain.
+ (string-append "CC=3D" ,(cc-for-target)))))
+ (add-after 'build 'build-doc
+ (lambda _
+ (with-directory-excursion
+ "docs"
+ (invoke "make" "html"))))
+ (add-before 'check 'set-cc
+ (lambda _
+ (setenv "CC" ,(cc-for-target))))
+ (add-after 'install 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (copy-recursively
+ "docs/build/html"
+ (string-append
+ (assoc-ref outputs "out")
+ "/share/doc/"
+ ,name "-" ,version))))
+ (add-after 'install-doc 'fix-ld-library-path
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let ((out (assoc-ref outputs "out")))
+ (delete-file (string-append out "/bin/idris2"))
+ (copy-file (string-append out "/bin/idris2_app/idris2.so")
+ (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_ap=
p")))))
+ (add-after 'fix-ld-library-path 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (idris2 (string-append out "/bin/idris2"))
+ (version ,version))
+ (wrap-program idris2
+ `("LD_LIBRARY_PATH" ":" prefix
+ (,(string-append out "/idris2-" version "/lib")))
+ `("CHEZ" ":" =3D (,chez)))))))))
+ (inputs
+ `(("bash" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)
+ ("gmp" ,gmp)))
+ (native-inputs
+ ;; For building docs.
+ `(("python-sphinx" ,python-sphinx)
+ ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+ ("python" ,python) ))
+ (native-search-paths
+ (list (search-path-specification
+ (variable "IDRIS2_PACKAGE_PATH")
+ (files (list (string-append "idris2-" version))))
+ (search-path-specification
+ (variable "IDRIS2_LIBS")
+ (files (list (string-append "idris2-" version "/lib")))
+ (file-type 'directory))
+ (search-path-specification
+ (variable "IDRIS2_DATA")
+ (files (list (string-append "idris2-" version "/support")))
+ (file-type 'directory))))
+ (home-page "https://idris-lang.org/")
+ (synopsis "Purely functional programming language with first class typ=
es")
+ (description
+ "Idris 2 is a general purpose language with dependent linear types.
+It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. It can use multiple languages as =
code
+generation backends.")
+ (license license:bsd-3)))
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH i=
s set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
base-commit: 9cb35c02164d929fcb8929e7f454df215df8cf25
--=20
2.32.0
Xinglu Chen <public@HIDDEN>:guix-patches@HIDDEN.
Full text available.guix-patches@HIDDEN:bug#49607; Package guix-patches.
Full text available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.