mathlib pull requests

Stream: general

[Sean Leather]

@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]

@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]

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]

Anything I should be doing for refine_struct?

[Mario Carneiro]

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]

Cool, sure thing

[Sean Leather]

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]

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

[Simon Hudon]

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

[Scott Morrison]

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]

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]

(@Simon Hudon)

[Sean Leather]

@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]

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]

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]

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

[Sean Leather]

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]

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

[Simon Hudon]

(deleted)

[FMLJohn]

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]

I left a comment on the PR