build-system: New agda-build-system.

* guix/build-system/agda.scm: New file.
* guix/build/agda-build-system.scm: New file.
* Makefile.am (MODULES): Register them.
* doc/guix.texi (Build Systems): Add documentation for agda-build-system.

4 files changed, 274 insertions, 0 deletions

diff --git a/Makefile.am b/Makefile.am
index 685e2b2f86..ab901df757 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -141,6 +141,7 @@ MODULES =					\
   guix/platforms/riscv.scm                      \
   guix/platforms/x86.scm                        \
   guix/build-system.scm				\
+  guix/build-system/agda.scm                    \
   guix/build-system/android-ndk.scm		\
   guix/build-system/ant.scm			\
   guix/build-system/cargo.scm			\
@@ -196,6 +197,7 @@ MODULES =					\
   guix/diagnostics.scm				\
   guix/ui.scm					\
   guix/status.scm				\
+  guix/build/agda-build-system.scm              \
   guix/build/android-ndk-build-system.scm	\
   guix/build/ant-build-system.scm		\
   guix/build/download.scm			\
diff --git a/doc/guix.texi b/doc/guix.texi
index db37676e12..c9b3fb642c 100644
--- a/doc/guix.texi
+++ b/doc/guix.texi
@@ -8963,6 +8963,27 @@ of @code{gnu-build-system}, and differ mainly in the set of inputs
 implicitly added to the build process, and in the list of phases
 executed.  Some of these build systems are listed below.
 
