From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:59458) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fjRO1-00041I-Pd for guix-patches@gnu.org; Sat, 28 Jul 2018 11:44:06 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fjRNy-0008Br-Kf for guix-patches@gnu.org; Sat, 28 Jul 2018 11:44:05 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:56265) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fjRNy-0008BY-GE for guix-patches@gnu.org; Sat, 28 Jul 2018 11:44:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1fjRNy-00010s-9G for guix-patches@gnu.org; Sat, 28 Jul 2018 11:44:02 -0400 Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-Message-ID: From: Marius Bakke In-Reply-To: <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> 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> Date: Sat, 28 Jul 2018 17:42:57 +0200 Message-ID: <87d0v74b9a.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@debbugs.gnu.org --=-=-= Content-Type: text/plain 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. --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAltcjwEACgkQoqBt8qM6 VPqaFwgAgIYoF+a+pyEHKzSBd37tHuIeWDAiTtPXd/I63/RlS/wc8NnPtEALB7uT B6Lj4SwqRYNrE1nH0rsVMJbT12ePNsYpUBcLL2+Oc4y92xPY4rG11U5j+L4Z8yWw 7Cr3JADxJ2YlaH9vhCKIa8duGGZAwFPL9edz0r0IJ0cWvUDojXMpU5ZGOuOEw4wI wPz3Jm7dGNN3n0iEJFse94QcoOY0ZoQaG/ZbSOG5mmiK0zKxSdzrjM3CzpXanzVc QvFiKYmDJPC2nHi6hPDiejpQmOhkN1jDo6uZc6eW6UkS98BHeSS4bvGvwWWX0A8Y jUE1cKh1i7aj0N1sr6snDCFjkA8dig== =3KsZ -----END PGP SIGNATURE----- --=-=-=--