lean4: handle rpaths in lean compiler/build system

To: pkgsrc-wip-changes%NetBSD.org@localhost
Subject: lean4: handle rpaths in lean compiler/build system
From: Thomas Klausner (via pkgsrc-wip) <commit-notify%pkgsrc.org@localhost>
Date: Fri, 24 Jul 2026 18:29:20 +0000
Module Name:	pkgsrc-wip
Committed By:	Thomas Klausner <wiz%NetBSD.org@localhost>
Pushed By:	wiz
Date:		Fri Jul 24 19:32:04 2026 +0200
Changeset:	420766a0de51a69ce467dfb49b91ab1c12ddcd07

Modified Files:
	lean4/Makefile
	lean4/distinfo
Added Files:
	lean4/patches/patch-src_Leanc.lean
	lean4/patches/patch-src_lake_Lake_Build_Common.lean

Log Message:
lean4: handle rpaths in lean compiler/build system

Define C++ standard used, use CMake variables instead of manual
post-installation rule. Depend on required gmp version.

To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=420766a0de51a69ce467dfb49b91ab1c12ddcd07

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

diffstat:
 lean4/Makefile                                     | 21 ++++++++++++--
 lean4/distinfo                                     |  2 ++
 lean4/patches/patch-src_Leanc.lean                 | 14 ++++++++++
 .../patches/patch-src_lake_Lake_Build_Common.lean  | 32 ++++++++++++++++++++++
 4 files changed, 66 insertions(+), 3 deletions(-)

diffs:
diff --git a/lean4/Makefile b/lean4/Makefile
index 118f5d2ae0..03b6d4e7ed 100644
--- a/lean4/Makefile
+++ b/lean4/Makefile
@@ -17,6 +17,8 @@ DEPENDS+=	cadical-[0-9]*:../../wip/cadical
 USE_LANGUAGES=	c c++
 USE_TOOLS+=	bash:run gmake pkg-config
 
