From b206aa4fe3a4c1c45600674a0a55626d80014e19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@riseup.net>
Date: Tue, 19 Oct 2021 23:41:00 +0200
Subject: [PATCH] dev-lang/lean: add version 3.33.0
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Package-Manager: Portage-3.0.20, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@riseup.net>
---
 dev-lang/lean/Manifest           |  1 +
 dev-lang/lean/lean-3.33.0.ebuild | 45 ++++++++++++++++++++++++++++++++
 dev-lang/lean/metadata.xml       | 20 ++++++++++++++
 3 files changed, 66 insertions(+)
 create mode 100644 dev-lang/lean/Manifest
 create mode 100644 dev-lang/lean/lean-3.33.0.ebuild
 create mode 100644 dev-lang/lean/metadata.xml

diff --git a/dev-lang/lean/Manifest b/dev-lang/lean/Manifest
new file mode 100644
index 0000000000..fd42aa380d
--- /dev/null
+++ b/dev-lang/lean/Manifest
@@ -0,0 +1 @@
+DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3
diff --git a/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild
new file mode 100644
index 0000000000..120a2ac2e7
--- /dev/null
+++ b/dev-lang/lean/lean-3.33.0.ebuild
@@ -0,0 +1,45 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+CMAKE_IN_SOURCE_BUILD="ON"
+
+inherit cmake
+
+DESCRIPTION="The Lean Theorem Prover"
+HOMEPAGE="https://leanprover-community.github.io/"
+
+if [[ "${PV}" == *9999* ]]; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
+else
+	SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
+	KEYWORDS="~amd64"
+fi
+S="${WORKDIR}/lean-${PV}/src"
+
+RESTRICT="!test? ( test )"
+LICENSE="Apache-2.0"
+SLOT="0"
+IUSE="+json test +threads"
+
+RDEPEND="dev-libs/gmp"
+DEPEND="${RDEPEND}"
+
+src_configure() {
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+		-DMULTI_THREAD=$(usex threads)
+		-DUSE_GITHASH=OFF
+	)
+	cmake_src_configure
+}
+
+pkg_postinst() {
+	elog "You probably want to use lean with mathlib, to install it use leanpkg."
+	elog "For example: leanpkg install https://github.com/leanprover-community/mathlib"
+}
diff --git a/dev-lang/lean/metadata.xml b/dev-lang/lean/metadata.xml
new file mode 100644
index 0000000000..9e03d53ade
--- /dev/null
+++ b/dev-lang/lean/metadata.xml
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="person">
+    <email>xgqt@riseup.net</email>
+    <name>Maciej Barć</name>
+  </maintainer>
+  <longdescription lang="en">
+    The Lean theorem prover is a proof assistant developed principally
+    by Leonardo de Moura at Microsoft Research.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/leanprover-community/lean/issues</bugs-to>
+    <remote-id type="github">leanprover-community/lean</remote-id>
+  </upstream>
+  <use>
+    <flag name="json"> Enable JSON support</flag>
+  </use>
+</pkgmetadata>