netbird/FreeBSD-ports
0
0
Fork 0
mirror of https://github.com/netbirdio/FreeBSD-ports.git synced 2026-05-22 18:42:42 -07:00
Code Issues Packages Projects Releases Wiki Activity

math/lean4: New port: Theorem prover and functional language for math (new gen)

Browse Source
This commit is contained in:
Yuri Victorovich
2024-01-13 19:50:20 -08:00
parent 2bf3db579d
commit 27b9012337
12 changed files with 2443 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
math/Makefile
+1
View File
@@ -436,6 +436,7 @@
SUBDIR += lcalc
SUBDIR += ldouble
SUBDIR += lean
SUBDIR += lean4
SUBDIR += lemon
SUBDIR += levmar
SUBDIR += lib2geom
math/lean4/Makefile
+40
View File
@@ -0,0 +1,40 @@
PORTNAME= lean4
DISTVERSIONPREFIX= v
DISTVERSION= 4.5.0-rc1
CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
MAINTAINER= yuri@FreeBSD.org
COMMENT= Theorem prover and functional language for math (new gen)
WWW= https://lean-lang.org/
LICENSE= APACHE20
LICENSE_FILE= ${WRKSRC}/LICENSE
BUILD_DEPENDS= bash:shells/bash
LIB_DEPENDS= libgmp.so:math/gmp
USES= cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project
USE_GITHUB= yes
GH_ACCOUNT= leanprover
CFLAGS+= -fPIC
CXXFLAGS+= -fPIC
BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD}
post-install:
# remove empty dirs
@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
# remove stray files
@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
# strip binaries
@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
bin/lake \
bin/lean \
bin/leanc \
lib/lean/libleanshared.so
# 6 tests are known to fail due to bugs in the testcase code, see https://github.com/leanprover/lean4/issues/3179
.include <bsd.port.mk>
math/lean4/distinfo
+3
View File
@@ -0,0 +1,3 @@
TIMESTAMP = 1705134061
SHA256 (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 8b5ae344816670adb2a68859b2f4c309592feb32674d477e46e061275f9e8129
SIZE (leanprover-lean4-v4.5.0-rc1_GH0.tar.gz) = 17060956
math/lean4/files/patch-src_CMakeLists.txt
+23
View File
@@ -0,0 +1,23 @@
--- src/CMakeLists.txt.orig 2023-12-21 22:11:33 UTC
+++ src/CMakeLists.txt
@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
+ string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
+ string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+ string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+ string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
@@ -592,7 +597,7 @@ endif()
file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
endif()
-install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean
+install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.md"
math/lean4/files/patch-src_runtime_io.cpp
+17
View File
@@ -0,0 +1,17 @@
--- src/runtime/io.cpp.orig 2024-01-13 17:13:25 UTC
+++ src/runtime/io.cpp
@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
char dest[PATH_MAX];
memset(dest, 0, PATH_MAX);
pid_t pid = getpid();
- snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+#if defined(__linux__)
+ snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+#elif defined(__FreeBSD__)
+ snprintf(path, PATH_MAX, "/proc/%d/file", pid);
+#else
+# error "Unknown platform"
+#endif
if (readlink(path, dest, PATH_MAX) == -1) {
return io_result_mk_error("failed to locate application");
} else {
math/lean4/files/patch-src_runtime_stack__overflow.cpp
+12
View File
@@ -0,0 +1,12 @@
--- src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC
+++ src/runtime/stack_overflow.cpp
@@ -20,6 +20,9 @@ Port of the corresponding Rust code (see links below).
#include <lean/lean.h>
#include "runtime/stack_overflow.h"
+#include <pthread_np.h>
+#define pthread_getattr_np pthread_attr_get_np
+
namespace lean {
// stack guard of the main thread
static stack_guard * g_stack_guard;
math/lean4/files/patch-stage0_src_CMakeLists.txt
+23
View File
@@ -0,0 +1,23 @@
--- stage0/src/CMakeLists.txt.orig 2023-12-21 22:11:33 UTC
+++ stage0/src/CMakeLists.txt
@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
+ string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
+ string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+ string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+ string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
@@ -592,7 +597,7 @@ endif()
file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
endif()
-install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean
+install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.md"
math/lean4/files/patch-stage0_src_runtime_io.cpp
+16
View File
@@ -0,0 +1,16 @@
--- stage0/src/runtime/io.cpp.orig 2024-01-13 09:36:50 UTC
+++ stage0/src/runtime/io.cpp
@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
char dest[PATH_MAX];
memset(dest, 0, PATH_MAX);
pid_t pid = getpid();
+#if defined(__linux__)
snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+#elif defined(__FreeBSD__)
+ snprintf(path, PATH_MAX, "/proc/%d/file", pid);
+#else
+# error "Unknown platform"
+#endif
if (readlink(path, dest, PATH_MAX) == -1) {
return io_result_mk_error("failed to locate application");
} else {
math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
+21
View File
@@ -0,0 +1,21 @@
--- stage0/src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC
+++ stage0/src/runtime/stack_overflow.cpp
@@ -7,6 +7,10 @@ Port of the corresponding Rust code (see links below).
Print a nicer error message on stack overflow.
Port of the corresponding Rust code (see links below).
*/
+
+#include <pthread_np.h>
+#define pthread_getattr_np pthread_attr_get_np
+
#ifdef LEAN_WINDOWS
#include <windows.h>
#else
@@ -19,6 +23,7 @@ Port of the corresponding Rust code (see links below).
#include <cstring>
#include <lean/lean.h>
#include "runtime/stack_overflow.h"
+
namespace lean {
// stack guard of the main thread
math/lean4/pkg-descr
+6
View File
@@ -0,0 +1,6 @@
Lean is an open source theorem prover and programming language being developed
at Microsoft Research. Lean aims to bridge the gap between interactive and
automated theorem proving, by situating automated tools and methods in a
framework that supports user interaction and the construction of fully specified
axiomatic proofs. The mathematical components library mathlib for Lean is being
developed at Carnegie Mellon University.
math/lean4/pkg-message
+22
View File
@@ -0,0 +1,22 @@
[
{ type: install
message: <<EOM
================================================================================
You installed Lean: The Theorem Prover.
(1) Please note that Lean requires /proc to be mounted.
The usual way to do this is to add this line to /etc/fstab:
proc /proc procfs rw 0 0
and then run this command as root:
# mount /proc
(2) You might also want to install mathlibtools (math/mathlibtools) in case
you need to use the mathematical library of Lean.
mathlibtools download this library to user's home directory for further
use by Lean.
================================================================================
EOM
}
]
math/lean4/pkg-plist
+2259
View File
File diff suppressed because it is too large Load Diff