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.

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

feat: skip defeq check for synport #187

Merged
merged 2 commits into from Oct 22, 2022
Merged

feat: skip defeq check for synport #187

merged 2 commits into from Oct 22, 2022

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Oct 14, 2022

This solves the issue of in all the definitions, as well as significantly improving the performance of synport. You probably want to keep the skipDefEq option off if you are using the Mathbin compiled olean files, but for synport it's just a waste of cycles to check defeqs when we are often explicitly interested in breaking these defeqs in practice.

Fixes #170

@digama0 digama0 force-pushed the defeq_synport branch 6 times, most recently from a3d1c39 to aee0df7 Compare October 16, 2022 09:48
@gebner
Copy link
Member

gebner commented Oct 19, 2022

You probably want to keep the skipDefEq option off if you are using the Mathbin compiled olean files

Everyone uses the default releases though, so if we enable skipDefEq then they'll have to take it.

Personally, I think we can drop import Mathbin support if this helps with the port. But I just want us to be clear that we are dropping it.

@digama0 digama0 merged commit 8695123 into master Oct 22, 2022
@digama0 digama0 deleted the defeq_synport branch October 22, 2022 02:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

remove ₓ
2 participants