Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: lake: check normalized packages directory path before rename #3795

Merged
merged 2 commits into from
Mar 29, 2024
Merged

fix: lake: check normalized packages directory path before rename #3795

merged 2 commits into from
Mar 29, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Mar 28, 2024 •
edited
Loading

Normalize the relative packages directory paths in the pre-rename check to avoid renames if the difference in paths is only in the path separators. Also adds a log message on rename.

Closes #3502.

@tydeu
Copy link
Member Author

tydeu commented Mar 28, 2024 •
edited
Loading

This builds on #3753 to fix a Windows error in Lake that has been occurring often on Zulip lately.

@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 Mar 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3795
fa9ca2d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3795
84693df
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3795
c80a46a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3795
18f2bd9
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 28, 2024 •
edited
Loading

Mathlib CI status (docs):

  • 🟡 Mathlib branch lean-pr-testing-3795 build against this PR was cancelled. (2024-03-28 00:51:40) View Log
  • ✅ Mathlib branch lean-pr-testing-3795 has successfully built against this PR. (2024-03-28 02:02:05) View Log
  • ✅ Mathlib branch lean-pr-testing-3795 has successfully built against this PR. (2024-03-28 02:44:21) View Log
  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-28 17:19:07)

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3795
8196bd6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3795
12f68b3
@tydeu tydeu force-pushed the lake/normalize-pkgs-dir branch from 99d98e9 to 6542ac6 Compare March 28, 2024 16:58
@tydeu tydeu marked this pull request as ready for review March 28, 2024 17:22
@tydeu tydeu added the will-merge-soon …unless someone speaks up label Mar 28, 2024
@tydeu tydeu added this pull request to the merge queue Mar 29, 2024
Merged via the queue into leanprover:master with commit e54a0d7 Mar 29, 2024
18 checks passed
@tydeu tydeu deleted the lake/normalize-pkgs-dir branch March 29, 2024 02:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Lake update error: could not rename package on Windows
2 participants
@tydeu @leanprover-community-mathlib4-bot