diff options
author | Josselin Poiret <dev@jpoiret.xyz> | 2023-04-30 12:01:43 +0200 |
---|---|---|
committer | Josselin Poiret <dev@jpoiret.xyz> | 2023-06-04 10:59:34 +0200 |
commit | 80d122832135c4b7f1a35d22ae746cc6374a83f5 (patch) | |
tree | 4a9b112dbac908ffb50d5cdce17d9a8a2644eb03 /guix/build | |
parent | 0769a9b3c580df7d31db05e439d33e76d5db17e2 (diff) | |
download | guix-patches-80d122832135c4b7f1a35d22ae746cc6374a83f5.tar guix-patches-80d122832135c4b7f1a35d22ae746cc6374a83f5.tar.gz |
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.
Diffstat (limited to 'guix/build')
-rw-r--r-- | guix/build/agda-build-system.scm | 128 |
1 files changed, 128 insertions, 0 deletions
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)) |