math/lean: Update 3.33.0 -> 3.35.0
Reported by: portscout
This commit is contained in:
parent
f6eca5725e
commit
02cc8aec8f
5 changed files with 10 additions and 74 deletions
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)
|
|
@ -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 {
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue