projects/guix·blob ruby-team · refs

202 lines · 8.6 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;;;
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 lean)
26 #:use-module (ice-9 match)
27 #:use-module (gnu packages base)
28 #:use-module (gnu packages bash)
29 #:use-module (gnu packages check)
30 #:use-module (gnu packages llvm)
31 #:use-module (gnu packages c)
32 #:use-module (gnu packages maths)
33 #:use-module (gnu packages multiprecision)
34 #:use-module (guix build-system cmake)
35 #:use-module (guix build-system pyproject)
36 #:use-module ((guix licenses) #:prefix license:)
37 #:use-module (guix gexp)
38 #:use-module (guix packages)
39 #:use-module (guix git-download)
40 #:use-module (gnu packages graphviz)
41 #:use-module (gnu packages libevent)
42 #:use-module (gnu packages perl)
43 #:use-module (gnu packages pkg-config)
44 #:use-module (gnu packages version-control)
45 #:use-module (gnu packages python)
46 #:use-module (gnu packages python-build)
47 #:use-module (gnu packages python-crypto)
48 #:use-module (gnu packages python-web)
49 #:use-module (gnu packages python-xyz))
50
51(define-public lean4
52 (package
53 (name "lean4")
54 (version "4.29.0")
55 (home-page "https://lean-lang.org" )
56 (source (origin
57 (method git-fetch)
58 (uri (git-reference
59 (url "https://github.com/leanprover/lean4.git")
60 (commit (string-append "v" version))))
61 (file-name (git-file-name name version))
62 (sha256
63 (base32
64 "09f347n99iicvq3gnjkxxf0ym2964c9fwalmb1dp0x4bn170xznj"))))
65 (build-system cmake-build-system)
66 (native-inputs
67 (list git ; for the tests
68 perl ; for the tests
69 pkg-config
70 python-wrapper
71 tzdata-for-tests))
72 (inputs
73 (list cadical gmp libuv llvm))
74 (arguments
75 (list
76 #:make-flags
77 #~(list "SHELL=bash -euo pipefail")
78 #:build-type "Release" ; default upstream build type
79 ;; XXX: Test phases currently fail on 32-bit sytems.
80 ;; Tests for those architectures have been temporarily
81 ;; disabled, pending further investigation.
82 #:tests? (and (not (%current-target-system))
83 (let ((arch (%current-system)))
84 (not (or (string-prefix? "i686" arch)
85 (string-prefix? "armhf" arch)))))
86 #:phases
87 #~(modify-phases %standard-phases
88 (add-before 'configure 'patch
89 (lambda _
90 (substitute* '("stage0/src/CMakeLists.txt"
91 "src/CMakeLists.txt")
92 ;; Convert clang option to GCC option.
93 (("--print-target-triple") "-dumpmachine")) ; -print-multiarch
94 (substitute* '("src/bin/leanc.in"
95 "src/util/ffi.cpp"
96 "stage0/src/bin/leanc.in"
97 "stage0/src/util/ffi.cpp")
98 ;; Prevent ld error from:
99 ;; "--start-group" "-lInit" "-lleanrt" "--end-group" "-lstdc++"
100 ;; "-lLake" ""
101 ((" @LEAN_EXTRA_LINKER_FLAGS@")
102 "@LEAN_EXTRA_LINKER_FLAGS@"))
103 (substitute* "src/lean.mk.in"
104 (("SHELL = /usr/bin/env bash")
105 "SHELL = bash"))
106 (substitute* "src/stdlib.make.in"
107 (("/usr/bin/env bash")
108 "bash"))
109 (setenv "SHELL" "bash -euo pipefail")))
110 (add-after 'configure 'pre-populate-mimalloc
111 (lambda _
112 ;; Lean's CMake tries to git-clone mimalloc at build
113 ;; time, which fails in the sandbox. Pre-populate the
114 ;; source and create stamp files so ExternalProject
115 ;; skips the download.
116 (let ((mimalloc-dir "../build/mimalloc/src/mimalloc")
117 (stamp-dir "../build/mimalloc/src/mimalloc-stamp"))
118 (mkdir-p stamp-dir)
119 (copy-recursively #$(package-source mimalloc) mimalloc-dir)
120 ;; Create stamp files so ExternalProject skips all steps.
121 (for-each (lambda (step)
122 (call-with-output-file
123 (string-append stamp-dir "/mimalloc-" step)
124 (lambda (port) (display "" port))))
125 '("mkdir" "download" "update" "patch"
126 "configure" "build" "install")))))
127 (replace 'check
128 (lambda* (#:key tests? parallel-tests? #:allow-other-keys)
129 (when tests?
130 (with-directory-excursion "../source"
131 (invoke "ctest" "--preset" "release" "--test-dir" "../build/stage1"
132 "-E" (string-join
133 (list "leancomptest_(doc_example|foreign)"
134 "tests/lake/examples/(reverse-ffi|ffi)"
135 "tests/lean/run/(timeIO|async_dns)"
136 "tests/lean/server/"
137 "tests/lean/interactive/")
138 "|")
139 "-j" (if parallel-tests?
140 (number->string (parallel-job-count))
141 "1"))))))
142 (add-before 'install 'delete-junk
143 (lambda _
144 ;; Package is reproducible with ".git" deleted.
145 (for-each delete-file-recursively
146 (find-files "../source/src/lake/tests" "^\\.git$"
147 #:directories? #t)))))))
148 (synopsis "Theorem prover and programming language")
149 (description
150 "Lean is a theorem prover and programming language with a small trusted
151core based on dependent typed theory, aiming to bridge the gap between
152interactive and automated theorem proving.")
153 (license license:asl2.0)))
154
155(define-public python-mathlibtools
156 (package
157 (name "python-mathlibtools")
158 (version "1.3.2")
159 (source
160 (origin
161 (method git-fetch)
162 (uri (git-reference
163 (url "https://github.com/leanprover-community/mathlib-tools")
164 (commit (string-append "v" version))))
165 (file-name (git-file-name name version))
166 (sha256
167 (base32 "0vjz3f2lvkql9dz9x1d9mq8vczqs70v2ar88g7p4wm6qq7pgx7l3"))))
168 (build-system pyproject-build-system)
169 (arguments
170 (list
171 #:test-flags
172 #~(list "-k"
173 ;; These tests require network access.
174 (string-join (list "not test_new"
175 "test_add"
176 "test_upgrade_project"
177 "test_upgrade_mathlib"
178 "test_get_tutorials")
179 " and not "))
180 #:phases
181 #~(modify-phases %standard-phases
182 (add-before 'build 'set-home-env
183 (lambda _
184 (setenv "HOME" "/tmp"))))))
185 (native-inputs (list python-pytest python-setuptools))
186 (inputs (list python-toml
187 python-pygithub
188 python-certifi
189 python-gitpython
190 python-requests
191 python-click
192 python-tqdm
193 python-networkx
194 python-pydot
195 python-pyyaml
196 python-atomicwrites))
197 (home-page "https://github.com/leanprover-community/mathlib-tools")
198 (synopsis "Development tools for Lean mathlib")
199 (description
200 "This package contains @command{leanproject}, a supporting tool for Lean
201mathlib, a mathematical library for the Lean theorem prover.")
202 (license license:asl2.0)))