projects/guix·blob javascript-team · refs

586 lines · 23.1 KiB

1;;; GNU Guix --- Functional package management for GNU
2;;; Copyright © 2019 Amin Bandali <[email protected]>
3;;; Copyright © 2020 Brett Gilio <[email protected]>
4;;; Copyright © 2020 Tobias Geerinckx-Rice <[email protected]>
5;;; Copyright © 2022 Pradana Aumars <[email protected]>
6;;; Copyright © 2023 Zhu Zihao <[email protected]>
7;;; Copyright © 2025 Luca Di Sera <[email protected]>
8;;; Copyright © 2026 Lîm Tsú-thuàn <[email protected]>
9;;; Copyright © 2026 Carlo Zancanaro <[email protected]>
10;;;
11;;; This file is part of GNU Guix.
12;;;
13;;; GNU Guix is free software; you can redistribute it and/or modify it
14;;; under the terms of the GNU General Public License as published by
15;;; the Free Software Foundation; either version 3 of the License, or (at
16;;; your option) any later version.
17;;;
18;;; GNU Guix is distributed in the hope that it will be useful, but
19;;; WITHOUT ANY WARRANTY; without even the implied warranty of
20;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
21;;; GNU General Public License for more details.
22;;;
23;;; You should have received a copy of the GNU General Public License
24;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
25
26(define-module (gnu packages lean)
27 #:use-module (ice-9 match)
28 #:use-module (gnu packages base)
29 #:use-module (gnu packages bash)
30 #:use-module (gnu packages check)
31 #:use-module (gnu packages llvm)
32 #:use-module (gnu packages c)
33 #:use-module (gnu packages maths)
34 #:use-module (gnu packages multiprecision)
35 #:use-module (guix build-system cmake)
36 #:use-module (guix build-system gnu)
37 #:use-module (guix build-system pyproject)
38 #:use-module ((guix licenses) #:prefix license:)
39 #:use-module (guix gexp)
40 #:use-module (guix packages)
41 #:use-module (guix git-download)
42 #:use-module (gnu packages graphviz)
43 #:use-module (gnu packages libevent)
44 #:use-module (gnu packages perl)
45 #:use-module (gnu packages pkg-config)
46 #:use-module (gnu packages version-control)
47 #:use-module (gnu packages python)
48 #:use-module (gnu packages python-build)
49 #:use-module (gnu packages python-crypto)
50 #:use-module (gnu packages python-web)
51 #:use-module (gnu packages python-xyz))
52
53(define-public lean4
54 (package
55 (name "lean4")
56 (version "4.29.0")
57 (home-page "https://lean-lang.org" )
58 (source (origin
59 (method git-fetch)
60 (uri (git-reference
61 (url "https://github.com/leanprover/lean4.git")
62 (commit (string-append "v" version))))
63 (file-name (git-file-name name version))
64 (sha256
65 (base32
66 "09f347n99iicvq3gnjkxxf0ym2964c9fwalmb1dp0x4bn170xznj"))))
67 (build-system cmake-build-system)
68 (native-inputs
69 (list git ; for the tests
70 perl ; for the tests
71 pkg-config
72 python-wrapper
73 tzdata-for-tests))
74 (inputs
75 (list cadical gmp libuv llvm))
76 (arguments
77 (list
78 #:make-flags
79 #~(list "SHELL=bash -euo pipefail")
80 #:build-type "Release" ; default upstream build type
81 ;; XXX: Test phases currently fail on 32-bit sytems.
82 ;; Tests for those architectures have been temporarily
83 ;; disabled, pending further investigation.
84 #:tests? (and (not (%current-target-system))
85 (let ((arch (%current-system)))
86 (not (or (string-prefix? "i686" arch)
87 (string-prefix? "armhf" arch)))))
88 #:phases
89 #~(modify-phases %standard-phases
90 (add-before 'configure 'patch
91 (lambda _
92 (substitute* '("stage0/src/CMakeLists.txt"
93 "src/CMakeLists.txt")
94 ;; Convert clang option to GCC option.
95 (("--print-target-triple") "-dumpmachine")) ; -print-multiarch
96 (substitute* '("src/bin/leanc.in"
97 "src/util/ffi.cpp"
98 "stage0/src/bin/leanc.in"
99 "stage0/src/util/ffi.cpp")
100 ;; Prevent ld error from:
101 ;; "--start-group" "-lInit" "-lleanrt" "--end-group" "-lstdc++"
102 ;; "-lLake" ""
103 ((" @LEAN_EXTRA_LINKER_FLAGS@")
104 "@LEAN_EXTRA_LINKER_FLAGS@"))
105 (substitute* "src/lean.mk.in"
106 (("SHELL = /usr/bin/env bash")
107 "SHELL = bash"))
108 (substitute* "src/stdlib.make.in"
109 (("/usr/bin/env bash")
110 "bash"))
111 (setenv "SHELL" "bash -euo pipefail")))
112 (add-after 'configure 'pre-populate-mimalloc
113 (lambda _
114 ;; Lean's CMake tries to git-clone mimalloc at build
115 ;; time, which fails in the sandbox. Pre-populate the
116 ;; source and create stamp files so ExternalProject
117 ;; skips the download.
118 (let ((mimalloc-dir "../build/mimalloc/src/mimalloc")
119 (stamp-dir "../build/mimalloc/src/mimalloc-stamp"))
120 (mkdir-p stamp-dir)
121 (copy-recursively #$(package-source mimalloc) mimalloc-dir)
122 ;; Create stamp files so ExternalProject skips all steps.
123 (for-each (lambda (step)
124 (call-with-output-file
125 (string-append stamp-dir "/mimalloc-" step)
126 (lambda (port) (display "" port))))
127 '("mkdir" "download" "update" "patch"
128 "configure" "build" "install")))))
129 (replace 'check
130 (lambda* (#:key tests? parallel-tests? #:allow-other-keys)
131 (when tests?
132 (with-directory-excursion "../source"
133 (invoke "ctest" "--preset" "release" "--test-dir" "../build/stage1"
134 "-E" (string-join
135 (list "leancomptest_(doc_example|foreign)"
136 "tests/lake/examples/(reverse-ffi|ffi)"
137 "tests/lean/run/(timeIO|async_dns)"
138 "tests/lean/server/"
139 "tests/lean/interactive/")
140 "|")
141 "-j" (if parallel-tests?
142 (number->string (parallel-job-count))
143 "1"))))))
144 (add-before 'install 'delete-junk
145 (lambda _
146 ;; Package is reproducible with ".git" deleted.
147 (for-each delete-file-recursively
148 (find-files "../source/src/lake/tests" "^\\.git$"
149 #:directories? #t)))))))
150 (native-search-paths
151 ;; Lean packages are a full build tree for the package, which stores its
152 ;; build results in this directory. This fits with how Lake expects to
153 ;; find things, so it all works out. Hopefully upstream improves this
154 ;; over time: https://github.com/leanprover/lean4/issues/5122
155 (list (search-path-specification
156 (variable "LEAN_PATH")
157 (files (list ".lake/build/lib/lean")))))
158 (synopsis "Theorem prover and programming language")
159 (description
160 "Lean is a theorem prover and programming language with a small trusted
161core based on dependent typed theory, aiming to bridge the gap between
162interactive and automated theorem proving.")
163 (license license:asl2.0)))
164
165(define (lean-package-name package)
166 "Return the name of the Lean package that this Guix PACKAGE represents, as
167specified in its lean-package-name property."
168 (assoc-ref (package-properties package)
169 'lean-package-name))
170
171(define (make-package-overrides.json package)
172 "Return a GEXP for a package-overrides.json file which tells Lake where to
173find the dependencies of PACKAGE."
174 (let* ((packages (map cadr
175 (package-propagated-inputs package)))
176 (relevant-packages (filter lean-package-name packages)))
177 (mixed-text-file "package-overrides.json"
178 "{\"version\":\"1.2.0\",\"packages\": ["
179 #~(string-join (list #$@(map (lambda (package
180 )
181 #~(string-append
182 "{\"name\":\""
183 #$(lean-package-name
184 package)
185 "\",\"type\":\"path\",\"dir\":\""
186 #$package
187 "\",\"inherited\":false}"))
188 relevant-packages)) ",")
189 "]}")))
190
191(define-syntax-rule (package-overrides.json)
192 "Returns a GEXP for a package-overrides.json file which tells Lake where to
193find the dependencies of the current package."
194 (make-package-overrides.json this-package))
195
196(define-public lean4-aesop
197 (package
198 (name "lean4-aesop")
199 (version (package-version lean4))
200 (source
201 (origin
202 (method git-fetch)
203 (uri (git-reference
204 (url "https://github.com/leanprover-community/aesop")
205 (commit (string-append "v" version))))
206 (file-name (git-file-name name version))
207 (sha256
208 (base32 "0n1njrklz5fh7xm7wd8sdagq2wgwrhcwjn04gpnnhf9w50v33p08"))))
209 (build-system gnu-build-system)
210 (arguments
211 (list
212 #:phases
213 #~(modify-phases %standard-phases
214 (delete 'configure)
215 (replace 'build
216 (lambda _
217 (setenv "CC" "gcc")
218 (invoke "lake" "build" "--packages"
219 #$(package-overrides.json) "Aesop:static")))
220 (delete 'check)
221 (replace 'install
222 (lambda _
223 (copy-recursively "."
224 #$output))))))
225 (native-inputs (list lean4))
226 (propagated-inputs (list lean4-batteries))
227 (home-page "https://github.com/leanprover-community/aesop")
228 (synopsis "White-box automation for Lean 4")
229 (description "Aesop is a proof tactic for Lean 4 that is broadly similar
230to Isabelle's @code{auto}. Definitions can be tagged with @code{@@[aesop]}.
231The @code{aesop} tactic will use these tagged definitions to attempt to
232automatically prove goals.")
233 (license license:asl2.0)
234 (properties '((lean-package-name . "aesop")))))
235
236(define-public lean4-batteries
237 (package
238 (name "lean4-batteries")
239 (version (package-version lean4))
240 (source
241 (origin
242 (method git-fetch)
243 (uri (git-reference
244 (url "https://github.com/leanprover-community/batteries")
245 (commit (string-append "v" version))))
246 (file-name (git-file-name name version))
247 (sha256
248 (base32 "013bh6anafhwgq8mav7yswqy7ym86gwvf5m6h39s45dnd25h6hmh"))))
249 (build-system gnu-build-system)
250 (arguments
251 (list
252 #:phases
253 #~(modify-phases %standard-phases
254 (delete 'configure)
255 (replace 'build
256 (lambda _
257 (setenv "CC" "gcc")
258 (invoke "lake" "build" "--packages"
259 #$(package-overrides.json) "Batteries:static")))
260 (delete 'check)
261 (replace 'install
262 (lambda _
263 (copy-recursively "."
264 #$output))))))
265 (native-inputs (list lean4))
266 (home-page "https://github.com/leanprover-community/batteries")
267 (synopsis
268 "Collection of maths/computer science data structures and tactics")
269 (description
270 "Batteries is the the \"batteries included\" extended library for Lean 4.
271This is a collection of data structures and tactics intended for use by both
272computer-science applications and mathematics applications of Lean 4.")
273 (license license:asl2.0)
274 (properties '((lean-package-name . "batteries")))))
275
276(define-public lean4-cli
277 (package
278 (name "lean4-cli")
279 (version (package-version lean4))
280 (source
281 (origin
282 (method git-fetch)
283 (uri (git-reference
284 (url "https://github.com/leanprover/lean4-cli")
285 (commit (string-append "v" version))))
286 (file-name (git-file-name name version))
287 (sha256
288 (base32 "0fasl91y1dlfpgd8whfs6cbv1a8z0m2p07p47rc0p6ymqpi2a9cc"))))
289 (build-system gnu-build-system)
290 (arguments
291 (list
292 #:phases
293 #~(modify-phases %standard-phases
294 (delete 'configure)
295 (replace 'build
296 (lambda _
297 (setenv "CC" "gcc")
298 (invoke "lake" "build" "Cli:static")))
299 (delete 'check)
300 (replace 'install
301 (lambda _
302 (copy-recursively "."
303 #$output))))))
304 (native-inputs (list lean4))
305 (home-page "https://github.com/leanprover/lean4-cli")
306 (synopsis "Command line parsing for Lean 4")
307 (description "Cli is a Lean 4 library for configuring Command Line
308Interfaces and parsing command line arguments. Commands are configured with a
309lightweight DSL.")
310 (license license:expat)
311 (properties '((lean-package-name . "Cli")))))
312
313(define-public lean4-import-graph
314 (package
315 (name "lean4-import-graph")
316 (version (package-version lean4))
317 (source
318 (origin
319 (method git-fetch)
320 (uri (git-reference
321 (url "https://github.com/leanprover-community/import-graph")
322 (commit (string-append "v" version))))
323 (file-name (git-file-name name version))
324 (sha256
325 (base32 "1f39gycfiwwfkk39fp1x9169f8xn7vpblcmddk29r24nmkd4x9xn"))))
326 (build-system gnu-build-system)
327 (arguments
328 (list
329 #:phases
330 #~(modify-phases %standard-phases
331 (delete 'configure)
332 (replace 'build
333 (lambda _
334 (setenv "CC" "gcc")
335 (invoke "lake" "build" "--packages"
336 #$(package-overrides.json) "ImportGraph:static")))
337 (delete 'check)
338 (replace 'install
339 (lambda _
340 (copy-recursively "."
341 #$output))))))
342 (native-inputs (list lean4))
343 (propagated-inputs (list lean4-cli))
344 (home-page "https://github.com/leanprover-community/import-graph")
345 (synopsis "Create import graphs of Lake packages")
346 (description
347 "This package provides a tool to create import graphs of Lake packages
348(Lean projects) in the Graphviz/dot format or as HTML.")
349 (license license:asl2.0)
350 (properties '((lean-package-name . "importGraph")))))
351
352(define-public lean4-mathlib4
353 (package
354 (name "lean4-mathlib4")
355 (version (package-version lean4))
356 (source
357 (origin
358 (method git-fetch)
359 (uri (git-reference
360 (url "https://github.com/leanprover-community/mathlib4")
361 (commit (string-append "v" version))))
362 (file-name (git-file-name name version))
363 (sha256
364 (base32 "1wbrb5nnxja0x8ccjvk0ppp6dbx1jcxgxxr503kx5i8dp15smvvx"))))
365 (build-system gnu-build-system)
366 (arguments
367 (list
368 #:phases
369 #~(modify-phases %standard-phases
370 (delete 'configure)
371 (add-before 'build 'remove-proof-widgets
372 (lambda _
373 ;; ProofWidgets needs some JavaScript dependencies that we can't
374 ;; properly package, so patch the lakefile to not require it.
375 (substitute* "lakefile.lean"
376 (("require \"leanprover-community\" / \"proofwidgets\"")
377 "/-")
378 (("Lean Zulip.\"")
379 "-/"))))
380 (add-before 'build 'remove-widget-tactics
381 (lambda _
382 ;; These tactics don't work without ProofWidgets, so delete them
383 ;; and all references to them.
384 (substitute* '("Mathlib.lean" "Mathlib/Tactic.lean"
385 "Mathlib/Tactic/Common.lean")
386 (("^public import Mathlib.Tactic.Widget.*")
387 ""))
388 (substitute* "Mathlib/Tactic/Linter/DirectoryDependency.lean"
389 (("\\(`MathlibTest.Header, `ProofWidgets\\),")
390 "")
391 ((", `ProofWidgets")
392 ""))
393 (delete-file-recursively "Mathlib/Tactic/Widget")))
394 (replace 'build
395 (lambda _
396 (setenv "CC" "gcc")
397 (invoke "lake" "build" "--packages"
398 #$(package-overrides.json) "Mathlib:static")))
399 (delete 'check)
400 (replace 'install
401 (lambda _
402 (copy-recursively "."
403 #$output))))))
404 (native-inputs (list lean4))
405 (propagated-inputs (list lean4-cli
406 lean4-batteries
407 lean4-quote4
408 lean4-aesop
409 lean4-import-graph
410 lean4-plausible
411 lean4-search-client))
412 (home-page "https://github.com/leanprover-community/mathlib4")
413 (synopsis "The math library of Lean 4")
414 (description
415 "Mathlib is a user maintained library for the Lean theorem
416prover. It contains both programming infrastructure and mathematics, as well
417as tactics that use the former and allow to develop the latter.")
418 (license license:asl2.0)
419 (properties '((lean-package-name . "MathLib")))))
420
421(define-public lean4-plausible
422 (package
423 (name "lean4-plausible")
424 (version (package-version lean4))
425 (source
426 (origin
427 (method git-fetch)
428 (uri (git-reference
429 (url "https://github.com/leanprover-community/plausible")
430 (commit (string-append "v" version))))
431 (file-name (git-file-name name version))
432 (sha256
433 (base32 "178vkdys7hzaf5w2m7rkpd4rm2hxgvly8rsy4y1hmr4ac43wviyk"))))
434 (build-system gnu-build-system)
435 (arguments
436 (list
437 #:phases
438 #~(modify-phases %standard-phases
439 (delete 'configure)
440 (replace 'build
441 (lambda _
442 (setenv "CC" "gcc")
443 (invoke "lake" "build" "--packages"
444 #$(package-overrides.json) "Plausible:static")))
445 (delete 'check)
446 (replace 'install
447 (lambda _
448 (copy-recursively "."
449 #$output))))))
450 (native-inputs (list lean4))
451 (propagated-inputs (list lean4-batteries))
452 (home-page "https://github.com/leanprover-community/plausible")
453 (synopsis "Property testing framework for Lean 4 that integrates into
454the tactic framework")
455 (description "Plausible is a property testing framework for Lean 4 that
456integrates into the tactic framework.")
457 (license license:asl2.0)
458 (properties '((lean-package-name . "plausible")))))
459
460(define-public lean4-quote4
461 (package
462 (name "lean4-quote4")
463 (version (package-version lean4))
464 (source
465 (origin
466 (method git-fetch)
467 (uri (git-reference
468 (url "https://github.com/leanprover-community/quote4")
469 (commit (string-append "v" version))))
470 (file-name (git-file-name name version))
471 (sha256
472 (base32 "03cx5xpm3sr6b8hmigq14apn4ahw13n12f7m17gbl9b7zn33kmm4"))))
473 (build-system gnu-build-system)
474 (arguments
475 (list
476 #:phases
477 #~(modify-phases %standard-phases
478 (delete 'configure)
479 (replace 'build
480 (lambda _
481 (setenv "CC" "gcc")
482 (invoke "lake" "build" "--packages"
483 #$(package-overrides.json) "Qq:static")))
484 (delete 'check)
485 (replace 'install
486 (lambda _
487 (copy-recursively "."
488 #$output))))))
489 (native-inputs (list lean4))
490 (home-page "https://github.com/leanprover-community/quote4")
491 (synopsis "Type-safe expression quotations for Lean 4")
492 (description
493 "This package implements type-safe expression quotations,
494which are a way of constructing object-level expressions (Expr) in meta-level
495code.")
496 (license license:asl2.0)
497 (properties '((lean-package-name . "Qq")))))
498
499(define-public lean4-search-client
500 (package
501 (name "lean4-search-client")
502 (version "4.32.0")
503 (source
504 (origin
505 (method git-fetch)
506 (uri (git-reference
507 (url "https://github.com/leanprover-community/LeanSearchClient")
508 (commit (string-append "v" version))))
509 (file-name (git-file-name name version))
510 (sha256
511 (base32 "1wwlh8sz9bhbrydr5ifrjiph9yf9agn3s0m9ljl68jsg6vv5a52k"))))
512 (build-system gnu-build-system)
513 (arguments
514 (list
515 #:phases
516 #~(modify-phases %standard-phases
517 (delete 'configure)
518 (replace 'build
519 (lambda _
520 (setenv "CC" "gcc")
521 (invoke "lake" "build" "--packages"
522 #$(package-overrides.json) "LeanSearchClient:static")))
523 (delete 'check)
524 (replace 'install
525 (lambda _
526 (copy-recursively "."
527 #$output))))))
528 (native-inputs (list lean4))
529 (home-page "https://github.com/leanprover-community/LeanSearchClient")
530 (synopsis "Natural language search within Lean")
531 (description
532 "LeanSearchClient provides syntax for search using the
533leansearch API and the LeanStateSearch API from within Lean. It allows you to
534search for Lean tactics and theorems using natural language. It also allows
535searches on Loogle from within Lean.")
536 (license license:asl2.0)
537 (properties '((lean-package-name . "LeanSearchClient")))))
538
539(define-public python-mathlibtools
540 (package
541 (name "python-mathlibtools")
542 (version "1.3.2")
543 (source
544 (origin
545 (method git-fetch)
546 (uri (git-reference
547 (url "https://github.com/leanprover-community/mathlib-tools")
548 (commit (string-append "v" version))))
549 (file-name (git-file-name name version))
550 (sha256
551 (base32 "0vjz3f2lvkql9dz9x1d9mq8vczqs70v2ar88g7p4wm6qq7pgx7l3"))))
552 (build-system pyproject-build-system)
553 (arguments
554 (list
555 #:test-flags
556 #~(list "-k"
557 ;; These tests require network access.
558 (string-join (list "not test_new"
559 "test_add"
560 "test_upgrade_project"
561 "test_upgrade_mathlib"
562 "test_get_tutorials")
563 " and not "))
564 #:phases
565 #~(modify-phases %standard-phases
566 (add-before 'build 'set-home-env
567 (lambda _
568 (setenv "HOME" "/tmp"))))))
569 (native-inputs (list python-pytest python-setuptools))
570 (inputs (list python-toml
571 python-pygithub
572 python-certifi
573 python-gitpython
574 python-requests
575 python-click
576 python-tqdm
577 python-networkx
578 python-pydot
579 python-pyyaml
580 python-atomicwrites))
581 (home-page "https://github.com/leanprover-community/mathlib-tools")
582 (synopsis "Development tools for Lean mathlib")
583 (description
584 "This package contains @command{leanproject}, a supporting tool for Lean
585mathlib, a mathematical library for the Lean theorem prover.")
586 (license license:asl2.0)))