git: 7584cbd4c081 - main - math/lean4: update 4.32.0 → 4.32.1

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Mon, 27 Jul 2026 01:37:00 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=7584cbd4c081ea400b419a38c85c112cbb6c63b2

commit 7584cbd4c081ea400b419a38c85c112cbb6c63b2
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2026-07-27 01:36:48 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2026-07-27 01:36:58 +0000

    math/lean4: update 4.32.0 → 4.32.1
---
 math/lean4/Makefile                                |  2 +-
 math/lean4/distinfo                                |  6 ++---
 math/lean4/files/patch-src_CMakeLists.txt          | 12 ++++-----
 math/lean4/files/patch-src_include_lean_lean.h     | 29 ++++++++++++++++++++++
 math/lean4/files/patch-src_runtime_object.cpp      |  2 +-
 math/lean4/files/patch-stage0_src_CMakeLists.txt   | 12 ++++-----
 .../files/patch-stage0_src_include_lean_lean.h     | 29 ++++++++++++++++++++++
 .../files/patch-stage0_src_runtime_object.cpp      |  2 +-
 8 files changed, 76 insertions(+), 18 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 2431721f6b2f..3402b4d2f4a8 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.32.0
+DISTVERSION=	4.32.1
 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
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 2af2d958e506..f98762b632d4 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1784011437
-SHA256 (leanprover-lean4-v4.32.0_GH0.tar.gz) = f39c6d87a9b4e9253bef15ffae460d2652b668e619688e4c01e59bbd2cd3b002
-SIZE (leanprover-lean4-v4.32.0_GH0.tar.gz) = 75094778
+TIMESTAMP = 1785103908
+SHA256 (leanprover-lean4-v4.32.1_GH0.tar.gz) = 5ee893d6081dba103c3d1206930a0637f9dd8afe3c631823b98a21593386dbd7
+SIZE (leanprover-lean4-v4.32.1_GH0.tar.gz) = 75094335
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index 5f9d89f2d38f..8098ed7948d6 100644
--- a/math/lean4/files/patch-src_CMakeLists.txt
+++ b/math/lean4/files/patch-src_CMakeLists.txt
@@ -1,6 +1,6 @@
---- src/CMakeLists.txt.orig	2026-06-13 21:32:55 UTC
+--- src/CMakeLists.txt.orig	2026-07-22 17:50:04 UTC
 +++ src/CMakeLists.txt
-@@ -395,7 +395,7 @@ endif()
+@@ -407,7 +407,7 @@ endif()
    endif()
  endif()
  
@@ -9,7 +9,7 @@
  
  # Pick up `llvm-config` to setup LLVM flags.
  if(LLVM)
-@@ -537,7 +537,7 @@ endif()
+@@ -549,7 +549,7 @@ endif()
    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm")
  endif()
  
@@ -18,7 +18,7 @@
    if(BSYMBOLIC)
      string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
      string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-@@ -550,6 +550,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+@@ -562,6 +562,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
      " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
    )
    string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
@@ -38,7 +38,7 @@
  elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
    string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
-@@ -708,6 +721,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
+@@ -720,6 +733,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
  # Lean code only needs this one include
  string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include")
  
