Skip to content

Conversation

@tydeu
Copy link
Member

@tydeu tydeu commented Sep 26, 2025

This PR alters libPrefixOnWindows behavior to add the lib prefix to the library's libName rather than just the file path. This means that Lake's -l will now have the prefix on Windows. While this should not matter to a MSYS2 build (which accepts both lib-prefixed and unprefixed variants), it should ensure compatibility with MSVC (if that is ever an issue).

@tydeu tydeu added release-ci Enable all CI checks for a PR, like is done for releases changelog-lake Lake labels Sep 26, 2025
@tydeu tydeu force-pushed the lake/win-lib-prefix-name branch from b52b1da to 4e51663 Compare September 26, 2025 22:37
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 27, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 00:03:03)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-27 00:03:05)

@tydeu tydeu marked this pull request as ready for review September 27, 2025 00:56
@tydeu tydeu added this pull request to the merge queue Sep 27, 2025
Merged via the queue into leanprover:master with commit f80d6e7 Sep 27, 2025
21 checks passed
@tydeu tydeu deleted the lake/win-lib-prefix-name branch September 27, 2025 02:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants