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


1.2
date	2026.08.11.12.55.48;	author wiz;	state Exp;
branches;
next	1.1;
commitid	0E2cLSa8fQuPGdRG;

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


desc
@@


1.2
log
@lean4: update to 4.33.0.

Lean 4.33.0 concentrates on responsiveness and consolidation: the
editor keeps more of your work while you type, try? can propose
proofs on its own, lia and grind tactics are improved, and Float
stops being an opaque type. Continuing the transparency work of
v4.31.0, it also enables backward.isDefEq.respectTransparency.types
by default — the change most likely to need attention when porting.
@
text
@$NetBSD: patch-src_lake_Lake_Build_Common.lean,v 1.1 2026/07/24 18:39:20 wiz Exp $

Use linker flags during linking (for rpath).

--- src/lake/Lake/Build/Common.lean.orig	2026-08-03 09:21:21.000000000 +0000
+++ src/lake/Lake/Build/Common.lean
@@@@ -937,7 +937,7 @@@@ -/
 : JobM (Array String) := do
   let lean ← getLeanInstall
   let baseArgs ← mkLinkArgs objs libs linkDeps
-  return baseArgs ++ args ++ #["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
+  return baseArgs ++ args ++ #["-L", lean.leanLibDir.toString] ++ #[@@LINKER_FLAGS@@] ++ lean.ccLinkFlags sharedLean
 
 /--
 Build a shared library using `linker`.
@


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
@d1 1
a1 1
$NetBSD$
d5 1
a5 1
--- src/lake/Lake/Build/Common.lean.orig	2026-07-22 17:50:04.000000000 +0000
d7 6
a12 8
@@@@ -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}
d14 2
a15 17
@@@@ -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
@