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

[Alex ter Weele]

Marius Bakke <address@hidden> writes:

> Alex ter Weele <address@hidden> writes:
>
>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001
>> From: Alex ter Weele <address@hidden>
>> 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 <address@hidden>
>> 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!


>From 51ad1e736760fb083fd04d933f9aaf6658b4b7fe Mon Sep 17 00:00:00 2001
From: Alex ter Weele <address@hidden>
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

>From b57cfb8766e85a4c2c8491415f2bf0d9357bcca2 Mon Sep 17 00:00:00 2001
From: Alex ter Weele <address@hidden>
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