From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:45315) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fjF9M-0002Ul-Aa for guix-patches@gnu.org; Fri, 27 Jul 2018 22:40:09 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fjF9H-0007xR-CK for guix-patches@gnu.org; Fri, 27 Jul 2018 22:40:08 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:55656) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fjF9H-0007x1-2H for guix-patches@gnu.org; Fri, 27 Jul 2018 22:40:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1fjF9G-0007Z0-Ho for guix-patches@gnu.org; Fri, 27 Jul 2018 22:40:02 -0400 Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-Message-ID: From: Alex ter Weele 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> Date: Fri, 27 Jul 2018 21:39:33 -0500 In-Reply-To: <87a7qj5o6j.fsf@fastmail.com> (Marius Bakke's message of "Sun, 22 Jul 2018 16:40:20 +0200") Message-ID: <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" 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: Marius Bakke Cc: Alex ter Weele , 32235@debbugs.gnu.org --=-=-= Content-Type: text/plain 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! --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0001-gnu-agda-Compile-.agda-files.patch >From 51ad1e736760fb083fd04d933f9aaf6658b4b7fe 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. --- gnu/packages/agda.scm | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 6aa230116..d677bb7e5 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -67,6 +67,19 @@ ("ghc-text" ,ghc-text) ("ghc-unordered-containers" ,ghc-unordered-containers) ("ghc-zlib" ,ghc-zlib))) + (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"))) + (for-each (cut invoke agda-compiler <>) + (find-files (string-append out "/share") "\\.agda$")) + #t)))))) (home-page "http://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") -- 2.18.0 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0002-gnu-Add-emacs-agda2-mode.patch >From b57cfb8766e85a4c2c8491415f2bf0d9357bcca2 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. --- gnu/packages/agda.scm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index d677bb7e5..7bdf10e61 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -20,6 +20,7 @@ #:use-module (gnu packages haskell) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) + #:use-module (guix build-system emacs) #:use-module (guix build-system haskell) #:use-module (guix build-system trivial) #:use-module (guix download) @@ -97,3 +98,19 @@ such as Coq, Epigram and NuPRL.") ;; Agda is distributed under the MIT license, and a couple of ;; source files are BSD-3. See LICENSE for details. (license (list license:expat license:bsd-3)))) + +(define-public emacs-agda2-mode + (package + (inherit agda) + (name "emacs-agda2-mode") + (build-system emacs-build-system) + (inputs '()) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-after 'unpack 'enter-elisp-dir + (lambda _ (chdir "src/data/emacs-mode")))))) + (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html") + (synopsis "Emacs mode for Agda") + (description "This Emacs mode enables interactive development with +Agda. It also aids the input of Unicode characters."))) -- 2.18.0 --=-=-=--