build-system: create agda-build-system

3 files changed, 486 insertions, 72 deletions

diff --git a/yellowsquid/build-system/agda.scm b/yellowsquid/build-system/agda.scm
new file mode 100644
index 0000000..d72bbcb
--- /dev/null
+++ b/yellowsquid/build-system/agda.scm
@@ -0,0 +1,109 @@
+(define-module (yellowsquid build-system agda)
+  #:use-module (guix build-system)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix gexp)
+  #:use-module (guix modules)
+  #:use-module (guix monads)
+  #:use-module (guix packages)
+  #:use-module (guix search-paths)
+  #:use-module (guix store)
+  #:use-module (guix utils)
+  #:export (default-agda
+            lower
+            agda-build
+            agda-build-system))
+
+(define %agda-build-system-modules
+  (source-module-closure
+   `((yellowsquid build agda-build-system)
+     ,@%gnu-build-system-modules)
+   #:select?
+   (lambda (name)
+     (or (guix-module-name? name)
+         (eq? (car name) 'yellowsquid)))))
+
+(define (default-agda)
+  "Return the default agda package."
+  ;; Do not use `@' to avoid introducing circular dependencies.
+  (let ((module (resolve-interface '(gnu packages agda))))
+    (module-ref module 'agda)))
+
+(define* (lower name
+                #:key source inputs native-inputs outputs system target
+                (agda (default-agda))
+                (agda-inputs '())
+                #:allow-other-keys
+                #:rest arguments)
+  (define private-keywords
+    '(#:target #:agda #:inputs #:native-inputs))
+
+  (bag
+    (name name)
+    (system system)
+    (host-inputs `(,@(if source
+                         `(("source" ,source))
+                         '())
+                   ,@inputs
+                   ,@(standard-packages)))
+    (build-inputs `(("agda" ,agda)
+                    ,@native-inputs))
+    (outputs outputs)
+    (build agda-build)
+    (arguments (strip-keyword-arguments private-keywords arguments))))
+
+(define* (agda-build name inputs
+                     #:key
+                     guile source
+                     (outputs '("out"))
+                     (search-paths '())
+                     (out-of-source? #t)
+                     (validate-runpath? #t)
+                     (patch-shebangs? #t)
+                     (strip-binaries? #t)
+                     (strip-flags ''("--strip-debug"))
+                     (strip-directories ''("lib" "lib64" "libexec" "bin" "sbin"))
+                     (phases '(@ (yellowsquid build agda-build-system)
+                                 %standard-phases))
+                     (system (%current-system))
+                     (target #f)
+                     (imported-modules %agda-build-system-modules)
+                     (modules '((guix build utils)
+                                (yellowsquid build agda-build-system))))
+  "Build SOURCE using AGDA, and with INPUTS."
+
+  (define builder
+    (with-imported-modules imported-modules
+      #~(begin
+          (use-modules #$@modules)
+          #$(with-build-variables inputs outputs
+              #~(agda-build #:source #+source
+                            #:system #$system
+                            #:outputs %outputs
+                            #:inputs %build-inputs
+                            #:search-paths
+                            '#$(sexp->gexp
+                                (map search-path-specification->sexp
+                                     search-paths))
+                            #:phases #$(if (pair? phases)
+                                           (sexp->gexp phases)
+                                           phases)
+                            #:out-of-source? #$out-of-source?
+                            #:validate-runpath? #$validate-runpath?
+                            #:patch-shebangs? #$patch-shebangs?
+                            #:strip-binaries? #$strip-binaries?
+                            #:strip-flags #$(sexp->gexp strip-flags)
+                            #:strip-directories
+                            #$(sexp->gexp strip-directories))))))
+
+  (mlet %store-monad ((guile (package->derivation (or guile (default-guile))
+                                                  system #:graft? #f)))
+    (gexp->derivation name builder
+                      #:system system
+                      #:target #f
+                      #:guile-for-build guile)))
+
+(define agda-build-system
+  (build-system
+    (name 'agda)
+    (description "Build system for Agda libraries.")
+    (lower lower)))
diff --git a/yellowsquid/build/agda-build-system.scm b/yellowsquid/build/agda-build-system.scm
new file mode 100644
index 0000000..bd4f9d5
--- /dev/null
+++ b/yellowsquid/build/agda-build-system.scm
@@ -0,0 +1,291 @@
+(define-module (yellowsquid build agda-build-system)
+  #:use-module ((guix build gnu-build-system) #:prefix gnu:)
+  #:use-module (guix build utils)
+  #:use-module (guix records)
+  #:use-module (ice-9 ftw)
+  #:use-module (ice-9 match)
+  #:use-module (ice-9 receive)
+  #:use-module (ice-9 textual-ports)
+  #:use-module (srfi srfi-1)
+  #:use-module (srfi srfi-26)
+  #:use-module (srfi srfi-41)
+  #:export (%standard-phases
+            agda-build))
+
+(define-record-type* <agda-lib>
+  agda-lib make-agda-lib
+  agda-lib?
+  (name agda-lib-name (default #f))
+  (depends agda-lib-depends (default '()))
+  (includes agda-lib-includes (default '()))
+  (flags agda-lib-flags (default '())))
+
+(define (serialize-agda-lib agda-lib)
+  (match-record agda-lib <agda-lib>
+    (name depends includes flags)
+    (call-with-output-string
+      (lambda (port)
+        (if name
+            (format port "name: ~a~%" name))
+        (unless (null? depends)
+          (format port "depend:~%")
+          (for-each (cut format port "  ~a~%" <>) depends))
+        (unless (null? includes)
+          (format port "include:~%")
+          (for-each (cut format port "  ~a~%" <>) includes))
+        (unless (null? flags)
+          (format port "flag:~%")
+          (for-each (cut format port "  ~a~%" <>) flags))))))
+
+(define (parse-agda-lib filename)
+  "Parse an agda-lib file."
+
+  (define (strip-comments line)
+    (define (helper chars)
+      (match chars
+        (() '())
+        ((#\- #\- (? char-whitespace?) rest ...) '())
+        (((and c (? char-whitespace?)) rest ...)
+         (let ((rec (helper rest)))
+           (if (null? rec)
+               '()
+               (cons c rec))))
+        ((c rest ...) (cons c (helper rest)))))
+    (list->string (helper (string->list line))))
+
+  (define (parse-line line)
+    "Parse a line into header and content components."
+    (cond
+     ((null? line) '())
+     ((char-whitespace? (string-ref line 0))
+      ;; indented lines are content
+      `((content ,(string-trim line))))
+     (else (match (string-split line #\:)
+             ((head rest)
+              (if (string-any char-set:whitespace (string-trim-right head))
+                  (throw 'agda-lib-parse 'invalid-head head)
+                  `((header ,(string-trim-right head))
+                    ,@(if (string-null? (string-trim rest))
+                          '()
+                          `((content ,(string-trim rest)))))))))))
+
+  (define (group-lines lines)
+    "Collect headers and contents into lists."
+    (match lines
+      (() '())
+      ((('header head) rest ...)
+       (receive (content rest)
+           (span (lambda (line) (eq? 'content (car line))) rest)
+         (cons (cons head (map cadr content))
+               (group-lines rest))))
+      (_ (throw 'agda-lib-parse 'invalid-lines lines))))
+
+  (define (parse-generic lines)
+    (group-lines
+     (append-map
+      (lambda (line) (parse-line (strip-comments line)))
+      lines)))
+
+  (define (check-fields! headers)
+    (define* (duplicates xs #:optional (= equal?))
+      (match xs
+        (() #f)
+        ((x) #f)
+        ((x y rest ...) (or (= x y) (duplicates (cons y rest) =)))))
+    (let* ((sorted (sort headers string<)))
+      (if (duplicates sorted)
+          (throw 'agda-lib-parse 'duplicate-headers headers))))
+
+  (define (parse-name content)
+    (match content
+      (((and name (? (compose not (cut string-any char-set:whitespace <>)))))
+       name)
+      (_ (throw 'agda-lib-parse 'invalid-name content))))
+
+  (define (parse-includes content)
+    (define (fixup acc)
+      (let ((fp (acc '())))
+        (if (null? fp)
+            '()
+            (list (list->string fp)))))
+
+    (define (helper acc chars)
+      (match chars
+        (() (fixup acc))
+        ((#\\ #\  rest ...) (helper (compose acc (cut cons #\  <>)) rest))
+        ((#\\ #\\ rest ...) (helper (compose acc (cut cons #\\ <>)) rest))
+        ((#\  rest ...) (append (fixup acc) (helper identity rest)))
+        ((c rest ...) (helper (compose acc (cut cons c <>)) rest))))
+
+    (append-map
+     (compose (cut helper identity <>) string->list)
+     content))
+
+  (define (parse-flags content)
+    (append-map
+     (lambda (content)
+       (filter
+        (compose not string-null?)
+        (string-split content char-set:whitespace)))
+     content))
+
+  (define (parse-depends content)
+    (append-map
+     (lambda (content)
+       (filter
+        (compose not string-null?)
+        (string-split content
+                      (char-set-union char-set:whitespace
+                                      (char-set #\,)))))
+     content))
+
+  (define (build-lib fields)
+    (match fields
+      (() (agda-lib))
+      ((("name" content ...) rest ...)
+       (agda-lib
+        (inherit (build-lib rest))
+        (name (parse-name content))))
+      ((("include" content ...) rest ...)
+       (agda-lib
+        (inherit (build-lib rest))
+        (includes (parse-includes content))))
+      ((("depend" content ...) rest ...)
+       (agda-lib
+        (inherit (build-lib rest))
+        (depends (parse-depends content))))
+      ((("flags" content ...) rest ...)
+       (agda-lib
+        (inherit (build-lib rest))
+        (flags (parse-flags content))))))
+
+  (define (file->line-stream filename)
+    (let ((p (open-input-file filename)))
+      (stream-let loop ((line (get-line p)))
+         (if (eof-object? line)
+             (begin (close-input-port p)
+                    stream-null)
+             (stream-cons line (loop (get-line p)))))))
+
+  (let* ((lines (stream->list (file->line-stream filename)))
+         (fields (parse-generic lines)))
+    (check-fields! (map car fields))
+    (build-lib fields)))
+
+(define (find+parse-agda-lib)
+  (match (scandir "." (cut string-suffix? ".agda-lib" <>))
+    ((original) (parse-agda-lib original))))
+
+(define* (generate-libraries #:key inputs #:allow-other-keys)
+  "Generate a libraries file for a given Agda library."
+  (let ((agda-lib (find+parse-agda-lib)))
+    (call-with-output-file "libraries"
+      (lambda (port)
+        (for-each
+         (lambda (lib)
+           (receive (name _)
+               (package-name->name+version lib)
+             (format port
+                     "~a~%"
+                     (search-input-file
+                      inputs
+                      (format #f "/share/agda/lib/~a.agda-lib" name)))))
+         (agda-lib-depends agda-lib))))))
+
+(define* (build #:key outputs #:allow-other-keys)
+  "Build a given Agda library."
+  (invoke "agda"
+          "--include-path=."
+          "--library-file=libraries"
+          "Everything.agda"))
+
+(define* (build-docs #:key outputs #:allow-other-keys)
+  "Build documentation for a given Agda library."
+  (let ((out (assoc-ref outputs "out"))
+        (readme (scandir "." (cut equal? "README.agda" <>))))
+    (invoke "agda"
+            "--include-path=."
+            "--library-file=libraries"
+            "--html"
+            (format #f
+                    "--html-dir=~a/share/doc/~a/html"
+                    out
+                    (strip-store-file-name out))
+            (match readme
+              ((filename) filename)
+              (_ "Everything.agda")))))
+
+(define* (install #:key inputs outputs #:allow-other-keys)
+  "Install a given Agda library."
+
+  ;;; Taken from (gnu build copy-build-system)
+  (define (install-file file target)
+    (let ((dest (string-append target
+                               (if (string-suffix? "/" target)
+                                   file
+                                   (string-append "/" file)))))
+      (format (current-output-port) "`~a' -> `~a'~%" file dest)
+      (mkdir-p (dirname dest))
+      (let ((stat (lstat file)))
+        (case (stat:type stat)
+          ((symlink)
+           (let ((target (readlink file)))
+             (symlink target dest)))
+          (else
+           (copy-file file dest))))))
+
+  (define (serialize-configuration config fields)
+    (apply string-append
+           (map (lambda (field)
+                  ((configuration-field-serializer field)
+                   (configuration-field-name field)
+                   ((configuration-field-getter field) config)))
+                fields)))
+
+  (let* ((my-agda-lib (find+parse-agda-lib))
+         (out (assoc-ref outputs "out"))
+         (name (agda-lib-name my-agda-lib))
+         (libdir (string-append out "/share/agda/lib/"))
+         (my-agda-lib* (agda-lib
+                        (inherit my-agda-lib)
+                        (includes
+                         (map (cut string-append name "/" <>)
+                              (agda-lib-includes my-agda-lib))))))
+    (mkdir-p libdir)
+    (receive (name* _)
+        (package-name->name+version name)
+      (call-with-output-file (string-append libdir name* ".agda-lib")
+        (cut display
+             (serialize-agda-lib my-agda-lib*)
+             <>)))
+    (receive (_ agda-ver)
+        (package-name->name+version
+         (strip-store-file-name (assoc-ref inputs "agda")))
+      (for-each
+       (lambda (src-dir dest-dir)
+         (for-each
+          (match-lambda
+            ((base extension)
+             (with-directory-excursion (string-append base src-dir)
+               (map
+                (cut install-file <> (string-append libdir base dest-dir))
+                (find-files "." extension)))))
+          `(("" "\\.agda")
+            (,(string-append "_build/" agda-ver "/agda/") "\\.agdai"))))
+       (agda-lib-includes my-agda-lib)
+       (agda-lib-includes my-agda-lib*)))))
+
+(define %standard-phases
+  (modify-phases gnu:%standard-phases
+    (delete 'bootstrap)
+    (delete 'configure)
+    (add-before 'build 'generate-libraries generate-libraries)
+    (replace 'build build)
+    (add-after 'build 'build-docs build-docs)
+    (delete 'check)
+    (replace 'install install)))
+
+(define* (agda-build #:key inputs (phases %standard-phases)
+                     #:allow-other-keys #:rest args)
+  "Build the given package, applying all of PHASES in order."
+  (apply gnu:gnu-build #:inputs inputs #:phases phases args))
diff --git a/yellowsquid/packages/agda.scm b/yellowsquid/packages/agda.scm
index c3c1f7d..7bba1bd 100644
--- a/yellowsquid/packages/agda.scm
+++ b/yellowsquid/packages/agda.scm
@@ -1,10 +1,11 @@
 (define-module (yellowsquid packages agda)
   #:use-module (gnu packages agda)
+  #:use-module (gnu packages haskell)
   #:use-module (gnu packages haskell-xyz)
-  #:use-module (guix build-system haskell)
   #:use-module (guix git-download)
   #:use-module ((guix licenses) #:prefix license:)
-  #:use-module (guix packages))
+  #:use-module (guix packages)
+  #:use-module (yellowsquid build-system agda))
 
 (define-public agda-stdlib
   (package
@@ -17,79 +18,92 @@
                                   (commit (string-append "v" version))))
               (file-name (git-file-name name version))
               (sha256
-               (base32 "0khl12jvknsvjsq3l5cbp2b5qlw983qbymi1dcgfz9z0b92si3r0"))))
-    (build-system haskell-build-system)
-    (native-inputs (list agda ghc-filemanip))
-    (outputs '("out" "doc"))
+               (base32
+                "0khl12jvknsvjsq3l5cbp2b5qlw983qbymi1dcgfz9z0b92si3r0"))))
+    (build-system agda-build-system)
+    (native-inputs (list ghc ghc-filemanip))
     (arguments
-     `(#:modules ((guix build haskell-build-system)
-                  (guix build utils)
-                  (ice-9 receive))
-       #:phases
+     '(#:phases
        (modify-phases %standard-phases
-         (add-after 'build 'generate-everything
-           (lambda* (#:key inputs #:allow-other-keys)
-             (invoke "dist/build/GenerateEverything/GenerateEverything")))
-         (add-after 'generate-everything 'compile-agda
-           (lambda* (#:key inputs #:allow-other-keys)
-             (invoke "agda" "-i." "-isrc" "Everything.agda")))
-         (add-after 'compile-agda 'build-doc
-           (lambda* (#:key inputs #:allow-other-keys)
-             (invoke "agda" "-i." "-isrc" "--html" "README.agda")))
-         (delete 'haddock)
-         (replace 'install
-           (lambda* (#:key inputs outputs #:allow-other-keys)
-             (define (install-file file target)
-               (let ((dest (string-append target
-                                          (if (string-suffix? "/" target)
-                                              file
-                                              (string-append "/" file)))))
-                 (format (current-output-port) "`~a' -> `~a'~%" file dest)
-                 (mkdir-p (dirname dest))
-                 (let ((stat (lstat file)))
-                   (case (stat:type stat)
-                     ((symlink)
-                      (let ((target (readlink file)))
-                        (symlink target dest)))
-                     (else
-                      (copy-file file dest))))))
+         (add-before 'build 'generate-everything
+           ;; taken from (gnu build haskell-build-system)
+           (lambda* (#:key outputs #:allow-other-keys)
+             (use-modules (srfi srfi-1))
+             (define %tmp-db-dir
+               (string-append (or (getenv "TMP") "/tmp")
+                              "/package.conf.d"))
 
-             (let ((lib (string-append (assoc-ref outputs "out")
-                                       "/share/agda/lib"))
-                   (doc (string-append (assoc-ref outputs "doc")
-                                       "/share/doc/agda-stdlib-1.7.1"))
-                   (agda (assoc-ref inputs "agda")))
-               (mkdir-p lib)
-               (mkdir-p doc)
-               (call-with-output-file
-                   (string-append lib "/standard-library.agda-lib")
-                 (lambda (port)
-                   (display "
-name: standard-library-1.7.1
-include: stdlib\n"
-                            port)))
-               (copy-recursively "html" (string-append doc "/"))
-               (with-directory-excursion "src"
-                 (map (lambda (file)
-                        (install-file file (string-append lib "/stdlib/")))
-                      (find-files "." "\\.agda")))
-               (receive (_ agda-ver)
-                   (package-name->name+version (strip-store-file-name agda))
-                 (with-directory-excursion
-                     (string-append "_build/" agda-ver "/agda/src")
-                   (map
-                    (lambda (file)
-                      (install-file
-                       file
-                       (string-append lib
-                                      "/_build/"
-                                      agda-ver
-                                      "/agda/stdlib/")))
-                    (find-files "." "\\.agdai")))))))
-         (delete 'register))))
+             (define (run-setuphs command params)
+               (let ((setup-file (cond
+                                  ((file-exists? "Setup.hs")
+                                   "Setup.hs")
+                                  ((file-exists? "Setup.lhs")
+                                   "Setup.lhs")
+                                  (else
+                                   #f)))
+                     (pkgdb (string-append "-package-db=" %tmp-db-dir)))
+                 (if setup-file
+                     (begin
+                       (format #t
+                               "running \"runhaskell Setup.hs\" with command \
+~s and parameters ~s~%"
+                               command params)
+                       (apply invoke
+                              "runhaskell"
+                              pkgdb
+                              setup-file
+                              command
+                              params))
+                     (error "no Setup.hs nor Setup.lhs found"))))
+
+             #;(run-setuphs "run" '("GenerateEverything"))
+             (let* ((out (assoc-ref outputs "out"))
+                    (name-version (strip-store-file-name out))
+                    (ghc-path (getenv "GHC_PACKAGE_PATH"))
+                    (conf-dirs (search-path-as-string->list
+                                (getenv "GHC_PACKAGE_PATH")))
+                    (conf-files (append-map
+                                 (lambda (file) (find-files file "\\.conf$"))
+                                 conf-dirs))
+                    (params `(,(string-append "--prefix=" out)
+                              ,(string-append "--libdir=" out "/lib")
+                              ,(string-append "--docdir="
+                                              out
+                                              "/share/doc/"
+                                              name-version)
+                              "--libsubdir=$compiler/$pkg-$version"
+                              ,(string-append "--package-db=" %tmp-db-dir)
+                              "--global"
+                              "--enable-shared"
+                              "--enable-executable-dynamic"
+                              "--ghc-option=-fPIC"
+                              ,(string-append
+                                "--ghc-option=-optl=-Wl,-rpath="
+                                out
+                                "/lib/$compiler/$pkg-$version"))))
+               (mkdir-p %tmp-db-dir)
+               (for-each
+                (lambda (file)
+                  (let ((dest (string-append %tmp-db-dir
+                                             "/"
+                                             (basename file))))
+                    (unless (file-exists? dest)
+                      (copy-file file dest))))
+                conf-files)
+               (invoke "ghc-pkg"
+                       (string-append "--package-db=" %tmp-db-dir)
+                       "recache")
+               (unsetenv "GHC_PACKAGE_PATH")
+               (when (file-exists? "configure")
+                 (setenv "CONFIG_SHELL" "sh"))
+               (run-setuphs "configure" params)
+               (setenv "GHC_PACKAGE_PATH" ghc-path)
+               (run-setuphs "build" '())
+               (invoke
+                "dist/build/GenerateEverything/GenerateEverything")))))))
     (synopsis "Standard library for Agda")
-    (description "The Agda standard library aims to contain all the tools needed
-to write both programs and proofs easily.  Whilst the library tries to write
-efficient code, ease of proof is prioritised over type-checking and
+    (description "The Agda standard library aims to contain all the tools
+needed to write both programs and proofs easily.  Whilst the library tries to
+write efficient code, ease of proof is prioritised over type-checking and
 normalisation performance.")
     (license license:expat)))