+@defvar agda-build-system
+This variable is exported by @code{(guix build-system agda)}.  It
+implements a build procedure for Agda libraries.
+
+It adds @code{agda} to the set of inputs.  A different Agda can be
+specified with the @code{#:agda} key.
+
+The @code{#:plan} key is a list of cons cells @code{(@var{regexp}
+. @var{parameters})}, where @var{regexp} is a regexp that should match
+the @code{.agda} files to build, and @var{parameters} is an optional
+list of parameters that will be passed to @code{agda} when type-checking
+it.
+
+When the library uses Haskell to generate a file containing all imports,
+the convenience @code{#:gnu-and-haskell?} can be set to @code{#t} to add
+@code{ghc} and the standard inputs of @code{gnu-build-system} to the
+input list.  You will still need to manually add a phase or tweak the
+@code{'build} phase, as in the definition of @code{agda-stdlib}.
+
+@end defvar
+
 @defvar ant-build-system
 This variable is exported by @code{(guix build-system ant)}.  It
 implements the build procedure for Java packages that can be built with
diff --git a/guix/build-system/agda.scm b/guix/build-system/agda.scm
new file mode 100644
index 0000000000..64983dff60
--- /dev/null
+++ b/guix/build-system/agda.scm
@@ -0,0 +1,123 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2023 Josselin Poiret <dev@jpoiret.xyz>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (guix build-system agda)
+  #:use-module (guix build-system)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix build-system haskell)
+  #:use-module (guix gexp)
+  #:use-module (guix monads)
+  #:use-module (guix packages)
+  #:use-module (guix search-paths)
+  #:use-module (guix store)
+  #:use-module (guix utils)
+  #:export (default-agda
+
+            %agda-build-system-modules
+            agda-build-system))
+
+(define (default-agda)
+  ;; Lazily resolve the binding to avoid a circular dependency.
+  (let ((agda (resolve-interface '(gnu packages agda))))
+    (module-ref agda 'agda)))
+
+(define %agda-build-system-modules
+  `((guix build agda-build-system)
+    ,@%gnu-build-system-modules))
+
+(define %default-modules
+  '((guix build agda-build-system)
+    (guix build utils)))
+
+(define* (lower name
+                #:key source inputs native-inputs outputs system target
+                (agda (default-agda))
+                gnu-and-haskell?
+                #:allow-other-keys
+                #:rest arguments)
+  "Return a bag for NAME."
+  (define private-keywords
+    '(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs))
+
+  ;; TODO: cross-compilation support
+  (and (not target)
+       (bag
+         (name name)
+         (system system)
+         (host-inputs `(,@(if source
+                              `(("source" ,source))
+                              '())
+                        ,@inputs))
+         (build-inputs `(("agda" ,agda)
+                         ,@(if gnu-and-haskell?
+                               (cons*
+                                (list "ghc" (default-haskell))
+                                (standard-packages))
+                               '())
+                         ,(assoc "locales" (standard-packages))
+                         ,@native-inputs))
+         (outputs outputs)
+         (build agda-build)
+         (arguments (strip-keyword-arguments private-keywords arguments)))))
+
+(define* (agda-build name inputs
+                     #:key
+                     source
+                     (phases '%standard-phases)
+                     (outputs '("out"))
+                     (search-paths '())
+                     (unpack-path "")
+                     (build-flags ''())
+                     (tests? #t)
+                     (system (%current-system))
+                     (guile #f)
+                     plan
+                     (extra-files '("^\\./.*\\.agda-lib$"))
+                     (imported-modules %agda-build-system-modules)
+                     (modules %default-modules))
+  (define builder
+    (with-imported-modules imported-modules
+      #~(begin
+          (use-modules #$@(sexp->gexp modules))
+          (agda-build #:name #$name
+                      #:source #+source
+                      #:system #$system
+                      #:phases #$phases
+                      #:outputs #$(outputs->gexp outputs)
+                      #:search-paths '#$(sexp->gexp
+                                         (map search-path-specification->sexp
+                                              search-paths))
+                      #:unpack-path #$unpack-path
+                      #:build-flags #$build-flags
+                      #:tests? #$tests?
+                      #:inputs #$(input-tuples->gexp inputs)
+                      #:plan '#$plan
+                      #:extra-files '#$extra-files))))
+
+  (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+                                                  system #:graft? #f)))
+    (gexp->derivation name builder
+                      #:system system
+                      #:guile-for-build guile)))
+
+(define agda-build-system
+  (build-system
+    (name 'agda)
+    (description
+     "Build system for Agda libraries")
+    (lower lower)))
diff --git a/guix/build/agda-build-system.scm b/guix/build/agda-build-system.scm
new file mode 100644
index 0000000000..49836d5dea
--- /dev/null
+++ b/guix/build/agda-build-system.scm
@@ -0,0 +1,128 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2023 Josselin Poiret <dev@jpoiret.xyz>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (guix build agda-build-system)
+  #:use-module ((guix build gnu-build-system) #:prefix gnu:)
+  #:use-module (guix build utils)
+  #:use-module (srfi srfi-26)
+  #:use-module (srfi srfi-34)
+  #:use-module (srfi srfi-35)
+  #:use-module (ice-9 ftw)
+  #:use-module (ice-9 match)
+  #:export (%standard-phases
+            agda-build))
+
+(define* (set-locpath #:key inputs native-inputs #:allow-other-keys)
+  (let ((locales (assoc-ref (or native-inputs inputs) "locales")))
+    (setenv "GUIX_LOCPATH" (string-append locales "/lib/locale"))))
+
+(define %agda-possible-extensions
+  (cons
+   ".agda"
+   (map (cute string-append ".lagda" <>)
+        '(""
+          ".md"
+          ".org"
+          ".rst"
+          ".tex"))))
+
+(define (pattern-predicate pattern)
+  (define compiled-rx (make-regexp pattern))
+  (lambda (file stat)
+    (regexp-exec compiled-rx file)))
+
+(define* (build #:key plan #:allow-other-keys)
+  (for-each
+   (match-lambda
+     ((pattern . options)
+      (for-each
+       (lambda (file)
+         (apply invoke (cons* "agda" file options)))
+       (let ((files (find-files "." (pattern-predicate pattern))))
+         (if (null? files)
+             (raise
+              (make-compound-condition
+               (condition
+                (&message
+                 (message (format #f "Plan pattern `~a' did not match any files"
+                                  pattern))))
+               (condition
+                (&error))))
+             files))))
+     (x
+      (raise
+       (make-compound-condition
+        (condition
+         (&message
+          (message (format #f "Malformed plan element `~a'" x))))
+        (condition
+         (&error))))))
+   plan))
+
+(define* (install #:key outputs name extra-files #:allow-other-keys)
+  (define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name))
+  (define agda-version
+    (car (scandir "./_build/"
+                  (lambda (entry)
+                    (not (member entry '("." "..")))))))
+  (define agdai-files
+    (with-directory-excursion
+        (string-join (list "." "_build" agda-version "agda") "/")
+      (find-files ".")))
+  (define (install-source agdai)
+    (define dir (dirname agdai))
+    ;; Drop .agdai
+    (define no-ext (string-drop-right agdai 6))
+    (define source
+      (match (filter file-exists? (map (cute string-append no-ext <>)
+                                       %agda-possible-extensions))
+        ((single) single)
+        (res (raise
+              (make-compound-condition
+               (condition
+                (&message
+                 (message
+                  (format #f
+                          "Cannot find unique source file for agdai file `~a`, got `~a`"
+                          agdai res))))
+               (condition
+                (&error)))))))
+    (install-file source (string-append libdir "/" dir)))
+  (for-each install-source agdai-files)
+  (copy-recursively "_build" (string-append libdir "/_build"))
+  (for-each
+   (lambda (pattern)
+     (for-each
+      (lambda (file)
+        (install-file file libdir))
+      (find-files "." (pattern-predicate pattern))))
+   extra-files))
+
+(define %standard-phases
+  (modify-phases gnu:%standard-phases
+    (add-before 'install-locale 'set-locpath set-locpath)
+    (delete 'bootstrap)
+    (delete 'configure)
+    (replace 'build build)
+    (delete 'check) ;; No universal checker
+    (replace 'install install)))
+
+(define* (agda-build #:key inputs (phases %standard-phases)
+                     #:allow-other-keys #:rest args)
+  "Build the given Agda package, applying all of PHASES in order."
+  (apply gnu:gnu-build #:inputs inputs #:phases phases args))