projects/guix·blob kernel-updates · refs

323 lines · 12.6 KiB

1;;; GNU Guix --- Functional package management for GNU
2;;; Copyright © 2018 Alex ter Weele <[email protected]>
3;;; Copyright © 2018 Ricardo Wurmus <[email protected]>
4;;; Copyright © 2018 Alex Vong <[email protected]>
5;;; Copyright © 2018, 2022 Tobias Geerinckx-Rice <[email protected]>
6;;; Copyright © 2018 John Soo <[email protected]>
7;;; Copyright © 2019 Ludovic Courtès <[email protected]>
8;;; Copyright © 2023 Josselin Poiret <[email protected]>
9;;;
10;;; This file is part of GNU Guix.
11;;;
12;;; GNU Guix is free software; you can redistribute it and/or modify it
13;;; under the terms of the GNU General Public License as published by
14;;; the Free Software Foundation; either version 3 of the License, or (at
15;;; your option) any later version.
16;;;
17;;; GNU Guix is distributed in the hope that it will be useful, but
18;;; WITHOUT ANY WARRANTY; without even the implied warranty of
19;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
20;;; GNU General Public License for more details.
21;;;
22;;; You should have received a copy of the GNU General Public License
23;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
24
25(define-module (gnu packages agda)
26 #:use-module (gnu packages)
27 #:use-module (gnu packages haskell-check)
28 #:use-module (gnu packages haskell-web)
29 #:use-module (gnu packages haskell-xyz)
30 #:use-module (gnu packages imagemagick)
31 #:use-module (gnu packages python)
32 #:use-module (gnu packages sphinx)
33 #:use-module (gnu packages texinfo)
34 #:use-module (guix build-system agda)
35 #:use-module (guix build-system emacs)
36 #:use-module (guix build-system gnu)
37 #:use-module (guix build-system haskell)
38 #:use-module (guix gexp)
39 #:use-module (guix download)
40 #:use-module (guix git-download)
41 #:use-module ((guix licenses) #:prefix license:)
42 #:use-module (guix packages))
43
44(define-public agda
45 (package
46 (name "agda")
47 (version "2.7.0.1")
48 (source
49 (origin
50 (method git-fetch)
51 (uri (git-reference
52 (url "https://github.com/agda/agda.git")
53 (commit (string-append "v" version))))
54 (file-name (git-file-name name version))
55 (sha256
56 (base32 "1dh9fi8lwjv9rk6zik2bwjgqln0f0d36m3hm9m3zmmk4fby4rsi2"))
57 (patches (search-patches "agda-libdirs-env-variable.patch"
58 "agda-use-sphinx-5.patch"))))
59 (build-system haskell-build-system)
60 (inputs
61 (list ghc-aeson
62 ghc-alex
63 ghc-ansi-terminal
64 ghc-async
65 ghc-blaze-html
66 ghc-boxes
67 ghc-case-insensitive
68 ghc-data-hash
69 ghc-edit-distance
70 ghc-equivalence
71 ghc-gitrev
72 ghc-happy
73 ghc-hashable
74 ghc-hashtables
75 ghc-monad-control
76 ghc-murmur-hash
77 ghc-parallel
78 ghc-peano
79 ghc-pqueue
80 ghc-regex-tdfa
81 ghc-split
82 ghc-strict
83 ghc-text-icu
84 ghc-unordered-containers
85 ghc-uri-encode
86 ghc-vector-hashtables
87 ghc-zlib))
88 (native-inputs
89 (list python
90 python-sphinx
91 python-sphinx-rtd-theme
92 texinfo
93 imagemagick))
94 (arguments
95 (list #:modules `((guix build haskell-build-system)
96 (guix build utils)
97 (srfi srfi-26)
98 (ice-9 match))
99 #:configure-flags #~(list "-foptimise-heavily" "-fenable-cluster-counting")
100 #:phases
101 #~(modify-phases %standard-phases
102 ;; This allows us to call the 'agda' binary before installing.
103 (add-after 'unpack 'set-ld-library-path
104 (lambda _
105 (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))))
106 (add-after 'build 'agda-compile
107 (lambda* (#:key outputs #:allow-other-keys)
108 (let ((agda-compiler (string-append #$output "/bin/agda")))
109 (for-each (cut invoke agda-compiler <>)
110 (find-files (string-append #$output "/share")
111 "\\.agda$")))))
112 (add-after 'agda-compile 'install-info
113 (lambda _
114 (with-directory-excursion "doc/user-manual"
115 (invoke "sphinx-build" "-b" "texinfo"
116 "." "_build_texinfo")
117 (with-directory-excursion "_build_texinfo"
118 (setenv "infodir" (string-append #$output
119 "/share/info"))
120 (invoke "make" "install-info"))))))))
121 (search-paths
122 (list (search-path-specification
123 (variable "AGDA_LIBDIRS")
124 (files (list "lib/agda")))))
125 (native-search-paths
126 search-paths)
127 (home-page "https://wiki.portal.chalmers.se/agda/")
128 (synopsis
129 "Dependently typed functional programming language and proof assistant")
130 (description
131 "Agda is a dependently typed functional programming language: it has
132inductive families, which are similar to Haskell's GADTs, but they can be
133indexed by values and not just types. It also has parameterised modules,
134mixfix operators, Unicode characters, and an interactive Emacs interface (the
135type checker can assist in the development of your code). Agda is also a
136proof assistant: it is an interactive system for writing and checking proofs.
137Agda is based on intuitionistic type theory, a foundational system for
138constructive mathematics developed by the Swedish logician Per Martin-Löf. It
139has many similarities with other proof assistants based on dependent types,
140such as Coq, Epigram and NuPRL.")
141 ;; Agda is distributed under the MIT license, and a couple of
142 ;; source files are BSD-3. See LICENSE for details.
143 (license (list license:expat license:bsd-3))))
144
145(define-public emacs-agda2-mode
146 (package
147 (name "emacs-agda2-mode")
148 (version (package-version agda))
149 (source (package-source agda))
150 (build-system emacs-build-system)
151 (arguments
152 (list
153 #:lisp-directory "src/data/emacs-mode"))
154 (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html")
155 (synopsis "Emacs mode for Agda")
156 (description "This Emacs mode enables interactive development with
157Agda. It also aids the input of Unicode characters.")
158 (license (package-license agda))))
159
160(define-public agda-ial
161 (let ((revision "1")
162 ;; There hasn't been a release in a long time, and the last one
163 ;; doesn't build with Agda 2.6.
164 (commit "ded30c410d5d40142249686572aa1acd1b2f8cc7"))
165 (package
166 (name "agda-ial")
167 (version (git-version "1.5.0" revision commit))
168 (source (origin
169 (method git-fetch)
170 (uri (git-reference (url "https://github.com/cedille/ial")
171 (commit commit)))
172 (file-name (git-file-name name version))
173 (sha256
174 (base32
175 "0xn6zvp1wnm0i84pz1rfbzfmayd15ch4i5s11ycd88d22pxd55dc"))))
176 (build-system agda-build-system)
177 (arguments
178 (list
179 #:gnu-and-haskell? #t
180 #:phases
181 #~(modify-phases %standard-phases
182 (add-before 'build 'patch-dependencies
183 (lambda _ (patch-shebang "find-deps.sh")))
184 (replace 'build
185 (lambda _
186 (invoke "make"))))))
187 (home-page "https://github.com/cedille/ial")
188 (synopsis "The Iowa Agda Library")
189 (description
190 "The goal is to provide a concrete library focused on verification
191examples, as opposed to mathematics. The library has a good number
192of theorems for booleans, natural numbers, and lists. It also has
193trees, tries, vectors, and rudimentary IO. A number of good ideas
194come from Agda's standard library.")
195 (license license:expat))))
196
197(define-public agda-stdlib
198 (package
199 (name "agda-stdlib")
200 (version "2.3")
201 (source (origin
202 (method git-fetch)
203 (uri (git-reference
204 (url "https://github.com/agda/agda-stdlib")
205 (commit (string-append "v" version))))
206 (file-name (git-file-name name version))
207 (sha256
208 (base32
209 "17w5vfn5pb2cgfs22zph3jfqnki52ja8y4zwyqj24zwf9rxairr4"))))
210 (build-system agda-build-system)
211 (arguments
212 (list
213 #:plan '(("^\\./doc/README.agda$" "-idoc/"))
214 #:gnu-and-haskell? #t
215 #:phases
216 #~(modify-phases %standard-phases
217 (add-before 'build 'generate-everything
218 (lambda* (#:key inputs native-inputs #:allow-other-keys)
219 (invoke
220 (search-input-file (or native-inputs inputs) "/bin/runhaskell")
221 "GenerateEverything.hs"
222 "--out-dir" "doc/"))))))
223 (native-inputs (list ghc-filemanip))
224 (synopsis "The Agda Standard Library")
225 (description
226 "The standard library aims to contain all the tools needed to write
227both programs and proofs easily. While we always try and write efficient
228code, we prioritize ease of proof over type-checking and normalization
229performance. If computational performance is important to you, then perhaps
230try agda-prelude instead.")
231 (home-page "https://wiki.portal.chalmers.se/agda/pmwiki.php")
232 (license license:expat)))
233
234(define-public agda-categories
235 (package
236 (name "agda-categories")
237 (version "0.2.0")
238 (source (origin
239 (method git-fetch)
240 (uri (git-reference
241 (url "https://github.com/agda/agda-categories.git")
242 (commit (string-append "v" version))))
243 (file-name (git-file-name name version))
244 (sha256
245 (base32
246 "0a9mz9zyifkm03ss00iixa7b844m3gyvsx92al410hqj6v3r02qr"))
247 (patches (search-patches "agda-categories-remove-incompatible-flags.patch"
248 "agda-categories-use-find.patch"
249 "agda-categories-use-newer-stdlib.patch"))))
250 (build-system agda-build-system)
251 (arguments
252 (list
253 #:gnu-and-haskell? #t
254 #:phases
255 #~(modify-phases %standard-phases
256 (replace 'build
257 (lambda _
258 (invoke "make"))))))
259 (propagated-inputs
260 (list agda-stdlib))
261 (synopsis "New Categories library for Agda")
262 (description "A new Categories library for Agda")
263 (home-page "https://github.com/agda/agda-categories")
264 (license license:expat)))
265
266(define-public agda-cubical
267 (package
268 (name "agda-cubical")
269 (version "0.7")
270 (source (origin
271 (method git-fetch)
272 (uri (git-reference
273 (url "https://github.com/agda/cubical.git")
274 (commit (string-append "v" version))))
275 (file-name (git-file-name name version))
276 (sha256
277 (base32
278 "1c6axx3xx9ga7pl5294xqwklgbw96irxj0n74a1bxafhcx2lmfm0"))))
279 (build-system agda-build-system)
280 (arguments
281 (list
282 #:gnu-and-haskell? #t
283 #:phases
284 #~(modify-phases %standard-phases
285 (replace 'build
286 (lambda _
287 (invoke "make"))))))
288 (synopsis "Standard library for Cubical Agda")
289 (description "A standard library for Cubical Agda, comparable to
290agda-stdlib but using cubical methods.")
291 (home-page "https://github.com/agda/cubical")
292 (license license:expat)))
293
294(define-public agda-1lab
295 ;; Upstream doesn't do releases (yet). Use a commit that builds with 2.6.4,
296 ;; since they use Agda HEAD.
297 (let* ((revision "3")
298 (commit "afcf848d367f906d6d07d1612fbd41d7dd8c978e"))
299 (package
300 (name "agda-1lab")
301 (version (git-version "0.0" revision commit))
302 (source
303 (origin
304 (method git-fetch)
305 (uri (git-reference
306 (url "https://github.com/plt-amy/1lab.git")
307 (commit commit)))
308 (file-name (git-file-name name version))
309 (sha256
310 (base32
311 "12ax3n9111dkzm7nm3kwnvgslzsybyh740vml7l089in89f979wn"))))
312 (build-system agda-build-system)
313 (arguments
314 ;; Check files individually first, to avoid running out of heap :(
315 (list #:plan '(("src/.+/.+\\.lagda\\.md$")
316 ("src/index\\.lagda\\.md$"))))
317 (synopsis "Reference resource for mathematics done in Homotopy Type Theory")
318 (description "A formalised, cross-linked reference resource for
319mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is
320not a “linear” resource: Concepts are presented as a directed graph, with
321links indicating dependencies.")
322 (home-page "https://1lab.dev")
323 (license license:agpl3))))