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
Updated version of #1822 #1851
Updated version of #1822 #1851
Conversation
Co-authored-by: Niels van der Weide <nnmvdw@gmail.com>
…nH/UniMath into small-obj-arg-contribution
…nH/UniMath into small-obj-arg-contribution
Merging this now without waiting for the macOS build. |
@DenSinH @nmvdw @benediktahrens merging this PR broke Coq CI (see for instance coq/coq#18713 that ran yesterday). The compilation of files UniMath/ModelCategories/Generated/LNWFSClosed.v and UniMath/ModelCategories/Generated/LNWFSClosed.v is very slow (multiple dozen minutes) and triggers the 1h timeout there. We are going to exclude package ModelCategories from Coq CI unless you have a better solution. |
I agree with your solution. We put ModelCategories in a separate package for that purpose. |
The compile times are due to some changes I had to make for this package to work with the recent changes in UniMath. If I recall correctly, the definitions for monads have changed slightly, and those for comonads have been added. These are apparently significantly slower somehow... |
I see. Such changes might require some minor refactoring at some other parts. |
This PR is an updated version of #1822