* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2021-10-22 0:46 Alessandro Barbieri
0 siblings, 0 replies; 7+ messages in thread
From: Alessandro Barbieri @ 2021-10-22 0:46 UTC (permalink / raw
To: gentoo-commits
commit: ddb94e3f25373ae8eae84682060e36b6bf108bf0
Author: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Fri Oct 22 00:09:12 2021 +0000
Commit: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Fri Oct 22 00:09:28 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=ddb94e3f
sci-mathematics/lean-mathlib: initial import
Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>
sci-mathematics/lean-mathlib/Manifest | 1 +
.../lean-mathlib/lean-mathlib-0.1_p20211021.ebuild | 43 ++++++++++++++++++++++
sci-mathematics/lean-mathlib/metadata.xml | 15 ++++++++
3 files changed, 59 insertions(+)
diff --git a/sci-mathematics/lean-mathlib/Manifest b/sci-mathematics/lean-mathlib/Manifest
new file mode 100644
index 000000000..6d4751f6e
--- /dev/null
+++ b/sci-mathematics/lean-mathlib/Manifest
@@ -0,0 +1 @@
+DIST lean-mathlib-0.1_p20211021.tar.gz 6665360 BLAKE2B 92d7627a095fd8cbc2bbdeccd9321c86badbd36152a034a15d005eadd0507c21aeeb73ecbef8199a267104b5b881ba5b100355e48003c68785205650c4a23876 SHA512 792e8074cba39d1baab87f47af64c49f2a95043c8e9d592f41fe87d8697405c2595933954e1fbf30cb657551e2350fa274e405996d030e47db166cd078a232e4
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
new file mode 100644
index 000000000..5b3bfe7c8
--- /dev/null
+++ b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
@@ -0,0 +1,43 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+COMMIT="3c11bd771ef17197a9e9fcd4a3fabfa2804d950c"
+
+DESCRIPTION="Lean mathematical components library"
+HOMEPAGE="https://github.com/leanprover-community/mathlib"
+SRC_URI="https://github.com/leanprover-community/mathlib/archive/${COMMIT}.tar.gz -> ${PF}.tar.gz"
+S="${WORKDIR}/mathlib-${COMMIT}"
+
+KEYWORDS="~amd64"
+LICENSE="Apache-2.0"
+SLOT="0"
+IUSE="test"
+
+RDEPEND=">=dev-lang/lean-3.34.0"
+DEPEND="
+ ${RDEPEND}
+ sci-mathematics/mathlib-tools
+"
+
+RESTRICT="!test? ( test )"
+
+src_configure() {
+ leanpkg configure || die
+}
+
+src_compile() {
+ leanpkg build || die
+}
+
+src_install() {
+ dodoc -r docs
+ rm -r docs || die
+ insinto /usr/lib/lean/mathlib
+ doins -r .
+}
+
+src_test() {
+ leanpkg test || die
+}
diff --git a/sci-mathematics/lean-mathlib/metadata.xml b/sci-mathematics/lean-mathlib/metadata.xml
new file mode 100644
index 000000000..3005583c8
--- /dev/null
+++ b/sci-mathematics/lean-mathlib/metadata.xml
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+ <maintainer type="person">
+ <email>lssndrbarbieri@gmail.com</email>
+ <name>Alessandro Barbieri</name>
+ </maintainer>
+ <longdescription lang="en">
+ </longdescription>
+ <upstream>
+ <bugs-to>https://github.com/leanprover-community/mathlib/issues</bugs-to>
+ <remote-id type="github">leanprover-community/mathlib</remote-id>
+ </upstream>
+</pkgmetadata>
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2021-10-23 5:11 Alessandro Barbieri
0 siblings, 0 replies; 7+ messages in thread
From: Alessandro Barbieri @ 2021-10-23 5:11 UTC (permalink / raw
To: gentoo-commits
commit: 88ff5382788c91478f80c6a576f9f4466e7bccb7
Author: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Sat Oct 23 05:11:22 2021 +0000
Commit: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Sat Oct 23 05:11:22 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=88ff5382
sci-mathematics/lean-mathlib: fix doc install
Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>
sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
index 5b3bfe7c8..414cad8fb 100644
--- a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
+++ b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
@@ -32,7 +32,7 @@ src_compile() {
}
src_install() {
- dodoc -r docs
+ dodoc -r docs/*
rm -r docs || die
insinto /usr/lib/lean/mathlib
doins -r .
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2021-10-24 14:53 Arthur Zamarin
0 siblings, 0 replies; 7+ messages in thread
From: Arthur Zamarin @ 2021-10-24 14:53 UTC (permalink / raw
To: gentoo-commits
commit: d9faaebbd0cbf547f9f496b312b1a6daa7bf8319
Author: Arthur Zamarin <arthurzam <AT> gentoo <DOT> org>
AuthorDate: Sun Oct 24 14:41:33 2021 +0000
Commit: Arthur Zamarin <arthurzam <AT> gentoo <DOT> org>
CommitDate: Sun Oct 24 14:41:33 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=d9faaebb
sci-mathematics/lean-mathlib: remove empty longdescription
Signed-off-by: Arthur Zamarin <arthurzam <AT> gentoo.org>
sci-mathematics/lean-mathlib/metadata.xml | 2 --
1 file changed, 2 deletions(-)
diff --git a/sci-mathematics/lean-mathlib/metadata.xml b/sci-mathematics/lean-mathlib/metadata.xml
index 3005583c8..cb8636fef 100644
--- a/sci-mathematics/lean-mathlib/metadata.xml
+++ b/sci-mathematics/lean-mathlib/metadata.xml
@@ -6,8 +6,6 @@
<email>lssndrbarbieri@gmail.com</email>
<name>Alessandro Barbieri</name>
</maintainer>
- <longdescription lang="en">
- </longdescription>
<upstream>
<bugs-to>https://github.com/leanprover-community/mathlib/issues</bugs-to>
<remote-id type="github">leanprover-community/mathlib</remote-id>
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2021-12-01 19:50 Andrew Ammerlaan
0 siblings, 0 replies; 7+ messages in thread
From: Andrew Ammerlaan @ 2021-12-01 19:50 UTC (permalink / raw
To: gentoo-commits
commit: 6c79f5e387b454cdfbe5d9f3826cfbea41a4055b
Author: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 1 19:50:06 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Wed Dec 1 19:50:06 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=6c79f5e3
sci-mathematics/lean-mathlib: dev-lang/lean --> sci-mathematics/lean
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>
sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
index 414cad8fb..0f991487e 100644
--- a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
+++ b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
@@ -15,7 +15,7 @@ LICENSE="Apache-2.0"
SLOT="0"
IUSE="test"
-RDEPEND=">=dev-lang/lean-3.34.0"
+RDEPEND=">=sci-mathematics/lean-3.34.0"
DEPEND="
${RDEPEND}
sci-mathematics/mathlib-tools
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2022-03-19 2:02 Alessandro Barbieri
0 siblings, 0 replies; 7+ messages in thread
From: Alessandro Barbieri @ 2022-03-19 2:02 UTC (permalink / raw
To: gentoo-commits
commit: 4c20f182f85c0ee52c965866bf9ccc0ace9fbbff
Author: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Sat Mar 19 02:02:07 2022 +0000
Commit: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Sat Mar 19 02:02:07 2022 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=4c20f182
sci-mathematics/lean-mathlib: add 0.1_p20220318
Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>
sci-mathematics/lean-mathlib/Manifest | 1 +
.../lean-mathlib/lean-mathlib-0.1_p20220318.ebuild | 43 ++++++++++++++++++++++
2 files changed, 44 insertions(+)
diff --git a/sci-mathematics/lean-mathlib/Manifest b/sci-mathematics/lean-mathlib/Manifest
index 6d4751f6e..bebf898ba 100644
--- a/sci-mathematics/lean-mathlib/Manifest
+++ b/sci-mathematics/lean-mathlib/Manifest
@@ -1 +1,2 @@
DIST lean-mathlib-0.1_p20211021.tar.gz 6665360 BLAKE2B 92d7627a095fd8cbc2bbdeccd9321c86badbd36152a034a15d005eadd0507c21aeeb73ecbef8199a267104b5b881ba5b100355e48003c68785205650c4a23876 SHA512 792e8074cba39d1baab87f47af64c49f2a95043c8e9d592f41fe87d8697405c2595933954e1fbf30cb657551e2350fa274e405996d030e47db166cd078a232e4
+DIST lean-mathlib-0.1_p20220318.tar.gz 8076743 BLAKE2B d8c76b93309f5b778654ccd7f8ecd68f9fed72b9bd5e40c5909c193bce96e2af0edf530232d71893a802f5292d7b34a83783826dbda619f8e4450431e0eda153 SHA512 a3708be6c1792de80015ff7ac242ed85ac2eb2e283774721e6f778fb98dd42380556f1238a4cd880f3f22377966cc06e7b92ca62cae078c01302c44c6377d608
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild
new file mode 100644
index 000000000..a1e9902e3
--- /dev/null
+++ b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild
@@ -0,0 +1,43 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+COMMIT="d04fff95f686d5c372f7895551c40e7fa683ed6b"
+
+DESCRIPTION="Lean mathematical components library"
+HOMEPAGE="https://github.com/leanprover-community/mathlib"
+SRC_URI="https://github.com/leanprover-community/mathlib/archive/${COMMIT}.tar.gz -> ${PF}.tar.gz"
+S="${WORKDIR}/mathlib-${COMMIT}"
+
+KEYWORDS="~amd64"
+LICENSE="Apache-2.0"
+SLOT="0"
+IUSE="test"
+
+RDEPEND=">=sci-mathematics/lean-3.41.0"
+DEPEND="
+ ${RDEPEND}
+ sci-mathematics/mathlib-tools
+"
+
+RESTRICT="!test? ( test )"
+
+src_configure() {
+ leanpkg configure || die
+}
+
+src_compile() {
+ leanpkg build || die
+}
+
+src_install() {
+ dodoc -r docs/*
+ rm -r docs || die
+ insinto /usr/lib/lean/mathlib
+ doins -r .
+}
+
+src_test() {
+ leanpkg test || die
+}
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2022-03-26 0:09 Alessandro Barbieri
0 siblings, 0 replies; 7+ messages in thread
From: Alessandro Barbieri @ 2022-03-26 0:09 UTC (permalink / raw
To: gentoo-commits
commit: 4bf925478b561d2c6fff0c0ed19590716fc7aa65
Author: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Thu Mar 24 14:42:00 2022 +0000
Commit: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Sat Mar 26 00:09:35 2022 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=4bf92547
sci-mathematics/lean-mathlib: add 0.1_p20220324
Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>
sci-mathematics/lean-mathlib/Manifest | 1 +
.../lean-mathlib/lean-mathlib-0.1_p20220324.ebuild | 43 ++++++++++++++++++++++
2 files changed, 44 insertions(+)
diff --git a/sci-mathematics/lean-mathlib/Manifest b/sci-mathematics/lean-mathlib/Manifest
index bebf898ba..cff053911 100644
--- a/sci-mathematics/lean-mathlib/Manifest
+++ b/sci-mathematics/lean-mathlib/Manifest
@@ -1,2 +1,3 @@
DIST lean-mathlib-0.1_p20211021.tar.gz 6665360 BLAKE2B 92d7627a095fd8cbc2bbdeccd9321c86badbd36152a034a15d005eadd0507c21aeeb73ecbef8199a267104b5b881ba5b100355e48003c68785205650c4a23876 SHA512 792e8074cba39d1baab87f47af64c49f2a95043c8e9d592f41fe87d8697405c2595933954e1fbf30cb657551e2350fa274e405996d030e47db166cd078a232e4
DIST lean-mathlib-0.1_p20220318.tar.gz 8076743 BLAKE2B d8c76b93309f5b778654ccd7f8ecd68f9fed72b9bd5e40c5909c193bce96e2af0edf530232d71893a802f5292d7b34a83783826dbda619f8e4450431e0eda153 SHA512 a3708be6c1792de80015ff7ac242ed85ac2eb2e283774721e6f778fb98dd42380556f1238a4cd880f3f22377966cc06e7b92ca62cae078c01302c44c6377d608
+DIST lean-mathlib-0.1_p20220324.tar.gz 8117563 BLAKE2B f183565927e9b957059995d301a20af45d9995ae159c7e3aa54114b91e8421908b6494ab8abfe38215c8cbf0d4e714d08b0a43f24ba85deaec58577d2ac47a5b SHA512 39effb1dbb659f0dbaeb008bc3a3181aafd4c1ad6429d6ff70aca13481ccaefb12f97335e870c9737620d08dffdcb1a94970158637dc37b9ad00faff6a700f01
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220324.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220324.ebuild
new file mode 100644
index 000000000..d00f91335
--- /dev/null
+++ b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220324.ebuild
@@ -0,0 +1,43 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+COMMIT="7c48d65cd4546dcb1cfa01073cbe016fa7f3fbcc"
+
+DESCRIPTION="Lean mathematical components library"
+HOMEPAGE="https://github.com/leanprover-community/mathlib"
+SRC_URI="https://github.com/leanprover-community/mathlib/archive/${COMMIT}.tar.gz -> ${PF}.tar.gz"
+S="${WORKDIR}/mathlib-${COMMIT}"
+
+KEYWORDS="~amd64"
+LICENSE="Apache-2.0"
+SLOT="0"
+IUSE="test"
+
+RDEPEND=">=sci-mathematics/lean-3.42.0"
+DEPEND="
+ ${RDEPEND}
+ sci-mathematics/mathlib-tools
+"
+
+RESTRICT="!test? ( test )"
+
+src_configure() {
+ leanpkg configure || die
+}
+
+src_compile() {
+ leanpkg build || die
+}
+
+src_install() {
+ dodoc -r docs/*
+ rm -r docs || die
+ insinto /usr/lib/lean/mathlib
+ doins -r .
+}
+
+src_test() {
+ leanpkg test || die
+}
^ permalink raw reply related [flat|nested] 7+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/
@ 2022-03-26 0:09 Alessandro Barbieri
0 siblings, 0 replies; 7+ messages in thread
From: Alessandro Barbieri @ 2022-03-26 0:09 UTC (permalink / raw
To: gentoo-commits
commit: 749e26c7ecb86356f3404da0b76efb2f7b801a73
Author: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Fri Mar 25 23:41:16 2022 +0000
Commit: Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Sat Mar 26 00:09:36 2022 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=749e26c7
sci-mathematics/lean-mathlib: drop 0.1_p20211021, 0.1_p20220318
Closes: https://bugs.gentoo.org/835922
Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>
sci-mathematics/lean-mathlib/Manifest | 2 -
.../lean-mathlib/lean-mathlib-0.1_p20211021.ebuild | 43 ----------------------
.../lean-mathlib/lean-mathlib-0.1_p20220318.ebuild | 43 ----------------------
3 files changed, 88 deletions(-)
diff --git a/sci-mathematics/lean-mathlib/Manifest b/sci-mathematics/lean-mathlib/Manifest
index cff053911..b7e1f6439 100644
--- a/sci-mathematics/lean-mathlib/Manifest
+++ b/sci-mathematics/lean-mathlib/Manifest
@@ -1,3 +1 @@
-DIST lean-mathlib-0.1_p20211021.tar.gz 6665360 BLAKE2B 92d7627a095fd8cbc2bbdeccd9321c86badbd36152a034a15d005eadd0507c21aeeb73ecbef8199a267104b5b881ba5b100355e48003c68785205650c4a23876 SHA512 792e8074cba39d1baab87f47af64c49f2a95043c8e9d592f41fe87d8697405c2595933954e1fbf30cb657551e2350fa274e405996d030e47db166cd078a232e4
-DIST lean-mathlib-0.1_p20220318.tar.gz 8076743 BLAKE2B d8c76b93309f5b778654ccd7f8ecd68f9fed72b9bd5e40c5909c193bce96e2af0edf530232d71893a802f5292d7b34a83783826dbda619f8e4450431e0eda153 SHA512 a3708be6c1792de80015ff7ac242ed85ac2eb2e283774721e6f778fb98dd42380556f1238a4cd880f3f22377966cc06e7b92ca62cae078c01302c44c6377d608
DIST lean-mathlib-0.1_p20220324.tar.gz 8117563 BLAKE2B f183565927e9b957059995d301a20af45d9995ae159c7e3aa54114b91e8421908b6494ab8abfe38215c8cbf0d4e714d08b0a43f24ba85deaec58577d2ac47a5b SHA512 39effb1dbb659f0dbaeb008bc3a3181aafd4c1ad6429d6ff70aca13481ccaefb12f97335e870c9737620d08dffdcb1a94970158637dc37b9ad00faff6a700f01
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
deleted file mode 100644
index 0f991487e..000000000
--- a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20211021.ebuild
+++ /dev/null
@@ -1,43 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-COMMIT="3c11bd771ef17197a9e9fcd4a3fabfa2804d950c"
-
-DESCRIPTION="Lean mathematical components library"
-HOMEPAGE="https://github.com/leanprover-community/mathlib"
-SRC_URI="https://github.com/leanprover-community/mathlib/archive/${COMMIT}.tar.gz -> ${PF}.tar.gz"
-S="${WORKDIR}/mathlib-${COMMIT}"
-
-KEYWORDS="~amd64"
-LICENSE="Apache-2.0"
-SLOT="0"
-IUSE="test"
-
-RDEPEND=">=sci-mathematics/lean-3.34.0"
-DEPEND="
- ${RDEPEND}
- sci-mathematics/mathlib-tools
-"
-
-RESTRICT="!test? ( test )"
-
-src_configure() {
- leanpkg configure || die
-}
-
-src_compile() {
- leanpkg build || die
-}
-
-src_install() {
- dodoc -r docs/*
- rm -r docs || die
- insinto /usr/lib/lean/mathlib
- doins -r .
-}
-
-src_test() {
- leanpkg test || die
-}
diff --git a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild b/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild
deleted file mode 100644
index a1e9902e3..000000000
--- a/sci-mathematics/lean-mathlib/lean-mathlib-0.1_p20220318.ebuild
+++ /dev/null
@@ -1,43 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-COMMIT="d04fff95f686d5c372f7895551c40e7fa683ed6b"
-
-DESCRIPTION="Lean mathematical components library"
-HOMEPAGE="https://github.com/leanprover-community/mathlib"
-SRC_URI="https://github.com/leanprover-community/mathlib/archive/${COMMIT}.tar.gz -> ${PF}.tar.gz"
-S="${WORKDIR}/mathlib-${COMMIT}"
-
-KEYWORDS="~amd64"
-LICENSE="Apache-2.0"
-SLOT="0"
-IUSE="test"
-
-RDEPEND=">=sci-mathematics/lean-3.41.0"
-DEPEND="
- ${RDEPEND}
- sci-mathematics/mathlib-tools
-"
-
-RESTRICT="!test? ( test )"
-
-src_configure() {
- leanpkg configure || die
-}
-
-src_compile() {
- leanpkg build || die
-}
-
-src_install() {
- dodoc -r docs/*
- rm -r docs || die
- insinto /usr/lib/lean/mathlib
- doins -r .
-}
-
-src_test() {
- leanpkg test || die
-}
^ permalink raw reply related [flat|nested] 7+ messages in thread
end of thread, other threads:[~2022-03-26 0:09 UTC | newest]
Thread overview: 7+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2022-03-26 0:09 [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/lean-mathlib/ Alessandro Barbieri
-- strict thread matches above, loose matches on Subject: below --
2022-03-26 0:09 Alessandro Barbieri
2022-03-19 2:02 Alessandro Barbieri
2021-12-01 19:50 Andrew Ammerlaan
2021-10-24 14:53 Arthur Zamarin
2021-10-23 5:11 Alessandro Barbieri
2021-10-22 0:46 Alessandro Barbieri
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox