Stream: coq-community devs & users

Topic: Repo maintenance in CPMOs


view this post on Zulip Karl Palmskog (Nov 27 2022 at 00:12):

if there was ever a clear example of a repository that would be better maintained in a community package maintenance org, I think this one is it: https://github.com/openai/miniF2F/pull/121 (employee who maintained repo quit the company)

view this post on Zulip Karl Palmskog (Nov 27 2022 at 00:21):

(ideally leanprover-community org arranges the repo transfer or makes a fork)

view this post on Zulip Bas Spitters (Nov 27 2022 at 11:25):

Did you contact the lean community, like @Jason Rute ;-) . Sounds like this could help automatic translation (of statements) across systems.

view this post on Zulip Jason Rute (Nov 27 2022 at 12:31):

The discussion on the Lean zulip about this is here: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Meta.20IMO.20result (Well, it is on the ML for TP stream of the zulip. I don't know how many Lean users read it regularly.)

view this post on Zulip Karl Palmskog (Nov 27 2022 at 12:43):

the fork at https://github.com/facebookresearch/miniF2F was mentioned, but it really doesn't solve the problem (now you have two repos with uncertain future prospects, in non-collaborative GitHub orgs)

view this post on Zulip Jason Rute (Nov 27 2022 at 13:32):

It is probably better to have the conversation there since some people who maintain both those repos are in those conversations.

view this post on Zulip Karl Palmskog (Nov 30 2022 at 11:35):

I filled in my point of view there, but unfortunately, seems that discussion got completely tangled up in the "IMO grand challenge" stuff. A general benchmark for ITP machine learning is of general interest, but I think the IMO stuff is not.

view this post on Zulip Karl Palmskog (Nov 30 2022 at 11:38):

if anyone plans to do Coq-miniF2F, best thing to do is likely to fork


Last updated: Feb 05 2023 at 14:02 UTC