mirror of
https://github.com/gentoo-mirror/guru.git
synced 2026-07-10 07:33:19 -04:00
sci-mathematics/lean-mathlib: add 0.1_p20220318
Signed-off-by: Alessandro Barbieri <lssndrbarbieri@gmail.com>
This commit is contained in:
@@ -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
|
||||
|
||||
@@ -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
|
||||
}
|
||||
Reference in New Issue
Block a user