[bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.

[Alex ter Weele <alex.ter.weele@gmail.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: 0001-gnu-agda-Compile-.agda-files.patch --]
[-- Type: text/x-patch, Size: 1976 bytes --]

From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
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


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0002-gnu-Add-emacs-agda2-mode.patch --]
[-- Type: text/x-patch, Size: 1600 bytes --]

From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001
From: Alex ter Weele <alex.ter.weele@gmail.com>
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