From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:53719) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fhFXl-0004Fk-Lb for guix-patches@gnu.org; Sun, 22 Jul 2018 10:41:06 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fhFXi-0003No-Fl for guix-patches@gnu.org; Sun, 22 Jul 2018 10:41:05 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:47492) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fhFXi-0003Nd-Bh for guix-patches@gnu.org; Sun, 22 Jul 2018 10:41:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1fhFXi-00015H-5b for guix-patches@gnu.org; Sun, 22 Jul 2018 10:41:02 -0400 Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-Message-ID: From: Marius Bakke In-Reply-To: <87va98o9bz.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> Date: Sun, 22 Jul 2018 16:40:20 +0200 Message-ID: <87a7qj5o6j.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 , 32235@debbugs.gnu.org --=-=-= Content-Type: text/plain 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? Worst case scenario we'll have to dynamically generate that GHC path based on architecture and version, but hoping there's another way. > + ,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? > + (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! --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAltUl1QACgkQoqBt8qM6 VPqKZgf+P0xxg4CypdzrgeEWaffg3IC5M8H96uKxVAbFi/tNCSmEK6I2Ay0ceC7g ParMhCCDwVlZtrfpEP1TqnOVZ1ZIC/dmc8dn2Qq33lhTUfSDXqAmOlXcmH5F1jeV MNMa+4FSPXSrVt4wX8rNIlHd1w37puNe4AsPCFX7wJtcY956kacsym4d/XseOoKm Q+Y1DhcmsqY36qeBPeYwMgw+YhFrhErwHdAk9VftSyLrpxcUXZ7mZRfPG5OWrBld tD5SNIRwrx+TMPOm0RDECFtJVqZfkdDDElrJyde0hMWajvqyCuVupgAhi4j6XVsg 7YxVmCTLjlQpjB5+3I7D+uIOokjXKw== =uRW1 -----END PGP SIGNATURE----- --=-=-=--