Skip site navigation (1)Skip section navigation (2)
Date:      Sun, 31 Oct 2021 17:23:27 GMT
From:      Yuri Victorovich <yuri@FreeBSD.org>
To:        ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org
Subject:   git: 02cc8aec8fb7 - main - math/lean: Update 3.33.0 -> 3.35.0
Message-ID:  <202110311723.19VHNRX5020124@gitrepo.freebsd.org>

next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=02cc8aec8fb73007cf609118a6dd981b1e8c40db

commit 02cc8aec8fb73007cf609118a6dd981b1e8c40db
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2021-10-31 16:57:34 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2021-10-31 17:23:17 +0000

    math/lean: Update 3.33.0 -> 3.35.0
    
    Reported by:    portscout
---
 math/lean/Makefile                   |  6 ++++-
 math/lean/distinfo                   |  8 ++++---
 math/lean/files/patch-CMakeLists.txt | 44 ------------------------------------
 math/lean/files/patch-util_path.cpp  | 14 ------------
 math/lean/pkg-plist                  | 12 ----------
 5 files changed, 10 insertions(+), 74 deletions(-)

diff --git a/math/lean/Makefile b/math/lean/Makefile
index 53a97b8fd6e5..101bfada5d21 100644
--- a/math/lean/Makefile
+++ b/math/lean/Makefile
@@ -1,8 +1,11 @@
 PORTNAME=	lean
 DISTVERSIONPREFIX=	v
-DISTVERSION=	3.33.0
+DISTVERSION=	3.35.0
 CATEGORIES=	math
 
+PATCH_SITES=	https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/
+PATCHFILES=	aba9d05dd1c725ec0a681aaec4a391554325a51b.patch:-p2 # FreeBSD patches: https://github.com/leanprover-community/lean/pull/643
+
 MAINTAINER=	yuri@FreeBSD.org
 COMMENT=	Theorem prover
 
@@ -12,6 +15,7 @@ LICENSE_FILE=	${WRKSRC}/../LICENSE
 LIB_DEPENDS=	libgmp.so:math/gmp
 
 USES=		cmake compiler:c++11-lang
+
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover-community
 
