-
Notifications
You must be signed in to change notification settings - Fork 36
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.
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
Remove Unicode dependency to avoid large downloads for mathlib4 users #112
Conversation
charInGeneralCategory c GeneralCategory.punctuation || | ||
charInGeneralCategory c GeneralCategory.separator || | ||
charInGeneralCategory c GeneralCategory.other | ||
false -- TODO: restore the behavior described in the docstring |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
c == " "
is probably a marginally better choice
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure, go for it then 👍
Do you want to make the mentioned change in the comment or shall I go ahead and merge it? |
CI fails so I would recommend against merging this! |
Oh I was thinking this is just the usual CI fail from mathlib4 and std4 incompatability /o\ |
b910c11
to
0c41523
Compare
Isn't this mostly fixed by 5f59fba |
It's definitely a great improval yes, I'll close the PR for now. |
Until
lake
learns to not download this, I would claim that the benefit of marginally-nicer URLs is not worth the cost of having every mathlib4 user download a large archive of unicode data.