[edemaine]

Remove the explicit -lLake overrides from mk_all and lint-style. On Windows, I found both executables to otherwise fail when loading a Lake workspace, with message:

error: invalid environment extension, 'Lake.packageAttr' has already been used
uncaught exception: failed to load Lake workspace

The Lean toolchain specified in Mathlib’s lean-toolchain file already supplies -lLake -lLeanExport for static linking and -lLake_shared for shared linking (source). Removing the overrides lets Lake select the matching static or shared libraries.

The regression came from Lean #14885, which added a LeanExport dependency to Lake. With the explicit static -lLake, unresolved LeanExport initializers are taken from libLake_shared.dll, loading a second copy of Lake and duplicating initialization. Previously the unused DLL was omitted. Lean #14963 added -lLeanExport to the automatic static flags, but Windows interpreter executables use the shared flags, so Mathlib's explicit override still causes this mixture. The old overrides originated in Mathlib #13850.

---

Validation on Windows with Lean 4.36.0-rc1:

• lake --no-cache build mk_all lint-style
• lake exe mk_all --check
• lake exe lint-style
• git diff --check

A standalone reproducer also passes on the August 27, 2026 nightly and produces the exact error on the August 28 nightly. Removing -lLake fixes both that nightly and toolchains 4.35.0 and 4.36.0-rc1. Adding static -lLeanExport also removes the DLL dependency and fixes the reproducer, confirming the dependency mechanism. Linux/macOS flag selection was checked in the toolchain source, not run locally.

AI assistance: Codex investigated the regression, ran the reproductions, prepared the patch, and drafted this description.

As a side note, perhaps we should consider adding Windows CI to prevent such regression in the future. Let me know if you'd like a PR.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary 2f0dccbd5c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2f0dccb).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 2f0dccbd5c
Reference commit 3d14fd9a31

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job