diff --git a/math/lean/distinfo b/math/lean/distinfo
index a15f89a7fb6e..63d0e9a472d5 100644
--- a/math/lean/distinfo
+++ b/math/lean/distinfo
@@ -1,3 +1,5 @@
-TIMESTAMP = 1631983261
-SHA256 (leanprover-community-lean-v3.33.0_GH0.tar.gz) = bb9b4cc1a6516726433f51d181c5089ba1eb20c2e08dc7c48c9bd862008d4003
-SIZE (leanprover-community-lean-v3.33.0_GH0.tar.gz) = 1890511
+TIMESTAMP = 1635697714
+SHA256 (leanprover-community-lean-v3.35.0_GH0.tar.gz) = 91d324089cdecff72de6a023605caece2732ed6d25f290b43aced95eef7b1a42
+SIZE (leanprover-community-lean-v3.35.0_GH0.tar.gz) = 1872221
+SHA256 (aba9d05dd1c725ec0a681aaec4a391554325a51b.patch) = 8595820a0dd31f62ebc26d5b98c5b8d3499db0b4c12d405229ba914f36bbad8f
+SIZE (aba9d05dd1c725ec0a681aaec4a391554325a51b.patch) = 2477
diff --git a/math/lean/files/patch-CMakeLists.txt b/math/lean/files/patch-CMakeLists.txt
deleted file mode 100644
index 1796f7cbca64..000000000000
--- a/math/lean/files/patch-CMakeLists.txt
+++ /dev/null
@@ -1,44 +0,0 @@
---- CMakeLists.txt.orig	2020-07-08 16:29:47 UTC
-+++ CMakeLists.txt
-@@ -179,7 +179,7 @@ endif()
- 
- if(STATIC)
-   message(STATUS "Creating a static executable")
--  if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux")
-+  if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly")
-     set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--whole-archive -lpthread -lrt -Wl,--no-whole-archive")
-   endif()
-   set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static")
-@@ -212,7 +212,7 @@ endif()
- 
- # SPLIT_STACK
- if (SPLIT_STACK)
--  if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
-+  if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
-      set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fsplit-stack -D LEAN_USE_SPLIT_STACK")
-      message(STATUS "Using split-stacks")
-   else()
-@@ -299,13 +299,7 @@ else()
- endif()
- 
- # DL
--if (EMSCRIPTEN)
--    # no dlopen
--elseif((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
--  # TODO(Jared): config dlopen windows support
--else()
--  set(EXTRA_LIBS ${EXTRA_LIBS} dl)
--endif()
-+set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
- 
- # TRACK_MEMORY_USAGE
- if(TRACK_MEMORY_USAGE)
-@@ -568,7 +562,7 @@ if(NOT (${GIT_SHA1} MATCHES "GITDIR-NOTFOUND"))
-   set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION}.git${GIT_SHA1}")
- endif()
- set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}")
--if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
-+if(${CMAKE_SYSTEM_NAME} MATCHES "Linux|.*BSD|DragonFly")
-   SET(CPACK_GENERATOR TGZ)
- else()
-   SET(CPACK_GENERATOR ZIP)
diff --git a/math/lean/files/patch-util_path.cpp b/math/lean/files/patch-util_path.cpp
deleted file mode 100644
index 2ea9fd1d73cb..000000000000
--- a/math/lean/files/patch-util_path.cpp
+++ /dev/null
@@ -1,14 +0,0 @@
---- util/path.cpp.orig	2018-07-22 05:22:25 UTC
-+++ util/path.cpp
-@@ -82,7 +82,11 @@ std::string get_exe_location() {
-     char dest[PATH_MAX];
-     memset(dest, 0, PATH_MAX);
-     pid_t pid = getpid();
-+#if defined(__FreeBSD__)
-+    snprintf(path, PATH_MAX, "/proc/%d/file", pid);
-+#else
-     snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
-+#endif
-     if (readlink(path, dest, PATH_MAX) == -1) {
-         throw exception("failed to locate Lean executable location");
-     } else {
diff --git a/math/lean/pkg-plist b/math/lean/pkg-plist
index e57ddc87fa83..855276ded98d 100644
--- a/math/lean/pkg-plist
+++ b/math/lean/pkg-plist
@@ -401,14 +401,6 @@ lib/lean/leanpkg/leanpkg/toml.lean
 lib/lean/library/data/buffer.lean
 lib/lean/library/data/buffer/parser.lean
 lib/lean/library/data/dlist.lean
-lib/lean/library/data/rbmap/default.lean
-lib/lean/library/data/rbtree/basic.lean
-lib/lean/library/data/rbtree/default.lean
-lib/lean/library/data/rbtree/find.lean
-lib/lean/library/data/rbtree/insert.lean
-lib/lean/library/data/rbtree/main.lean
-lib/lean/library/data/rbtree/min_max.lean
-lib/lean/library/data/stream.lean
 lib/lean/library/data/vector.lean
 lib/lean/library/init/algebra/classes.lean
 lib/lean/library/init/algebra/default.lean
@@ -471,10 +463,6 @@ lib/lean/library/init/data/ordering/lemmas.lean
 lib/lean/library/init/data/prod.lean
 lib/lean/library/init/data/punit.lean
 lib/lean/library/init/data/quot.lean
-lib/lean/library/init/data/rbmap/basic.lean
-lib/lean/library/init/data/rbmap/default.lean
-lib/lean/library/init/data/rbtree/basic.lean
-lib/lean/library/init/data/rbtree/default.lean
 lib/lean/library/init/data/repr.lean
 lib/lean/library/init/data/set.lean
 lib/lean/library/init/data/setoid.lean



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202110311723.19VHNRX5020124>