diff options
| -rw-r--r-- | Makefile.am | 2 | ||||
| -rw-r--r-- | doc/guix.texi | 21 | ||||
| -rw-r--r-- | guix/build-system/agda.scm | 123 | ||||
| -rw-r--r-- | guix/build/agda-build-system.scm | 128 |
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)) |