futurile/guix-play
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

build-system: New agda-build-system.

Browse Source 
* 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.
This commit is contained in:
Josselin Poiret 2023-04-30 12:01:43 +02:00
parent 0769a9b3c5
commit 80d1228321
No known key found for this signature in database
GPG Key ID: 505E40B916171A8A
4 changed files with 274 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile.am
View File

@ -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 \

21
doc/guix.texi
View File

@ -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

123
guix/build-system/agda.scm Normal file
View File

@ -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)))

128
guix/build/agda-build-system.scm Normal file
View File

@ -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))