+USE_CXX_FEATURES=	c++20
+
 # needed for stage0 tools that are called during build and installation
 MAKE_ENV+=	LD_LIBRARY_PATH=${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib/lean:${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib
 INSTALL_ENV+=	LD_LIBRARY_PATH=${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib/lean:${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib
@@ -27,6 +29,10 @@ CMAKE_CONFIGURE_ARGS+=	-DUSE_MIMALLOC=no
 # stage0/stage1 options need to be passed explicitly
 CMAKE_CONFIGURE_ARGS+=	-DSTAGE0_CMAKE_PREFIX_PATH=${BUILDLINK_DIR}
 CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_CMAKE_INSTALL_PREFIX=${PREFIX}
+# not install these binaries, they are dependencies
+CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_INSTALL_CADICAL=OFF
+CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_INSTALL_LEANTAR=OFF
+
 # LDFLAGS from environment are ignored
 CMAKE_CONFIGURE_ARGS+=	-DTOOLCHAIN_SHARED_LINKER_FLAGS=${LDFLAGS:Q}
 
@@ -35,16 +41,25 @@ LDFLAGS+=	${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean
 REPLACE_BASH+=	src/bin/leanmake
 REPLACE_BASH+=	stage0/src/bin/leanmake
 
-# as of 4.32.1: "Only makefile generators are supported"
+# avoid pkgsrc cwrapper cc in installed file
+SUBST_CLASSES+=		cc
+SUBST_FILES.cc+=	src/Leanc.lean
+SUBST_FILES.cc+=	src/lake/Lake/Build/Common.lean
+SUBST_SED.cc+=		-e "s,@LEANC_CC@,${CC},"
+SUBST_SED.cc+=		-e "s!@LINKER_FLAGS@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\"!"
+SUBST_STAGE.cc=		pre-configure
+SUBST_MESSAGE.cc=	Setting compiler path.
+
+# CMakeLists.txt: "Only makefile generators are supported"
 CMAKE_GENERATORS_INCOMPATIBLE=	ninja
 
 post-install:
-	${RM} ${DESTDIR}${PREFIX}/bin/cadical
-	${RM} ${DESTDIR}${PREFIX}/bin/leantar
 	${MV} ${DESTDIR}${PREFIX}/LICENSE* ${DESTDIR}${PREFIX}/share/lean4
+	${CHMOD} a+x ${DESTDIR}${PREFIX}/lib/lean/*.so
 
 .include "../../devel/cmake/build.mk"
 .include "../../devel/libuv/buildlink3.mk"
+BUILDLINK_API_DEPENDS.gmp+=	gmp>=5.0.5
 .include "../../devel/gmp/buildlink3.mk"
 .include "../../security/openssl/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/lean4/distinfo b/lean4/distinfo
index a818b8fc1d..f0e7de3714 100644
--- a/lean4/distinfo
+++ b/lean4/distinfo
@@ -4,6 +4,8 @@ BLAKE2s (lean4-4.32.1.tar.gz) = 9d98b0fcb0d958bdbbe110d108c6138c5e6f9c3e335dd160
 SHA512 (lean4-4.32.1.tar.gz) = c180c406c6d9b6c28705f93ac3fad64b1a975f76cc11ae8ba2b4447ff668e2babac2bf3dd997bae2a38b196767353b484b1674a6a21a145e9a37dc3879d3029f
 Size (lean4-4.32.1.tar.gz) = 75094335 bytes
 SHA1 (patch-src_CMakeLists.txt) = 055656efbe3796c5948f59da8f6709ac68ba9d66
+SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
+SHA1 (patch-src_lake_Lake_Build_Common.lean) = 2fd83850d22ba26beb56b8bd26bb3473b897aee8
 SHA1 (patch-src_runtime_process.cpp) = 4a4723d9f69046d51ad351dff20120db0e1b40f9
 SHA1 (patch-stage0_src_CMakeLists.txt) = 5a7a307617e1ca566c0cec698c308588edd3ceda
 SHA1 (patch-stage0_src_runtime_process.cpp) = 18f705c5f58a2a60d98930a0ff59baf49b522bdd
diff --git a/lean4/patches/patch-src_Leanc.lean b/lean4/patches/patch-src_Leanc.lean
new file mode 100644
index 0000000000..f6c5fce888
--- /dev/null
+++ b/lean4/patches/patch-src_Leanc.lean
@@ -0,0 +1,14 @@
+$NetBSD$
+
+Provide anchor for SUBST_SED, to provide rpath flags.
+
+--- src/Leanc.lean.orig	2026-07-22 17:50:04.000000000 +0000
++++ src/Leanc.lean
+@@ -41,6 +41,7 @@ Interesting options:
+   let mut cflagsInternal := getInternalCFlags root
+   let mut ldflagsInternal := getInternalLinkerFlags root
+   let mut ldflags := getLinkerFlags root linkStatic
++  ldflags := ldflags ++ #[@LINKER_FLAGS@]
+   if System.Platform.isWindows && !args.contains "-shared" then
+     ldflags := ldflags ++ #["-Wl,--whole-archive", "-lleanmanifest", "-Wl,--no-whole-archive"]
+ 
diff --git a/lean4/patches/patch-src_lake_Lake_Build_Common.lean b/lean4/patches/patch-src_lake_Lake_Build_Common.lean
new file mode 100644
index 0000000000..245edc01b7
--- /dev/null
+++ b/lean4/patches/patch-src_lake_Lake_Build_Common.lean
@@ -0,0 +1,32 @@
+$NetBSD$
+
+Use linker flags during linking (for rpath).
+
+--- src/lake/Lake/Build/Common.lean.orig	2026-07-22 17:50:04.000000000 +0000
++++ src/lake/Lake/Build/Common.lean
+@@ -930,7 +930,7 @@ public def buildSharedLib
+     -- and thus need to copied from the cache with that name
+     let art ← buildArtifactUnlessUpToDate libFile (ext := sharedLibExt) (restore := true) do
+       let libs ← if linkDeps then mkLinkOrder libs else pure #[]
+-      let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs
++      let args := mkLinkObjArgs objs libs ++ #[@LINKER_FLAGS@] ++ weakArgs ++ traceArgs
+       compileSharedLib libFile args linker
+     return {name := libName, path := art.path, deps := libs, plugin}
+ 
+@@ -955,7 +955,7 @@ public def buildLeanSharedLib
+       let lean ← getLeanInstall
+       let libs ← if linkDeps then mkLinkOrder libs else pure #[]
+       let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
+-        #["-L", lean.leanLibDir.toString] ++ lean.ccLinkSharedFlags
++        #["-L", lean.leanLibDir.toString] ++ #[@LINKER_FLAGS@] ++ lean.ccLinkSharedFlags
+       compileSharedLib libFile args lean.cc
+     return {name := libName, path := art.path, deps := libs, plugin}
+ 
+@@ -977,6 +977,6 @@ public def buildLeanExe
+       let lean ← getLeanInstall
+       let libs ← mkLinkOrder libs
+       let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
+-        #["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
++        #["-L", lean.leanLibDir.toString] ++ #[@LINKER_FLAGS@] ++ lean.ccLinkFlags sharedLean
+       compileExe exeFile args lean.cc
+     return art.path
Prev by Date: lean4: avoid conflict with leantar
Next by Date: cadical, leantar, lean4: remove, imported to pkgsrc
Previous by Thread: lean4: avoid conflict with leantar
Next by Thread: cadical, leantar, lean4: remove, imported to pkgsrc
Indexes:
Home | Main Index | Thread Index | Old Index