Marius Bakke <mbakke@fastmail.com> writes:

> Alex ter Weele <alex.ter.weele@gmail.com> writes:
>
>> 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.
>
> [...]
>
>> +    (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 <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.
>
> 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!