From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:33345) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fguXE-0002LT-UZ for guix-patches@gnu.org; Sat, 21 Jul 2018 12:15:10 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fguX9-0004SZ-SK for guix-patches@gnu.org; Sat, 21 Jul 2018 12:15:08 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:46221) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fguX9-0004S6-Il for guix-patches@gnu.org; Sat, 21 Jul 2018 12:15:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1fguX7-0000se-Qn for guix-patches@gnu.org; Sat, 21 Jul 2018 12:15:03 -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> Date: Sat, 21 Jul 2018 11:13:52 -0500 In-Reply-To: (GNU bug Tracking System's message of "Sat, 21 Jul 2018 16:01:02 +0000") Message-ID: <87va98o9bz.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: 32235@debbugs.gnu.org --=-=-= Content-Type: text/x-patch Content-Disposition: attachment; filename=0001-gnu-agda-Compile-.agda-files.patch >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. --- gnu/packages/agda.scm | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 6aa230116..f7474aae3 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -67,6 +67,29 @@ ("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")) + (agda-files-path (string-append + out + "/share/x86_64-linux-ghc-8.0.2/Agda-" + ,version + "/lib/prim/Agda/")) + (agda-files (append + (find-files agda-files-path "\\.agda$") + (find-files (string-append + agda-files-path + "Builtin") + "\\.agda$")))) + (for-each (cut invoke agda-compiler <>) agda-files) + #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: attachment; filename=0002-gnu-Add-emacs-agda2-mode.patch >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. --- gnu/packages/agda.scm | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index f7474aae3..1a2078c07 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) @@ -107,3 +108,18 @@ 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 "agda2-mode") + (build-system emacs-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-after 'unpack 'enter-elisp-dir + (lambda _ (chdir "src/data/emacs-mode")))))) + (home-page "https://agda.readthdocs.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 --=-=-=--