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

Compile times for model categories #1855

Closed
nmvdw opened this issue Feb 28, 2024 · 3 comments
Closed

Compile times for model categories #1855

nmvdw opened this issue Feb 28, 2024 · 3 comments

Comments

@nmvdw
Copy link
Collaborator

nmvdw commented Feb 28, 2024 

          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...

Originally posted by @DenSinH in #1851 (comment)
@DenSinH DenSinH mentioned this issue Mar 5, 2024
Merged
@DenSinH
Copy link
Contributor

DenSinH commented Mar 5, 2024

Working on this in #1858

benediktahrens pushed a commit that referenced this issue Mar 6, 2024
@DenSinH
Optimizing Model Categories (#1858)
6605a4a 
For fixing #1855 

I have yet to test how long it takes to `make ModelCategories` from
scratch on my 8 year old laptop through WSL, but I believe it is within
a reasonable time on my 8 year old laptop with:
- i5 7200U quad core @ 2.5GHz
- 8GB 2133MHz memory
I hope the CLI is faster than this extremely bottlenecked setup, but who
knows...

The LNWFSMonoidalStructure (~5min), LNWFSCocomplete.v, LNWFSClosed.v and
LNWFSSmallnessReduction.v files
still seem to take the longest, but this should be enough to compile
within the time limit I would think.
It kind of dazzles me though, since on Windows, and with a slightly
older version of UniMath, and Coq 8.17
the LNWFSClosed and LNWFSSmallnessReduction files take up literally half
a minute. What makes these
files different is that there are two proofs where I try to show an
LNWFS structure `L -->[mor] L'` on `mor`,
given an LNWFS structure `L -->[mor'] L'` for `mor' = mor`, so to say. I
used to use a rewrite in the proof,
which seems to cause the slowness. Now I abstracted that to an opaque
proof, which seems to speed up the
process slightly, but it is still pretty slow... 

I am not sure if there is already a CLI check for the ModelCategories
package, but I would like to know if the
files compile properly in the GitHub CLI as well. Preferably this should
happen kind of soon, since I am in the
process of writing an article on this theory based on my thesis,
supervised by Paige North, and it would be very
valuable if the theory is (properly) integrated into the UniMath
library.

Strategies for improving the compile times include sectioning and adding
Context variables, splitting up some proofs, making certain terms Opaque
within the file and shortening some proofs. I will work on it a bit more
tomorrow and get back to it in this PR.
@DenSinH
Copy link
Contributor

DenSinH commented Mar 6, 2024

I feel like this issue can be closed now, or does the package need to be optimized further?

@nmvdw
Copy link
Collaborator Author

nmvdw commented Mar 6, 2024

Yes, it can be closed

@nmvdw nmvdw closed this as completed Mar 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nmvdw @DenSinH