diff options
Diffstat (limited to 'yellowsquid')
| -rw-r--r-- | yellowsquid/build-system/agda.scm | 109 | ||||
| -rw-r--r-- | yellowsquid/build/agda-build-system.scm | 291 | ||||
| -rw-r--r-- | yellowsquid/packages/agda.scm | 158 |
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))) |