From nobody Sun Jan 14 03:50:22 2024 X-Original-To: dev-commits-ports-main@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4TCLrv0Jnhz56wdZ; Sun, 14 Jan 2024 03:50:23 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4TCLrv01p8z47ZM; Sun, 14 Jan 2024 03:50:23 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1705204223; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=0oOrrbeydAaT6ooE6W91HWTBI2DYRWsu7DQayYKo9wE=; b=Dq3ueCzS5R1de7UyEIEa5KKzYJb6xJ+DPJAClAn6dNwJ09OzWW4ZRmYymExrB8fIlEfMLP CbZT8Ujw56Xq50fmc6/+X4/c8jWnltlJyOTIbC2Rgue7p4AogCXzG2HBE2aXO01Btl8/Uk ef90RJc32TS8fGJF4mG8hr+4Karc+QLqHudHjfT/dz7aUK0y5FLTk2h5vh85slpZfc/brC kONirDa6RRpvah9ZqRCnSptJBS2SKKOBDjct5x42rAVQkHyLBQdkfA01MZSOK3OTtd6o7i IBJHsO/9xy4kofVF+T87PFngnqDxMpTORC8W9q79b8qIo9okwyAIs+zosAs2fQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1705204223; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=0oOrrbeydAaT6ooE6W91HWTBI2DYRWsu7DQayYKo9wE=; b=kuqv9YtEoRzQ1Exf6IxB+YGA28/zXe76ZJfR31Ru+i6rA1Dq7C/Mz/LN9sqLFV4Y2viK77 D5YcWbjUvgpz/yJ2JFmIpo1D2uPU5jbLCCMV/bpz/51oLtfjEYs60u7yIyLkjPe9qa/ydf Iru7YkDSPRo8+Zkpm8bfTWFKSnbNYcM+LZPOp+jXrj4u6VQ+fEqSlNKYVsd2rMABJETseQ NgVuiTJO/nM9JNnGI8pdp+L8rrKElHN1gX5vlA3IIP094XlamCPNMvgqj9Cj8cH3FAPrHD WJ0hZ0OLE7AHRi5vGpQhqEs3ebAvICn+FdmzMQLBlW7ls8MTP0KJPjrmL/33Fw== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1705204223; a=rsa-sha256; cv=none; b=mCvM2HUOPELgJEeMjeejlKhsIukwM1Pnm/iQ0dqpSpCz/W2kj5pHlHsHiun0u11vgGG7ne o4BMIkxQfnEoCI+afs0JWpOsAzsmoAFwhp67mZFhoybPzQ6He+gZCKU2JMVScJFIvfVp3l MKFiN2cvmI3EM5i3MTzhg3llJLo6kvx4tpYC8FuNRF/eMHkCNZIqOYOL/DT5DSfQGpZqj5 AFTcCOiwJqhZFZQiR+OgCv1IfQpxrTMemlasO7gLVTW/GwkFs61H1jrWSulvHpODQalOG0 WZNNat6vKZNDlLK9+CwZ88MuOCwBwIu6slIwOqLmQUZX2EEIC795JkzP97UDTA== Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 4TCLrt6BCVzxq3; Sun, 14 Jan 2024 03:50:22 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from gitrepo.freebsd.org ([127.0.1.44]) by gitrepo.freebsd.org (8.17.1/8.17.1) with ESMTP id 40E3oMsL022385; Sun, 14 Jan 2024 03:50:22 GMT (envelope-from git@gitrepo.freebsd.org) Received: (from git@localhost) by gitrepo.freebsd.org (8.17.1/8.17.1/Submit) id 40E3oMx4022382; Sun, 14 Jan 2024 03:50:22 GMT (envelope-from git) Date: Sun, 14 Jan 2024 03:50:22 GMT Message-Id: <202401140350.40E3oMx4022382@gitrepo.freebsd.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: 27b9012337ee - main - math/lean4: New port: Theorem prover and functional language for math (new gen) List-Id: Commits to the main branch of the FreeBSD ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-main List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-dev-commits-ports-main@freebsd.org X-BeenThere: dev-commits-ports-main@freebsd.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 27b9012337ee58a0ecc220dfd079cc2189dc99e2 Auto-Submitted: auto-generated The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=27b9012337ee58a0ecc220dfd079cc2189dc99e2 commit 27b9012337ee58a0ecc220dfd079cc2189dc99e2 Author: Yuri Victorovich AuthorDate: 2024-01-14 03:49:56 +0000 Commit: Yuri Victorovich CommitDate: 2024-01-14 03:50:20 +0000 math/lean4: New port: Theorem prover and functional language for math (new gen) --- math/Makefile | 1 + math/lean4/Makefile | 40 + math/lean4/distinfo | 3 + math/lean4/files/patch-src_CMakeLists.txt | 23 + math/lean4/files/patch-src_runtime_io.cpp | 17 + .../files/patch-src_runtime_stack__overflow.cpp | 12 + math/lean4/files/patch-stage0_src_CMakeLists.txt | 23 + math/lean4/files/patch-stage0_src_runtime_io.cpp | 16 + .../patch-stage0_src_runtime_stack__overflow.cpp | 21 + math/lean4/pkg-descr | 6 + math/lean4/pkg-message | 22 + math/lean4/pkg-plist | 2259 ++++++++++++++++++++ 12 files changed, 2443 insertions(+) diff --git a/math/Makefile b/math/Makefile index 345406ce012f..a933bb237101 100644 --- a/math/Makefile +++ b/math/Makefile @@ -436,6 +436,7 @@ SUBDIR += lcalc SUBDIR += ldouble SUBDIR += lean + SUBDIR += lean4 SUBDIR += lemon SUBDIR += levmar SUBDIR += lib2geom diff --git a/math/lean4/Makefile b/math/lean4/Makefile new file mode 100644 index 000000000000..a43194860970 --- /dev/null +++ b/math/lean4/Makefile @@ -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 diff --git a/math/lean4/distinfo b/math/lean4/distinfo new file mode 100644 index 000000000000..d307f90be676 --- /dev/null +++ b/math/lean4/distinfo @@ -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 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt new file mode 100644 index 000000000000..6109d2793eac --- /dev/null +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -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" diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp new file mode 100644 index 000000000000..767ad0a1625f --- /dev/null +++ b/math/lean4/files/patch-src_runtime_io.cpp @@ -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 { diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp new file mode 100644 index 000000000000..06914304dbaa --- /dev/null +++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp @@ -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 + #include "runtime/stack_overflow.h" + ++#include ++#define pthread_getattr_np pthread_attr_get_np ++ + namespace lean { + // stack guard of the main thread + static stack_guard * g_stack_guard; diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt new file mode 100644 index 000000000000..e8af91b549aa --- /dev/null +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -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" diff --git a/math/lean4/files/patch-stage0_src_runtime_io.cpp b/math/lean4/files/patch-stage0_src_runtime_io.cpp new file mode 100644 index 000000000000..67d799f2a916 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_io.cpp @@ -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 { diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp new file mode 100644 index 000000000000..5296c0cf49c2 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -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 ++#define pthread_getattr_np pthread_attr_get_np ++ + #ifdef LEAN_WINDOWS + #include + #else +@@ -19,6 +23,7 @@ Port of the corresponding Rust code (see links below). + #include + #include + #include "runtime/stack_overflow.h" ++ + + namespace lean { + // stack guard of the main thread diff --git a/math/lean4/pkg-descr b/math/lean4/pkg-descr new file mode 100644 index 000000000000..d549a156950f --- /dev/null +++ b/math/lean4/pkg-descr @@ -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. diff --git a/math/lean4/pkg-message b/math/lean4/pkg-message new file mode 100644 index 000000000000..e0c1a26dc720 --- /dev/null +++ b/math/lean4/pkg-message @@ -0,0 +1,22 @@ +[ +{ type: install + message: <