From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:36143) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fjtQ5-0000vg-CJ for guix-patches@gnu.org; Sun, 29 Jul 2018 17:40:06 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fjtQ2-0006Yn-8r for guix-patches@gnu.org; Sun, 29 Jul 2018 17:40:05 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:57357) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fjtQ2-0006Yb-5i for guix-patches@gnu.org; Sun, 29 Jul 2018 17:40:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1fjtQ1-0001sx-Uk for guix-patches@gnu.org; Sun, 29 Jul 2018 17:40:01 -0400 Subject: bug#32235: [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-To: guix-patches@gnu.org Resent-Message-ID: From: Marius Bakke In-Reply-To: <87d0v74b9a.fsf@fastmail.com> References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> <87a7qj5o6j.fsf@fastmail.com> <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87d0v74b9a.fsf@fastmail.com> Date: Sun, 29 Jul 2018 23:39:07 +0200 Message-ID: <874lgh4t8k.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Alex ter Weele Cc: 32235-done@debbugs.gnu.org --=-=-= Content-Type: text/plain Marius Bakke writes: > Alex ter Weele writes: > >> Marius Bakke writes: >> >>> Alex ter Weele writes: >>> >>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 >>>> From: Alex ter Weele >>>> Date: Fri, 20 Jul 2018 21:35:14 -0500 >>>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files. >>>> >>>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. >>> >>> [...] >>> >>>> + (arguments >>>> + `(#:modules ((guix build haskell-build-system) >>>> + (guix build utils) >>>> + (srfi srfi-26)) >>>> + #:phases >>>> + (modify-phases %standard-phases >>>> + (add-after 'compile 'agda-compile >>>> + (lambda* (#:key outputs #:allow-other-keys) >>>> + (let* ((out (assoc-ref outputs "out")) >>>> + (agda-compiler (string-append out "/bin/agda")) >>>> + (agda-files-path (string-append >>>> + out >>>> + "/share/x86_64-linux-ghc-8.0.2/Agda-" >>> >>> This is unfortunate, since it hard-codes both architecture and GHC >>> version. Can you think of another method to find these files? >>> >>> Are there ".agda" files elsewhere under "/share"? Could the find-files >>> invokation below simply search "out/share", for example? >>> >> >> That works! >> >>>> + ,version >>>> + "/lib/prim/Agda/")) >>>> + (agda-files (append >>>> + (find-files agda-files-path "\\.agda$") >>>> + (find-files (string-append >>>> + agda-files-path >>>> + "Builtin") >>>> + "\\.agda$")))) >>> >>> (find-files ...) recurses through subdirectories, are you sure adding an >>> extra pass for "Builtin/*.agda" makes a difference here? >>> >> >> Removed. >> >>>> + (for-each (cut invoke agda-compiler <>) agda-files) >>>> + #t)))))) >>>> (home-page "http://wiki.portal.chalmers.se/agda/") >>> >>> Otherwise LGTM. >>> >>> [...] >>> >>>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 >>>> From: Alex ter Weele >>>> Date: Sat, 21 Jul 2018 10:57:35 -0500 >>>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode >>>> >>>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable. >>> >>> LGTM! >> >> I found a few potential issues with it. The variable and package names >> were mismatched, the inputs were inherited, and the home page was >> misspelled. Corrected in the following patch series. >> >> Thanks for the review! > > Thanks for catching my review mistake! All LGTM. Whoops, Ludovic helpfully reminded me on IRC that you don't yet have commit access. I've pushed these patches. (note that I added a #t after the chdir for emacs-agda2-mode, since the return value of chdir is unspecified) --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAlteM/sACgkQoqBt8qM6 VPpMggf/RzgJhxbYy87xtJOUPuAcUg8nnoWiZC9xS8+yz6+gUUPMXa+FuoW3Rb8H j3zcilxfk4G+Wb0FNlojfPHnhbyjKMTJGX8/FUR8DrdZsUW9nXhFF0AdhmDQUDHb JqqJqVPPTqx/QSO8Gh5plJsbegMXHf8XDExQ7RtiyxlYooNefOBD030rTm5t9Sfj yAAXMyLeDMOdM4I2Hz3+sKUNbCmFSZPmLYUT15XnodrR/KaWtfMvdGj86Tv/RjXk ze6QYiif6I73msFNJIpi2pjX3hhslXeLM5FTMlOUjSnI474TypsBqBK+XEKjJG7p tDNirm9IyWIMOl/Dnu3FJV3svkS40A== =dw1p -----END PGP SIGNATURE----- --=-=-=--