head	1.1;
access;
symbols;
locks; strict;
comment	@# @;


1.1
date	2026.07.24.18.39.20;	author wiz;	state Exp;
branches;
next	;
commitid	nN62qu9ZRD0EaWOG;


desc
@@


1.1
log
@math/lean4: import lean4-4.32.1

Lean is a proof assistant and a functional programming language.
It is based on the calculus of constructions with inductive types.
@
text
@$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
@