Commit | Line | Data |
---|---|---|
f61682e7 AW |
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com> | |
787231e9 | 3 | ;;; Copyright © 2018 Ricardo Wurmus <rekado@elephly.net> |
58352f26 | 4 | ;;; Copyright © 2018 Alex Vong <alexvong1995@gmail.com> |
2c67e1cf | 5 | ;;; Copyright © 2018, 2022 Tobias Geerinckx-Rice <me@tobias.gr> |
276f598a | 6 | ;;; Copyright © 2018 John Soo <jsoo1@asu.edu> |
48752f27 | 7 | ;;; Copyright © 2019 Ludovic Courtès <ludo@gnu.org> |
f61682e7 AW |
8 | ;;; |
9 | ;;; This file is part of GNU Guix. | |
10 | ;;; | |
11 | ;;; GNU Guix is free software; you can redistribute it and/or modify it | |
12 | ;;; under the terms of the GNU General Public License as published by | |
13 | ;;; the Free Software Foundation; either version 3 of the License, or (at | |
14 | ;;; your option) any later version. | |
15 | ;;; | |
16 | ;;; GNU Guix is distributed in the hope that it will be useful, but | |
17 | ;;; WITHOUT ANY WARRANTY; without even the implied warranty of | |
18 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
19 | ;;; GNU General Public License for more details. | |
20 | ;;; | |
21 | ;;; You should have received a copy of the GNU General Public License | |
22 | ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. | |
23 | ||
24 | (define-module (gnu packages agda) | |
f61682e7 AW |
25 | #:use-module (gnu packages haskell-check) |
26 | #:use-module (gnu packages haskell-web) | |
dddbc90c | 27 | #:use-module (gnu packages haskell-xyz) |
1237653a | 28 | #:use-module (guix build-system emacs) |
276f598a | 29 | #:use-module (guix build-system gnu) |
f61682e7 AW |
30 | #:use-module (guix build-system haskell) |
31 | #:use-module (guix build-system trivial) | |
2e0d02eb | 32 | #:use-module (guix gexp) |
f61682e7 | 33 | #:use-module (guix download) |
48752f27 | 34 | #:use-module (guix git-download) |
f61682e7 AW |
35 | #:use-module ((guix licenses) #:prefix license:) |
36 | #:use-module (guix packages)) | |
37 | ||
38 | (define-public agda | |
39 | (package | |
40 | (name "agda") | |
2c67e1cf | 41 | (version "2.6.2.2") |
f61682e7 AW |
42 | (source |
43 | (origin | |
44 | (method url-fetch) | |
45 | (uri (string-append | |
46 | "https://hackage.haskell.org/package/Agda/Agda-" | |
47 | version ".tar.gz")) | |
48 | (sha256 | |
2c67e1cf | 49 | (base32 "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5")))) |
f61682e7 AW |
50 | (build-system haskell-build-system) |
51 | (inputs | |
8394619b LC |
52 | (list ghc-aeson |
53 | ghc-alex | |
54 | ghc-async | |
55 | ghc-blaze-html | |
56 | ghc-boxes | |
57 | ghc-case-insensitive | |
58 | ghc-data-hash | |
59 | ghc-edit-distance | |
60 | ghc-equivalence | |
61 | ghc-gitrev | |
62 | ghc-happy | |
63 | ghc-hashable | |
64 | ghc-hashtables | |
65 | ghc-monad-control | |
66 | ghc-murmur-hash | |
67 | ghc-parallel | |
68 | ghc-regex-tdfa | |
69 | ghc-split | |
70 | ghc-strict | |
71 | ghc-unordered-containers | |
72 | ghc-uri-encode | |
73 | ghc-zlib)) | |
253340dc | 74 | (arguments |
914d2c21 TGR |
75 | (list #:modules `((guix build haskell-build-system) |
76 | (guix build utils) | |
77 | (srfi srfi-26) | |
78 | (ice-9 match)) | |
79 | #:phases | |
80 | #~(modify-phases %standard-phases | |
81 | ;; This allows us to call the 'agda' binary before installing. | |
82 | (add-after 'unpack 'set-ld-library-path | |
83 | (lambda _ | |
84 | (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build")))) | |
85 | (add-after 'compile 'agda-compile | |
86 | (lambda* (#:key outputs #:allow-other-keys) | |
87 | (let ((agda-compiler (string-append #$output "/bin/agda"))) | |
88 | (for-each (cut invoke agda-compiler <>) | |
89 | (find-files (string-append #$output "/share") | |
90 | "\\.agda$")))))))) | |
0d2753cc | 91 | (home-page "https://wiki.portal.chalmers.se/agda/") |
f61682e7 AW |
92 | (synopsis |
93 | "Dependently typed functional programming language and proof assistant") | |
94 | (description | |
95 | "Agda is a dependently typed functional programming language: it has | |
96 | inductive families, which are similar to Haskell's GADTs, but they can be | |
97 | indexed by values and not just types. It also has parameterised modules, | |
98 | mixfix operators, Unicode characters, and an interactive Emacs interface (the | |
99 | type checker can assist in the development of your code). Agda is also a | |
100 | proof assistant: it is an interactive system for writing and checking proofs. | |
101 | Agda is based on intuitionistic type theory, a foundational system for | |
102 | constructive mathematics developed by the Swedish logician Per Martin-Löf. It | |
103 | has many similarities with other proof assistants based on dependent types, | |
104 | such as Coq, Epigram and NuPRL.") | |
105 | ;; Agda is distributed under the MIT license, and a couple of | |
106 | ;; source files are BSD-3. See LICENSE for details. | |
107 | (license (list license:expat license:bsd-3)))) | |
1237653a AW |
108 | |
109 | (define-public emacs-agda2-mode | |
110 | (package | |
111 | (inherit agda) | |
112 | (name "emacs-agda2-mode") | |
113 | (build-system emacs-build-system) | |
114 | (inputs '()) | |
115 | (arguments | |
116 | `(#:phases | |
117 | (modify-phases %standard-phases | |
118 | (add-after 'unpack 'enter-elisp-dir | |
119 | (lambda _ (chdir "src/data/emacs-mode") #t))))) | |
120 | (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html") | |
121 | (synopsis "Emacs mode for Agda") | |
122 | (description "This Emacs mode enables interactive development with | |
123 | Agda. It also aids the input of Unicode characters."))) | |
276f598a JS |
124 | |
125 | (define-public agda-ial | |
126 | (package | |
127 | (name "agda-ial") | |
128 | (version "1.5.0") | |
48752f27 LC |
129 | (home-page "https://github.com/cedille/ial") |
130 | (source (origin | |
131 | (method git-fetch) | |
132 | (uri (git-reference (url home-page) | |
133 | (commit (string-append "v" version)))) | |
134 | (file-name (git-file-name name version)) | |
135 | (sha256 | |
136 | (base32 | |
137 | "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g")))) | |
276f598a JS |
138 | (build-system gnu-build-system) |
139 | (inputs | |
8394619b | 140 | (list agda)) |
276f598a JS |
141 | (arguments |
142 | `(#:parallel-build? #f | |
143 | #:phases | |
144 | (modify-phases %standard-phases | |
145 | (delete 'configure) | |
146 | (add-before 'build 'patch-dependencies | |
147 | (lambda _ (patch-shebang "find-deps.sh") #t)) | |
148 | (delete 'check) | |
149 | (replace 'install | |
150 | (lambda* (#:key outputs #:allow-other-keys) | |
48752f27 LC |
151 | (let* ((out (assoc-ref outputs "out")) |
152 | (include (string-append out "/include/agda/ial"))) | |
153 | (for-each (lambda (file) | |
154 | (make-file-writable file) | |
155 | (install-file file include)) | |
83ac4c09 | 156 | (find-files "." "\\.agdai?(-lib)?$")) |
48752f27 LC |
157 | #t)))))) |
158 | (synopsis "The Iowa Agda Library") | |
276f598a JS |
159 | (description |
160 | "The goal is to provide a concrete library focused on verification | |
161 | examples, as opposed to mathematics. The library has a good number | |
162 | of theorems for booleans, natural numbers, and lists. It also has | |
163 | trees, tries, vectors, and rudimentary IO. A number of good ideas | |
164 | come from Agda's standard library.") | |
165 | (license license:expat))) |