unofficial mirror of bug-guix@gnu.org 
 help / color / mirror / code / Atom feed
blob 64983dff603e69ba72cfb402dba4144751ce4f86 4589 bytes (raw)
name: guix/build-system/agda.scm 	 # note: path name is non-authoritative(*)

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
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)))

debug log:

solving 64983dff60 ...
found 64983dff60 in https://git.savannah.gnu.org/cgit/guix.git

(*) Git path names are given by the tree(s) the blob belongs to.
    Blobs themselves have no identifier aside from the hash of its contents.^

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).