Ditch the modules; closes #1209 #1238
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
You can apparently tell coq which coercions should always be printed. Use the following straight after the definition of Coercion Tr : trunc_index >-> Modality.
Add Printing Coercion Tr.This will stop the modality |
Collaborator
|
Splitting up ReflectiveSubuniverse is #1099 |
Collaborator
|
Is there any point to having CoreflectiveSubuniverse.v in its own folder in Comodalities anymore? If it doesn't look likely that we will add any comodalities, should we not just put them in the modalities folder? It's not like everything in the modalities folder has to do with modalities anyway. |
Alizter
reviewed
Feb 16, 2020
| : {d:D & P d * Q d} <~> Pullback (@pr1 D P) (@pr1 D Q) | ||
| := Build_Equiv _ _ _ (ispullback_sigprod P Q). | ||
|
|
||
| (** If the induced map on fibers is an equivalence, then a square is a pullback. *) |
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Collaborator
|
By the way, you can implement all my suggestions at once into a single commit. Just press the Add Suggestion to batch button. |
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Collaborator
|
I'm glad that this is working out! After stepping through ReflectiveSubuniverse I noticed there are a lot of places we can optimise, for example by using |
Collaborator
|
I think that with my comment about printing coercions you can modify the last commit so that it only removes the imports of TrM. |
Alizter
reviewed
Feb 16, 2020
Alizter
reviewed
Feb 16, 2020
Contributor
Author
|
I actually find |
Collaborator
|
This is looking great! Much cleaner and easier to understand, and more flexible. It might be a day or two before I can continue reviewing. BTW, did you check how this reorganization affects the build times? |
Contributor
Author
|
No hurry, take your time. I haven't done a time check yet. |
Alizter
approved these changes
Feb 16, 2020
Collaborator
Alizter
left a comment
Alizter
left a comment
There was a problem hiding this comment.
LGTM. I am a bit worried about calling yet another thing descent however.
Contributor
Author
|
If we ever define descent for wild categories, all the others should be special cases... (-:O |
Contributor
Author
I ran a timing diff; click to expand.Apparently this actually speeds the entire library up by about 30 seconds! With most of the improvement happening, unsurprisingly, in the Modalities files. I can't guess why; I would have expected the added typeclass inference to slow it down. That might be what's happening to slow down BAut/Bool; perhaps some careful use of nrefine there would speed it up. |
Collaborator
|
@mikeshulman Fascinating. I wouldn't mind taking a look tomorrow and optimizing some of those files. |
Contributor
|
It looks like it's a small diff spread across many files. It wouldn't surprise me if there old code managed to exercise modules heavily enough that the speed up is due to fewer functors and modules lying around. (If I recall correctly, Coq needs to do special things when adding modules to the global namespace, that it doesn't need to do with constants? I'm not sure if I recall correctly, though.). Low confidence in this guess, but it seems possible. |
Collaborator
|
Here are all files where the change was 1s or more. As Jason said, no single file changed by a huge amount. |
Collaborator
|
And here are all of the files whose processing time (after this PR) takes at least 5s. There's probably some low-hanging fruit here. (For another PR, not this one.) |
Collaborator
|
This is great news, Mike. I was hoping it would be what happens, just because it's simpler overall. @Alizter , it's probably best to get this merged before trying to optimize things further. |
Collaborator
|
Very well, I will wait for this to be merged which I am happy with doing. |
Contributor
Author
|
FWIW, the apparent big speedup in Regarding looking for low-hanging fruit, we should pay a bit of attention not just to the total speed of files but their ratio of speed to length. For instance, one reason ReflectiveSubuniverse is on that list is just because it's currently massively long. |
Collaborator
|
ReflectiveSubuniverse has just a few lines that dominate the time. The timing-html/... file is very handy. |
Contributor
Author
|
Thanks for all these suggestions! However, I'm starting to feel that it's inefficient for you to make lots of little suggestions line by line on github and for me to then go through and implement them all. Github's suggest-a-change feature makes things a little easier, but wouldn't it be even easier for you to just make all the changes in a branch of your own as you find them and then submit a PR to my branch (or to the main repo after this is merged, if the changes aren't essential)? If there are any of the changes that I don't like, I can easily revert them when I merge your PR into my branch. |
Collaborator
|
Yes, that makes more sense. I'll limit myself to more conceptual comments now, then we can merge it, and then I can follow up with a PR with minor things. Can you do the ones I already mentioned? |
jdchristensen
approved these changes
Feb 17, 2020
Collaborator
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
LGTM, once the minor comments are addressed. I really like how cleanly things worked out in Descent.v!
Collaborator
|
@mikeshulman I guess you can merge when you are ready. |
Alizter
approved these changes
Feb 17, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This grew into a bigger project than I intended, but now I think it is clearly the right way to go.
The most important changes are in
ReflectiveSubuniverse.vandModality.v, combined with the new filesDescent.vandSeparated.v. (I don't expect the diffs for these files to be very readable; you'll probably want to fetch the branch directly and read the files locally.) The rest of the changes, to all the files in theModalitiesdirectory and lots of files elsewhere, are mainly either support for these changes or adapting to these changes.Now
ReflectiveSubuniverseandModalityare records parametrized by one universe on which they live. That is, an element ofReflectiveSubuniverse@{i}is a reflective subuniverse ofType@{i}.I did not make any changes to
Basicsor define anAccRSUtype such as suggested in Redefine IsTrunc as an instance of AccRSU in Overture #1224. As @jdchristensen proposed there, this idea seems to be unnecessary; we can maintain the previous design with many different ways to construct modalities, including truncations, some of which turn out to be accessible afterwards.The main changes visible in the rest of the library are (1) no longer any need to
Import TrM(yay!), but (2) you have to writeTr nin a bunch of places where you could previously just writen. I can't think of a way around the latter change at the moment (declaring a coercion fromtrunc_indextoModalitywould, combined with the coercion fromModalitytoFunclass, result in Coq displaying the propositional truncation ofAas(-1) A, which I think is undesirable).One of the benefits of this change (which I think i forgot even to mention in Ditch the modules; free the modalities #1209) is that it will enable us to split up the monster file
ReflectiveSubuniverse.v. But I didn't attempt that yet; this way it's easy to see that most of that file didn't need any change.A lot of the universe annotations that we used to need are now unnecessary. I removed some of them (indeed, some of them had to be removed), but didn't systematically go through removing them all. (On the other hand, the management of universes now becomes a little fiddlier when passing back and forth between accessible modalities and their extensions to larger universes.)
I took @jdchristensen's suggestion and introduced a typeclass for saying that a particular type has a reflection into a subuniverse, with a
ReflectiveSubuniversebeing one for which this holds of all types. Many of the theorems about reflective subuniverses could be stated with only hypotheses like these, rather than that the entire subuniverse is reflective, but I didn't bother trying to do that.Similarly, I introduced typeclasses saying that a particular reflection has dependent elimination into a subuniverse and that it has descent into a subuniverse. We say
O1 << O2if every O2-reflection has dependent elimination into O1-modal type families, andO1 <<< O2if in addition families of O1-modal types descend along O2-reflections. Then an RSU O is a modality iffO << O, and lex iffO <<< O, while for any RSU we haveO <<< Sep O. Most of the theorems about lex modalities, and many of the theorems in CORS about separated pairs, are special cases of theorems about these general relations between modalities. Accordingly, most of these theorems are now proven inModality.v(for<<) orDescent.v(for<<<), and simply re-stated inLex.v(and will be similarly re-stated inSeparated.vonce we formalize the proof thatSep Ois always reflective). I'm sorry about introducing this new content change at the same time as a technical refactoring, but the refactoring required making a choice about how to bundle things and how to represent separated subuniverses, and it seemed like it would be less work overall to incorporate this change right from the start.Since there are so many ways to define a modality, it's unclear which of them should be bundled up in the record type
Modality. I made one choice, but I'm not at all sure it's the best one; feel free to make other suggestions.Regarding the desire for truncations (for instance) to be polymorphic, it seems that this is very rarely an issue. A little universe annotation together with defining
Truncas a "cumulative inductive type" makesTrunc_functoras polymorphic as necessary, and a couple changes in other places are all that was needed so far.Regarding the question of universes being modal, it seems that most of the time it is easier to work directly with the property that "modal type families descend", or even "reflections are oo-extendable into the universe", rather than trying to rephrase the latter in terms of the universe actually belonging to some reflective subuniverse. It is possible to pass back and forth to such versions as well, but at the cost of some finicky universe-wrangling that took me a while to get right (but I wanted to be sure it was possible, to be sure we weren't losing anything very important with this change). The price is some interesting lemmas that look very confusing to step through unless you have
Set Printing Universeson to see how the universe annotations are changing at each step. Overall, I think there is less universe-wrangling than previously, and what there is is more "isolable".Since this is such a large PR and also a big design change, I expect it will take a while to read and review, and we should be sure to wait enough time for everyone who wants to have a look at it to weigh in.