1 |
commit: b206aa4fe3a4c1c45600674a0a55626d80014e19 |
2 |
Author: Maciej Barć <xgqt <AT> riseup <DOT> net> |
3 |
AuthorDate: Tue Oct 19 21:41:00 2021 +0000 |
4 |
Commit: Maciej Barć <xgqt <AT> riseup <DOT> net> |
5 |
CommitDate: Tue Oct 19 21:41:00 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=b206aa4f |
7 |
|
8 |
dev-lang/lean: add version 3.33.0 |
9 |
|
10 |
Package-Manager: Portage-3.0.20, Repoman-3.0.3 |
11 |
Signed-off-by: Maciej Barć <xgqt <AT> riseup.net> |
12 |
|
13 |
dev-lang/lean/Manifest | 1 + |
14 |
dev-lang/lean/lean-3.33.0.ebuild | 45 ++++++++++++++++++++++++++++++++++++++++ |
15 |
dev-lang/lean/metadata.xml | 20 ++++++++++++++++++ |
16 |
3 files changed, 66 insertions(+) |
17 |
|
18 |
diff --git a/dev-lang/lean/Manifest b/dev-lang/lean/Manifest |
19 |
new file mode 100644 |
20 |
index 000000000..fd42aa380 |
21 |
--- /dev/null |
22 |
+++ b/dev-lang/lean/Manifest |
23 |
@@ -0,0 +1 @@ |
24 |
+DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3 |
25 |
|
26 |
diff --git a/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild |
27 |
new file mode 100644 |
28 |
index 000000000..120a2ac2e |
29 |
--- /dev/null |
30 |
+++ b/dev-lang/lean/lean-3.33.0.ebuild |
31 |
@@ -0,0 +1,45 @@ |
32 |
+# Copyright 1999-2021 Gentoo Authors |
33 |
+# Distributed under the terms of the GNU General Public License v2 |
34 |
+ |
35 |
+EAPI=7 |
36 |
+ |
37 |
+CMAKE_IN_SOURCE_BUILD="ON" |
38 |
+ |
39 |
+inherit cmake |
40 |
+ |
41 |
+DESCRIPTION="The Lean Theorem Prover" |
42 |
+HOMEPAGE="https://leanprover-community.github.io/" |
43 |
+ |
44 |
+if [[ "${PV}" == *9999* ]]; then |
45 |
+ inherit git-r3 |
46 |
+ EGIT_REPO_URI="https://github.com/leanprover-community/lean.git" |
47 |
+else |
48 |
+ SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz" |
49 |
+ KEYWORDS="~amd64" |
50 |
+fi |
51 |
+S="${WORKDIR}/lean-${PV}/src" |
52 |
+ |
53 |
+RESTRICT="!test? ( test )" |
54 |
+LICENSE="Apache-2.0" |
55 |
+SLOT="0" |
56 |
+IUSE="+json test +threads" |
57 |
+ |
58 |
+RDEPEND="dev-libs/gmp" |
59 |
+DEPEND="${RDEPEND}" |
60 |
+ |
61 |
+src_configure() { |
62 |
+ local mycmakeargs=( |
63 |
+ -DALPHA=ON |
64 |
+ -DAUTO_THREAD_FINALIZATION=ON |
65 |
+ -DJSON=$(usex json) |
66 |
+ -DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}" |
67 |
+ -DMULTI_THREAD=$(usex threads) |
68 |
+ -DUSE_GITHASH=OFF |
69 |
+ ) |
70 |
+ cmake_src_configure |
71 |
+} |
72 |
+ |
73 |
+pkg_postinst() { |
74 |
+ elog "You probably want to use lean with mathlib, to install it use leanpkg." |
75 |
+ elog "For example: leanpkg install https://github.com/leanprover-community/mathlib" |
76 |
+} |
77 |
|
78 |
diff --git a/dev-lang/lean/metadata.xml b/dev-lang/lean/metadata.xml |
79 |
new file mode 100644 |
80 |
index 000000000..9e03d53ad |
81 |
--- /dev/null |
82 |
+++ b/dev-lang/lean/metadata.xml |
83 |
@@ -0,0 +1,20 @@ |
84 |
+<?xml version="1.0" encoding="UTF-8"?> |
85 |
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
86 |
+ |
87 |
+<pkgmetadata> |
88 |
+ <maintainer type="person"> |
89 |
+ <email>xgqt@××××××.net</email> |
90 |
+ <name>Maciej Barć</name> |
91 |
+ </maintainer> |
92 |
+ <longdescription lang="en"> |
93 |
+ The Lean theorem prover is a proof assistant developed principally |
94 |
+ by Leonardo de Moura at Microsoft Research. |
95 |
+ </longdescription> |
96 |
+ <upstream> |
97 |
+ <bugs-to>https://github.com/leanprover-community/lean/issues</bugs-to> |
98 |
+ <remote-id type="github">leanprover-community/lean</remote-id> |
99 |
+ </upstream> |
100 |
+ <use> |
101 |
+ <flag name="json"> Enable JSON support</flag> |
102 |
+ </use> |
103 |
+</pkgmetadata> |