Toggle diff (281 lines)
diff --git a/Makefile.am b/Makefile.am
index a763a7e305..9d137cfbb3 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -140,6 +140,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 \
@@ -195,6 +196,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 46e7fd3908..01cd199f0a 100644
--- a/doc/guix.texi
+++ b/doc/guix.texi
@@ -8885,6 +8885,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..cf96ffaa68
--- /dev/null
+++ b/guix/build-system/agda.scm
@@ -0,0 +1,105 @@
+(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..1d7e80d61b
--- /dev/null
+++ b/guix/build/agda-build-system.scm
@@ -0,0 +1,110 @@
+(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))
--
2.39.2
