chore: documentation for new Lake options (#883)

Documents new additions to Lake added in
github.com/leanprover/lean4/issues/14254

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>

Author: robsimmons

Manual/BuildTools/Lake.lean

@@ -488,6 +488,8 @@ module.ir
 module.ir.sig
 module.lean
 module.leanArts
+module.linkInfoExport
+module.linkInfoNoExport
 module.ltar
 module.o
 module.o.export
@@ -582,7 +584,7 @@ The facets available for modules are:
 
 : `c.o.noexport`
 
- The compiled object file, produced from the C file, with Lean symbols exported.
+ The compiled object file, produced from the C file, without Lean symbols exported.
 
 : `bc.o`
 
@@ -600,6 +602,14 @@ The facets available for modules are:
 
   A compressed archive (produced via `leantar`) of the module's build artifacts. {TODO}[Document `leantar` in the manual as well]
 
+: `linkInfoExport`
+
+  A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects have Lean symbols exported.
+
+: `linkInfoNoExport`
+
+  A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects do not Lean symbols exported.
+
 :::
 
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-07-02
+leanprover/lean4:nightly-2026-07-03