Negation of rational reals #1304
Conversation
|
While I greatly appreciate your effort to structure your contributions, I have to say that submitting so many tiny requests adds considerable organizational overhead on my part, as well as waiting time for the CIs to complete on each. Personally, I would prefer PRs that are somewhere between 200 lines to 1500 lines, if you could make that work with your workflow. Perhaps @EgbertRijke and @VojtechStep have different preferences, but I cannot personally continue to review at the pace you are submitting PRs given the size of the individual contributions. |
|
I was basing my strategy on this comment here by @EgbertRijke , which expressed appreciation for "simple and small pull requests that are easy to review and merge." I can try to find some place in between, or err on one side or another. I am also, to be clear, extremely fine with longer review times; I know I'm making a whole lot of changes very fast. |
|
I will admit my own software engineering background also biases in the direction of breaking out incremental changes that are as small as possible, letting CI work at its own pace, but that's just what I'm used to, not something I insist on. I would appreciate if you and the other maintainers decided on a preference I can follow universally, since it seems like there's disagreement on the best approach. |
|
Yes, let's wait for input from the others |
|
The thing that is universally agreed upon is that receiving pull requests is very much appreciated, especially if the author takes so much care of their work as you have been demonstrating. For some of your smaller lemmas it would be helpful if the thing you formalized it for was also included, because it helps the bigger picture. Sometimes a single definition is just a fine addition to the library, so it can stand on its own in a pull request. And sometimes, changes are more comprehensive, and then the pull request will contains everything in the transitive closure of all the changes that are necessary for that one change. When that happens, it is important that the pull request remains a comprehensive whole, but there are no laws in the users guide that formally restricts such pull requests. Like Fredrik said, pull requests up to about 2000 LOC that achieve a single goal are just about right for reviewing, but I am also happy with Fredrik's larger pull requests (I say that diplomatically, because I am myself also an author of occasional large pull requests). In terms of the amount of time per line of code spent reviewing those, I think it doesn't matter much. Possibly the smaller ones are actually more expensive in terms of time and effort, but it also has other advantages: You were new to contributing to agda-unimath and the fact that your pull requests were small made it possible for us to make incremental suggestions to your contributions. This brings me to a topic that actually I wanted to discuss with you, but I don't have other means of contacting you. Sometimes you show that the reals satisfy a certain property, but then you will just prove that instead of introducing that property formally for the most general kinds of structure for which it makes sense. For example, the Archimedean property is defined three times in an ad-hoc manner, and this could be much better stated as a general property of an ordered ring, and then showing that the four number systems that are shown to be Archimedean should be instances of those. Similarly for dense linear orders. However, please don't take these comments as criticism, I very much appreciate your work! |
|
If it helps, I joined the Univalent Agda Discord as Louis W. |
|
I think that guidance makes sense in a way I can apply to how I organize things. Thanks! I will say that when I don't make a more general form of things, it's often because I'm not certain how, where, or what things should be called -- the concept of a large preorder and what that meant was entirely new to me, for example. I am very much an amateur in this area -- for example, I have almost no category theory, though I'm trying to rectify that. I can try to be more aggressive about trying to generalize, but I suspect I'll make more missteps about naming, correct placement of things, and especially not realizing when there's already a tool in the library that can be applied, under a name I haven't heard yet. If you can tolerate that, I'm happy to give more of those things a go. |
|
Let me also say that I think you're doing a great job, and it has been a good thing that your individual contributions thus far have been very small. It helps us guide you to avoid misteps in the starting phase. I think it's probably a little early to ask you to scale up your contributions to 200 loc or more, but maybe we could try and scale them up a bit at least? There's a different point about formalizing with the appropriate level of generality in mind, and that often leads to larger pull requests, but we're here and willing to help you approach that |
No description provided.