A reminder about making PRs

Stream: Equational

[Shreyas Srinivas]

I would like to remind and request everybody that if you have an idea please request a task for it by creating an issue and discussing it in a zulip thread. Please follow the claims process. This keeps the maintainers' task simple and ensures that nobody's work overlaps too much with anybody else and everyone gets an opportunity to work on their contributions without worry of being overshadowed by competing PRs.

[Avi Levy]

@Shreyas Srinivas can you elaborate on the exact procedure for this part:

please request a task for it by creating an issue and discussing it in a zulip thread

For example, I spotted a typo in Definition 7.1 in the blueprint which I was going to fix just now. To follow the process listed above, I first opened a new issue Issue #470 then claimed the issue and proposed PR #471 on the issue. After merge validation completed on the PR, I also added the awaiting-review tag. However, throughout this process, nothing new showed up on the project board here, so I suspect I missed a step - but I do not know which.

[Shreyas Srinivas]

Ah so what's missing here is that maintainers have to add the task to the project board

[Shreyas Srinivas]

Since github doesn't restrict PRs on public repositories, it is the only filter we have to make ensure the contributions process works in some sense.

[Shreyas Srinivas]

Otherwise we could be flooded with overlapping PRs and lose track of which PR was doing exactly what

[Shreyas Srinivas]

This is why we encourage zulip discussions on the issue

[Avi Levy]

Ah, I think I missed another thing as well - I just noticed that when I added awaiting-review to the PR equational#471, it failed to find the link to the issue equational#470 - the failed job https://github.com/teorth/equational_theories/actions/runs/11258721703/job/31305993978 shows the error message

No related issue found in PR body. Exiting...

when running

ISSUE_NUMBER=$(jq -r '.body | capture("Closes #(?<num>[0-9]+)") | .num' pr.json)

I retroactively edited the PR body to include the phrase "Closes #470" and now I know to do this for next time!

[Shreyas Srinivas]

So if you had proposed the PR after the issue was added to the project, this would have happened automatically

[Shreyas Srinivas]

So if you look at how tasks were managed in the PFR project, the idea was that there would be outstanding tasks threads (see examples in #Polynomial Freiman-Ruzsa conjecture). People would claim them and Terence Tao would manually edit the top message to validate the claim. We built on that basic scheme and automated it all the way.

One difference is that the tasks don't have to be batched up anymore. That was primarily because of the constraints of managing the project over zulip (not wanting to lose track of tasks and threads for example)

[Shreyas Srinivas]

Essentially it is a ticket system, except here the maintainers post the tickets (issues/tasks) and contributors pick them up.

[Avi Levy]

Regarding the four entities:

1. Zulip thread
2. Issue
3. Project board
4. Pull request
   1,2, and 4 can be done by any contributor but 3 requires maintainer involvement. The link from 2 -> 4 is done by posting a "propose #XXX" message on the issue, and the link from 4 -> 2 is done (perhaps automatically in some scenarios) by including a "Closes #XXX" message in the PR. The Zulip thread should reference 2 and 4 using projectname#XXX which Zulip automatically linkifies

[Shreyas Srinivas]

3 is largely handled by CI actions

[Shreyas Srinivas]

One quibble I have with github's projects (I am saying this fully realizing that you work at Microsoft), is that there are a set of default workflows which can be expressed in flowchart GUI, but for everything else CI scripts are necessary. There is no room for custom project workflows to be added in the flowchart language.

[Shreyas Srinivas]

One of the default workflows takes any issue labelled "project-task" and adds it to the dashboard. We restrict this label to maintainers.