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: update System.FilePath.parent to handle edge cases for absolute paths #3645

Merged
merged 3 commits into from
Mar 26, 2024
Merged

fix: update System.FilePath.parent to handle edge cases for absolute paths #3645

merged 3 commits into from
Mar 26, 2024

Conversation

austinletson
Copy link
Contributor

@austinletson austinletson commented Mar 10, 2024 •
edited
Loading

System.FilePath.parent did not return the correct parent path in the case of absolute file paths

Example of previous behavior

(FilePath.mk "/foo").parent -> some (FilePath.mk "")

(System.FilePath.mk "/").parent -> some (FilePath.mk "")

The new behavior is based on rust's std::path::Path::parent function (as previously described in comment in System.FilePath)

Example of updated behavior

(System.FilePath.mk "/foo").parent -> some (FilePath.mk "/")

(System.FilePath.mk "/").parent -> none

Behavior for relative file paths is unchanged

Closes #3618

@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 10, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-10 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-10 19:09:19)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80d2455b6401acf6b0d107388b814c175e64c0d3 --onto 655ec964f5d6b0810ce0e517a6b3bbb3d5186d25. (2024-03-24 23:07:46)
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 00:51:12) View Log
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 01:30:01) View Log
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 05:49:55) View Log
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 16:19:47) View Log
  • 🟡 Mathlib branch lean-pr-testing-3645 build against this PR was cancelled. (2024-03-25 18:36:00) View Log
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 19:40:58) View Log
  • ✅ Mathlib branch lean-pr-testing-3645 has successfully built against this PR. (2024-03-25 21:29:33) View Log

@austinletson
Copy link
Contributor Author

I created this PR as draft since the relevant issue #3618 has not been approved by a maintainer

@austinletson
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Mar 10, 2024
@kim-em kim-em marked this pull request as ready for review March 22, 2024 00:05
@kim-em kim-em added the will-merge-soon …unless someone speaks up label Mar 22, 2024
@kim-em
Copy link
Collaborator

kim-em commented Mar 24, 2024

@austinletson, would you mind rebasing onto master (nightly-with-mathlib is fine too)? We can get this merged.

@austinletson
fix: update System.FilePath.parent to handle edge cases for absolute …
3950f46 
…file paths

System.FilePath.parent did not return the correct parent path in the case of absolute file paths
Example of previous behavior
```
(FilePath.mk "/foo").parent -> some (FilePath.mk "")

(System.FilePath.mk "/").parent -> some (FilePath.mk "")
```

The new behavior is based on rust's std::path::Path::parent function (as previously described in System.FilePath)

Example of new behavior after these changes
```
(System.FilePath.mk "/foo").parent -> some (FilePath.mk "/")

(System.FilePath.mk "/").parent -> none
```

Behavior for relative file paths is unchanged

Closes leanprover#3618
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 24, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3645
681fe6a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 24, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3645
3bb8c40
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
e5e99fd
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
0040d73
@austinletson
Copy link
Contributor Author

@semorrison I have rebased and Mathlib CI has passed. Is there anything else I need to do for this to be merged?

@kim-em kim-em added this pull request to the merge queue Mar 25, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 25, 2024
@kim-em
Copy link
Collaborator

kim-em commented Mar 25, 2024

@austinletson, there is a test failure on Windows. Could you take a look?

@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed will-merge-soon …unless someone speaks up labels Mar 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
ce7ad59
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
4d2c6a6
@kim-em kim-em added the full-ci label Mar 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
d47cf22
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
97d6c38
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
acd0fc8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
b67f479
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
cacaf71
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
bdf4bdb
@austinletson
Copy link
Contributor Author

austinletson commented Mar 25, 2024 •
edited
Loading

@semorrison I fixed the failing tests on Windows and added additional tests specifically for Windows for completeness.

I believe all CI is passing now. Let me know if there is anything else needed to add this to the merge queue.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
c127aa4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3645
96a27a7
@kim-em kim-em added this pull request to the merge queue Mar 26, 2024
Merged via the queue into leanprover:master with commit 83369f3 Mar 26, 2024
20 checks passed
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
awaiting-author Waiting for PR author to address issues awaiting-review Waiting for someone to review the PR 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
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

System.FilePath.parent bug at root
3 participants
@austinletson @leanprover-community-mathlib4-bot @kim-em