@@ -48,7 +48,7 @@
  # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc`
  string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
  string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-@@ -1025,7 +1041,7 @@ install(
+@@ -1037,7 +1053,7 @@ install(
  
  install(
    DIRECTORY "${CMAKE_SOURCE_DIR}/"
diff --git a/math/lean4/files/patch-src_include_lean_lean.h b/math/lean4/files/patch-src_include_lean_lean.h
new file mode 100644
index 000000000000..85a25f0ea4ad
--- /dev/null
+++ b/math/lean4/files/patch-src_include_lean_lean.h
@@ -0,0 +1,29 @@
+--- src/include/lean/lean.h.orig	2026-07-22 17:50:04 UTC
++++ src/include/lean/lean.h
+@@ -17,6 +17,10 @@ Author: Leonardo de Moura
+ #include <lean/mimalloc.h>
+ #endif
+ 
++#if defined(__FreeBSD__)
++#include <sys/param.h>
++#endif
++
+ #ifdef __cplusplus
+ #include <atomic>
+ #include <stdlib.h>
+@@ -484,7 +488,15 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
+ void free_sized(void* ptr, size_t);
++#else
++#  ifdef __cplusplus
++void free_sized(void* ptr, size_t) throw();
++#  else
++void free_sized(void* ptr, size_t);
++#  endif
++#endif
+ #endif
+ 
+ static inline void lean_free_small_object(lean_object * o) {
diff --git a/math/lean4/files/patch-src_runtime_object.cpp b/math/lean4/files/patch-src_runtime_object.cpp
index c8a62465f1d7..df8a2d96b019 100644
--- a/math/lean4/files/patch-src_runtime_object.cpp
+++ b/math/lean4/files/patch-src_runtime_object.cpp
@@ -15,7 +15,7 @@
  // `__attribute__((nothrow))` to be present or `noexcept`.
  __attribute__((nothrow))
  #endif
-+#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
  __attribute__((weak)) void free_sized(void *ptr, size_t) {
 +#else
 +__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index 403d15edeaac..1b499230c8d4 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -1,6 +1,6 @@
---- stage0/src/CMakeLists.txt.orig	2026-06-13 21:32:55 UTC
+--- stage0/src/CMakeLists.txt.orig	2026-07-22 17:50:04 UTC
 +++ stage0/src/CMakeLists.txt
-@@ -395,7 +395,7 @@ endif()
+@@ -407,7 +407,7 @@ endif()
    endif()
  endif()
  
@@ -9,7 +9,7 @@
  
  # Pick up `llvm-config` to setup LLVM flags.
  if(LLVM)
-@@ -537,7 +537,7 @@ endif()
+@@ -549,7 +549,7 @@ endif()
    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm")
  endif()
  
@@ -18,7 +18,7 @@
    if(BSYMBOLIC)
      string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
      string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-@@ -550,6 +550,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+@@ -562,6 +562,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
      " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
    )
    string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
@@ -38,7 +38,7 @@
  elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
    string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
-@@ -708,6 +721,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
+@@ -720,6 +733,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu
  # Lean code only needs this one include
  string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include")
  
@@ -48,7 +48,7 @@
  # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc`
  string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
  string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-@@ -1025,7 +1041,7 @@ install(
+@@ -1037,7 +1053,7 @@ install(
  
  install(
    DIRECTORY "${CMAKE_SOURCE_DIR}/"
diff --git a/math/lean4/files/patch-stage0_src_include_lean_lean.h b/math/lean4/files/patch-stage0_src_include_lean_lean.h
new file mode 100644
index 000000000000..412f1f76568e
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_include_lean_lean.h
@@ -0,0 +1,29 @@
+--- stage0/src/include/lean/lean.h.orig	2026-07-22 17:50:04 UTC
++++ stage0/src/include/lean/lean.h
+@@ -17,6 +17,10 @@ Author: Leonardo de Moura
+ #include <lean/mimalloc.h>
+ #endif
+ 
++#if defined(__FreeBSD__)
++#include <sys/param.h>
++#endif
++
+ #ifdef __cplusplus
+ #include <atomic>
+ #include <stdlib.h>
+@@ -484,7 +488,15 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
+ void free_sized(void* ptr, size_t);
++#else
++#  ifdef __cplusplus
++void free_sized(void* ptr, size_t) throw();
++#  else
++void free_sized(void* ptr, size_t);
++#  endif
++#endif
+ #endif
+ 
+ static inline void lean_free_small_object(lean_object * o) {
diff --git a/math/lean4/files/patch-stage0_src_runtime_object.cpp b/math/lean4/files/patch-stage0_src_runtime_object.cpp
index ca40a370d5be..98de136bdefb 100644
--- a/math/lean4/files/patch-stage0_src_runtime_object.cpp
+++ b/math/lean4/files/patch-stage0_src_runtime_object.cpp
@@ -15,7 +15,7 @@
  // `__attribute__((nothrow))` to be present or `noexcept`.
  __attribute__((nothrow))
  #endif
-+#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1500000
  __attribute__((weak)) void free_sized(void *ptr, size_t) {
 +#else
 +__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {