prioritizing porting efforts

Stream: mathlib4

[Arthur Paulino]

Is there a way to prioritize the porting efforts more precisely? Like knowing which unimplemented tactics are required more often or which non-ported files would unlock the most when ported.
Maybe we would have a better direction if we could follow some kind of naive greedy algorithm to focus our efforts

[Kevin Buzzard]

Someone (perhaps Patrick) suggested the following idea: pick a random file in mathlib (eg your favourite file) and see how well mathport does on it. If it doesn't succeed then start picking up the pieces.

[Arthur Paulino]

Then do it many times and count which pieces are more important?

[Alex J. Best]

Yeah, almost all tactics need to be ported eventually right? So just counting them by number of times they appear in the source code (with grep and wc for instance) seems like a fair greedy algorithm :smile:

[Gabriel Ebner]

There's still lots of low-hanging fruit in Mathport/Syntax.lean indeed.

[Edward Ayers]

I've almost done restate_axiom

[Edward Ayers]

Would it be ok to make github issues for some of the bigger tactic port projects?

[Arthur Paulino]

@Edward Ayers do you mean to signal that you're working on it?

[Edward Ayers]

I do

[Arthur Paulino]

No, I mean: do you want to create issues as a way of saying "hey, I'm working on this one"?
(or did you answer that question already? :joy: )

[Edward Ayers]

Yes I think github lets you assign people to issues so that was the idea

[Edward Ayers]

Just normal devopsy ticketing stuff

[Arthur Paulino]

I think we'd need higher privileges in the repo to do that ourselves without asking maintainers to do it for us (I don't think we'd be able to assign people to issues as of now)

[Arthur Paulino]

Another advantage of that would be being able to create branches on the repo. It would make it easier for people to fetch branches created by other people. Collaboration would be easier

[Patrick Massot]

I'm pretty sure we can give you more right on the mathlib4 repo (both to Arthur and Ed).

[Scott Morrison]

I went ahead and gave @Edward Ayers and @Arthur Paulino write access on the mathlib4 repo.

[Scott Morrison]

(I think we haven't protected master yet, so this gives you technical permission to push direct to master, but obviously try to remember not to do this. :-)

[Arthur Paulino]

Alright, thanks!