Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

fix: make .lean hashes cross-platform/autocrlf compatible #170

Merged
merged 1 commit into from
May 23, 2023

Conversation

Kha
Copy link
Member

@Kha Kha commented May 21, 2023

This is the Lake equivalent of leanprover-community/mathlib4#3096, needed for mathlib4's caching implementation

@tydeu
Copy link
Member

tydeu commented May 21, 2023

@Kha I imagine the reason you did not just change computeFileHash directly is because that is doing binary hashing and this optimization should only apply to text files? In that case, maybe we should just call the wrapper TextFilePath? Does that seem reasonable / am I understanding correctly?

@tydeu tydeu added the enhancement New feature or request label May 21, 2023
@Kha
Copy link
Member Author

Kha commented May 22, 2023

Yes, exactly. TextFilePath is fine as well, sure.

@Kha
Copy link
Member Author

Kha commented May 22, 2023

I haven't touched other functions such as inputFile since this issue is quite specific to mathlib caching

@tydeu tydeu merged commit 5a8f71c into leanprover:master May 23, 2023
4 checks passed
@tydeu
Copy link
Member

tydeu commented May 23, 2023

Looks good to me. Merged.

@Kha
Copy link
Member Author

Kha commented May 24, 2023

Oops, committing flake.lock was not intended. Let's continue the talks about merging lake into lean4 soon so I don't have to worry about that anymore 😄 .

tydeu added a commit that referenced this pull request May 24, 2023
@tydeu
Copy link
Member

tydeu commented May 24, 2023

@Kha Fixed. 😄

Kha added a commit to Kha/lean4 that referenced this pull request Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this pull request Jul 17, 2023
Kha added a commit to Kha/lean4 that referenced this pull request Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this pull request Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants