Zulip Chat Archive

Stream: mathlib4

Topic: prioritizing porting efforts


Arthur Paulino (Mar 15 2022 at 12:58):

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 (Mar 15 2022 at 17:29):

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 (Mar 15 2022 at 17:38):

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

Alex J. Best (Mar 15 2022 at 17:52):

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 (Mar 15 2022 at 18:10):

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

Edward Ayers (Mar 15 2022 at 18:10):

I've almost done restate_axiom

Edward Ayers (Mar 15 2022 at 19:38):

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

Arthur Paulino (Mar 15 2022 at 20:09):

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

Edward Ayers (Mar 15 2022 at 20:09):

I do

Arthur Paulino (Mar 15 2022 at 20:10):

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 (Mar 15 2022 at 20:11):

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

Edward Ayers (Mar 15 2022 at 20:11):

Just normal devopsy ticketing stuff

Arthur Paulino (Mar 15 2022 at 20:13):

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 (Mar 15 2022 at 20:18):

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 (Mar 15 2022 at 20:48):

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

Scott Morrison (Mar 16 2022 at 03:31):

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

Scott Morrison (Mar 16 2022 at 03:33):

(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 (Mar 16 2022 at 09:15):

Alright, thanks!


Last updated: Dec 20 2023 at 11:08 UTC