Zulip Chat Archive

Stream: general

Topic: mathlib pull requests


Sean Leather (Jun 19 2018 at 07:10):

@Mario Carneiro and @Johannes Hölzl: There are a lot of pending PRs. What would you like to do with them?

I understand you were busy in Hanoi for a while. And perhaps you're still busy with other things. This is just a friendly ping to see what your status is.

Every now and then, something comes up that I want to contribute to mathlib, but then I see the list of pending PRs, and I get a bit discouraged, thinking that it might not be worth it. Some pretty simple PRs have not seen any response to indicate what will happen to them.

That said, if you need help managing contributions, I can volunteer some time. I can do commenting, labeling, and merging of simple PRs, while leaving the more interesting ones to you. (Of course, it's git, so things can always be changed later.)

Sean Leather (Jun 19 2018 at 12:21):

@Mario Carneiro Thanks for all your recent PR merges and comments. Just so you know, if you'd like more help with mathlib maintenance, my offer stands.

Mario Carneiro (Jun 19 2018 at 12:24):

I did all the easy stuff. I'm still a bit busy with Tom Hales' conference this week, but some organization or prioritization of existing PRs would be a thing third parties could do to make it easier. Unfortunately in many of the remaining PRs there is something I see a problem with but I haven't found the time to write about it, so for those you may have to just wait or guess (or ask).

Simon Hudon (Jun 19 2018 at 12:26):

Anything I should be doing for refine_struct?

Mario Carneiro (Jun 19 2018 at 12:29):

I'd rather not merge conflicts from github, could you do that? Otherwise it's okay (the conversation and travis failure made it look more complicated than it is, but I see it's ready for merge now.)

Simon Hudon (Jun 19 2018 at 12:29):

Cool, sure thing

Sean Leather (Jun 19 2018 at 12:42):

some organization or prioritization of existing PRs would be a thing third parties could do to make it easier.

Yeah, that's basically what I was thinking: triage with labels, assign issues and reviewers, ping the various parties every now and then, and update statuses. If it's an easy/obvious PR, merge it.

Unfortunately in many of the remaining PRs there is something I see a problem with but I haven't found the time to write about it, so for those you may have to just wait or guess (or ask).

Yep.

Simon Hudon (Jun 19 2018 at 14:31):

The build time for mathlib is truly incredible. I wonder if we could minimize the rebuild size on every change

Simon Hudon (Jun 19 2018 at 14:34):

This is where a lint tool would be very useful: we could find dead code and spurious dependencies

Scott Morrison (Jun 20 2018 at 06:27):

The refine_struct in mathlib seems to be misbehaving. Here's my MWE:

import tactic.interactive

variable (α : Type)
def foo : semigroup α :=
begin
  refine_struct ({ .. } : semigroup α),
end

Scott Morrison (Jun 20 2018 at 06:28):

Which just says failed on the refine_struct. It seems that it's failing at the very first line str ← e.get_structure_instance_info, of refine_struct.

Scott Morrison (Jun 20 2018 at 06:28):

(@Simon Hudon)

Sean Leather (Jun 20 2018 at 06:30):

@Scott Morrison Would you mind creating a new GitHub issue with this information? It will make tracking the problem and its solution easier.

Scott Morrison (Jun 20 2018 at 06:31):

Can do! I thought that since it was such a basic thing I might be doing something stupid, and should ask here first. :-)

Sean Leather (Jun 20 2018 at 06:32):

Can do! I thought that since it was such a basic thing I might be doing something stupid, and should ask here first. :-)

Even if it is something stupid, others might run into it, too. And it's still easier to search GitHub than Zulip. :wink:

Sean Leather (Jun 20 2018 at 06:33):

(That's my personal experience, anyway. Others may have different thoughts.)

Sean Leather (Jun 20 2018 at 06:34):

Of course, you can always check here first and put it there later, I suppose. But I think that creates extra work for you.

Scott Morrison (Jun 20 2018 at 06:44):

https://github.com/leanprover/mathlib/issues/160

Simon Hudon (Jun 20 2018 at 11:48):

(deleted)

FMLJohn (Nov 23 2023 at 11:45):

Hi all! Right now I am stuck on some issue in my recent pull request. Some strange thing has happened. I have edited my codes several times, but the continuous integration still cannot be passed. Specifically, my pull request cannot pass the step continuous integration / Build (push). I had a look at the details of the errors, and noticed that lots of errors appeared in some files I had never changed before. I have tried git merge master, lake exe cache get, etc. but the problem still cannot be solved. Is there any method to deal with this issue? Here is the link of my pull request: https://github.com/leanprover-community/mathlib4/pull/8187. Thank you very much!

Eric Wieser (Nov 23 2023 at 11:50):

I left a comment on the PR


Last updated: Dec 20 2023 at 11:08 UTC