Remove agda libraries that are packaged by guix.

agda-stdlib: remove package
agda-categories: remove package
cubical: remove package

3 files changed, 0 insertions, 560 deletions

diff --git a/yellowsquid/build-system/agda.scm b/yellowsquid/build-system/agda.scm
deleted file mode 100644
index a4d01da..0000000
--- a/yellowsquid/build-system/agda.scm
+++ /dev/null
@@ -1,114 +0,0 @@
-(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))
-                #:allow-other-keys
-                #:rest arguments)
-  (define private-keywords
-    '(#:target #:agda #:inputs #:native-inputs))
-
-  (bag
-    (name name)
-    (system system)
-    (target target)
-    (build-inputs `(,@(if source
-                         `(("source" ,source))
-                         '())
-                    ,@native-inputs
-                    ,@(if target '() inputs)
-                    ("agda" ,agda)
-                    ,@(standard-packages)))
-    (host-inputs (if target inputs '()))
-    (outputs outputs)
-    (build agda-build)
-    (arguments (strip-keyword-arguments private-keywords arguments))))
-
-(define* (agda-build name inputs
-                     #:key
-                     guile source
-                     (everything "Everything.agda")
-                     (readme "README.agda")
-                     (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
-                            #:everything #$everything
-                            #:readme #$readme
-                            #: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
deleted file mode 100644
index d1d2ca5..0000000
--- a/yellowsquid/build/agda-build-system.scm
+++ /dev/null
@@ -1,280 +0,0 @@
-(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 "flags:~%")
-          (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?) _ ...) '())
-        (((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)
-        ((_) #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 everything #:allow-other-keys)
-  "Build a given Agda library."
-  (invoke "agda"
-          "--include-path=."
-          "--library-file=libraries"
-          everything))
-
-(define* (build-docs #:key outputs readme #:allow-other-keys)
-  "Build documentation for a given Agda library."
-  (let ((out (assoc-ref outputs "out")))
-    (invoke "agda"
-            "--include-path=."
-            "--library-file=libraries"
-            "--html"
-            (format #f
-                    "--html-dir=~a/share/doc/~a/html"
-                    out
-                    (strip-store-file-name out))
-            readme)))
-
-(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))))))
-
-  (let* ((my-agda-lib (find+parse-agda-lib))
-         (out (assoc-ref outputs "out"))
-         (name (or (agda-lib-name my-agda-lib) (strip-store-file-name out)))
-         (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
deleted file mode 100644
index fe16581..0000000
--- a/yellowsquid/packages/agda.scm
+++ /dev/null
@@ -1,166 +0,0 @@
-(define-module (yellowsquid packages agda)
-  #:use-module (gnu packages agda)
-  #:use-module (gnu packages haskell)
-  #:use-module (gnu packages haskell-xyz)
-  #:use-module (guix git-download)
-  #:use-module ((guix licenses) #:prefix license:)
-  #:use-module (guix packages)
-  #:use-module (yellowsquid build-system agda)
-  #:use-module (yellowsquid packages))
-
-(define-public agda-stdlib-1.7.2
-  (package
-    (name "agda-stdlib")
-    (version "1.7.2")
-    (home-page "https://github.com/agda/agda-stdlib")
-    (source (origin
-              (method git-fetch)
-              (uri (git-reference (url home-page)
-                                  (commit (string-append "v" version))))
-              (file-name (git-file-name name version))
-              (sha256
-               (base32
-                "065hf24xjpciwdrvk4isslgcgi01q0k93ql0y1sjqqvy5ryg5xmy"))))
-    (build-system agda-build-system)
-    (native-inputs (list ghc ghc-filemanip))
-    (arguments
-     '(#:phases
-       (modify-phases %standard-phases
-         (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"))
-
-             (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
-normalisation performance.")
-    (license license:expat)))
-
-(define-public agda-stdlib agda-stdlib-1.7.2)
-
-(define-public agda-categories
-  (package
-    (name "agda-categories")
-    (version "0.1.7.2")
-    (home-page "https://github.com/agda/agda-categories")
-    (source (origin
-              (method git-fetch)
-              (uri (git-reference (url home-page)
-                                  (commit (string-append "v" version))))
-              (file-name (git-file-name name version))
-              (sha256
-               (base32
-                "0xwgm2mfl2pxipsv31bin8p14y1yhd9n27lv3clvsxd4z9yc034m"))
-              (patches
-               (search-patches "agda-categories-everything.patch"))))
-    (build-system agda-build-system)
-    (inputs (list agda-stdlib-1.7.2))
-    (arguments
-     '(#:readme "Everything.agda"))
-    (synopsis "Categories library for Agda")
-    (description "A proof-relevant category theory library for Agda.  The
-library contains definitions for many important parts of category theory.
-A major goal is to make the category ready to be incorporated into the
-standard library.  Note that the library is currently pre-beta software, and
-backwards compatibility is not assured.")
-    (license license:expat)))
-
-(define-public cubical
-  (package
-    (name "cubical")
-    (version "0.5")
-    (home-page "https://github.com/agda/cubical")
-    (source (origin
-              (method git-fetch)
-              (uri (git-reference (url home-page)
-                                  (commit (string-append "v" version))))
-              (file-name (git-file-name name version))
-              (sha256
-               (base32
-                "0yfg7gr55n08ly1qgzpcp16s15k1abycppbcdi9lzg1hjryqxcg3"))))
-    (build-system agda-build-system)
-    (native-inputs (list ghc))
-    (arguments
-     '(#:phases
-       (modify-phases %standard-phases
-         (add-before 'build 'generate-everything
-           (lambda* (#:key outputs #:allow-other-keys)
-             (invoke "make" "gen-everythings"))))
-       #:everything "Cubical/README.agda"
-       #:readme "Cubical/README.agda"))
-    (synopsis "Standard library for Cubical Agda")
-    (description "A standard library for Cubical Agda. ")
-    (license license:expat)))