PRs Welcome : CI actions to manage the project

Stream: Equational

[Shreyas Srinivas]

Hi all, I just want to leave this task list for CI actions we need to automate the management of outstanding tasks:

1. A CI action that takes a user comment "claim" on an issue and if it isn't assigned to anyone else, then assigns it to that user.
2. A CI action that takes a user comment "disclaim" on an issue and removes the issue assignment to the user.
3. A CI comment that takes a user comment that reads "propose PR #xyz", checks if that issue is assigned to the user, and if yes, then attaches that PR as the resolving PR for that issue.
4. A CI comment that takes a user comment that reads "withdraw PR #xyz" to remove the PR from this position.
5. A CI comment that takes a user comment "awaiting-review" and adds the label as well as changes the project status to the correct label. Similar actions forother project statuses (github provides an action template for this: https://github.com/github/update-project-action#inputs)

[Shreyas Srinivas]

PRs for adding these actions are welcome

[Shreyas Srinivas]

I'll review the PRs as soon as I can (mostly 10-15 hours from now)

[Shreyas Srinivas]

Combined with the existing workflow, we should have a functional task table. The expected workflow is roughly:

1. @Terence Tao posts an issue for each task with the label project-task.
2. A user claims the task by commenting "claim" under it. If you wish to drop your claim, then please comment "disclaim" on the issue.
3. If there is no other user assigned to the task, the user gets assigned to the issue.
4. The user creates a PR and then comments "propose PR #xyz" under the issue. If it is already assigned to them, their PR is now linked to the issue. To withdraw your PR, please comment "withdraw PR #xyz".
5. The user finishes the PR and comments "awaiting-review". This puts the PR in the PR Review list on the dashboard.
6. Maintainers review and merge it.
7. The project dashboard gets updated in all teh above steps.

[Shreyas Srinivas]

An example dashboard : https://github.com/users/teorth/projects/1

[Shreyas Srinivas]

You can change the things you wish to see by clicking on the arrow with blue dot. See screenshot for example:
Screenshot from 2024-09-28 03-12-12.png

[Shreyas Srinivas]

Also, until the CI actions are up : the maintainers (me, @Pietro Monticone and @Joachim Breitner ) will do our best to manually move the PRs around. And now I am off to catch some sleep.

[Pietro Monticone]

Ok, I have just tested task 1 and it should work fine now.

Screenshot 2024-09-28 at 17.28.08.png

[Pietro Monticone]

Task 2 done https://github.com/teorth/equational_theories/issues/57

[Shreyas Srinivas]

Nice

[Shreyas Srinivas]

could we alter the project status in the same files?

[Shreyas Srinivas]

or do we need to add separate tasks for those?

[Shreyas Srinivas]

the moving of tasks to "Completed Tasks" status happens with the default workflow already

[Pietro Monticone]

Task 3 and 4 don't require CI since the GitHub browser GUI already allows to do that.

The user just have to go to the Development section in the right column (under Assignees) and click on Create a branch that will be connected with this issue so that when the PR gets merged the related issue gets closed too.

[Shreyas Srinivas]

So far I have had to manually assign them

[Shreyas Srinivas]

I think the GUI only allows admins and moderators to link a PR to a task

[Shreyas Srinivas]

Ideally we only want an assigned user to link the PR.

[Shreyas Srinivas]

At scale this makes sure we don't have to mediate among competing claims

[Pietro Monticone]

Ok, can you expand a bit on task 3?

[Shreyas Srinivas]

We don't want a second user writing "claim" to overwrite a previous assigned user

[Shreyas Srinivas]

If person A is already assigned to an issue, then as long A remains the assignee, B can't claim the issue.

[Pietro Monticone]

Ok, I'll work on that

[Shreyas Srinivas]

Similarly in task 4, we want only an existing assignee to be able to propose and withdraw PRs. This avoids a lot of hassles with parallel PRs

[Shreyas Srinivas]

@Pietro Monticone : I am using an issue as the unit of work in the project. PR's get linked to issues. So the comments propose PR #xyz and withdraw PR #xyz need to be made on the issue, not the PR.

[Pietro Monticone]

I know. I am developing that propose-pr workflow.

[Shreyas Srinivas]

okay. I was confused by the comments being on the PR: https://github.com/teorth/equational_theories/pull/66

[Pietro Monticone]

No, wait. Then it's not clear what you want exactly...

[Shreyas Srinivas]

See this workflow message:

Shreyas Srinivas said:

Combined with the existing workflow, we should have a functional task table. The expected workflow is roughly:

1. Terence Tao posts an issue for each task with the label project-task.
2. A user claims the task by commenting "claim" under it. If you wish to drop your claim, then please comment "disclaim" on the issue.
3. If there is no other user assigned to the task, the user gets assigned to the issue.
4. The user creates a PR and then comments "propose PR #xyz" under the issue. If it is already assigned to them, their PR is now linked to the issue. To withdraw your PR, please comment "withdraw PR #xyz".
5. The user finishes the PR and comments "awaiting-review". This puts the PR in the PR Review list on the dashboard.
6. Maintainers review and merge it.
7. The project dashboard gets updated in all teh above steps.

[Pietro Monticone]

I see. I'll work on it later.

[Shreyas Srinivas]

a more detailed version in Contributing.md : https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md#the-contributions-process

[Pietro Monticone]

Task 3 is done.

[Shreyas Srinivas]

5 is actually multiple tasks bundled into one. It is about manipulating the task status in the project

[Shreyas Srinivas]

The most complete documentation of my design is i the contribution page link I posted above

[Shreyas Srinivas]

Currently the project workflow already adds issues with "project-task" labels to be added with the status "Unclaimed Outstanding Tasks"

[Shreyas Srinivas]

Further, when a project is in the "In Progress" state and a PR is merged, the issue is automatically moved to the "completed tasks" state

[Shreyas Srinivas]

what remains to be done are the following :

1. When a user is assigned a task, the task is moved to the state "Claimed Tasks"

[Shreyas Srinivas]

2. When a PR is linked to the task, the task moves to the "In Progress" state

[Shreyas Srinivas]

3. When an "In Progress" task's linked PR is given the awaiting-review label, the issue is moved to the "PR Reviews" state

[Shreyas Srinivas]

The state names correspond to the column names in the project dashboard's task view

[Pietro Monticone]

Task 4 is done.

These workflow files aren't perfect, but decent enough I guess.

[Shreyas Srinivas]

One key check for all the actions of task 5 is to check that they are only triggered on issues which are part of the project "equational theories project"

[Shreyas Srinivas]

with task 5, we will essentially have automated the entire job of the "Outstanding tasks" threads and any manual interventions we need to do will be limited

[Pietro Monticone]

I will probably find a little bit of time tomorrow to attack task 5.

[Shreyas Srinivas]

okay. I will give it a shot later today, but this weird mixing of yaml and bash still trips me up, so it is likely to remain open

[Pietro Monticone]

I'm sorry for the inefficiency (you have already published the CONTRIBUTING file with those commands taken for granted but I haven't finished yet).

[Pietro Monticone]

But have many other things to do I can't pospone.

[Shreyas Srinivas]

Why apologise? There's no need for that

[Shreyas Srinivas]

Ideally I should be doing this all by myself

[Pietro Monticone]

Shreyas Srinivas said:

okay. I will give it a shot later today, but this weird mixing of yaml and bash still trips me up, so it is likely to remain open

Don't worry, I claim task 5.

[Pietro Monticone]

The task "claim: assign issue and move task card from 'Unclaimed Outstanding Tasks' to 'Claimed Tasks'" is done.

[Shreyas Srinivas]

I bow to your CI mastery

[Pietro Monticone]

The task "disclaim: unassign issue and move task card from 'Claimed Tasks' to 'Unclaimed Outstanding Tasks'" is done.

[Pietro Monticone]

Shreyas Srinivas said:

I bow to your CI mastery

Not a master at all as can be seen by the commit history (aka wall of shame).

[Pietro Monticone]

Now that we activated the PAT, the awaiting-CI will work on PRs coming from forks too.

[Shreyas Srinivas]

Nice

[Shreyas Srinivas]

Unintended and pleasant consequences

[Pietro Monticone]

The task "propose PR #PR_NUMBER: move task card from 'Claimed Tasks' to 'In Progress'" is done.

[Shreyas Srinivas]

I think with this we have already automated the current workflow. The awaiting-review task will come in handy if we are flooded with PRs

[Shreyas Srinivas]

But that doesn't seem to be the case yet

[Pietro Monticone]

The task "withdraw PR #PR_NUMBER: move task card from 'In Progress' to 'Claimed Tasks'" is still missing.

[Pietro Monticone]

Should withdraw PR #PR_NUMBER close the related PR too?

[Shreyas Srinivas]

I think we should let the author decide that

[Shreyas Srinivas]

It just shouldn't appear on our task view

[Shreyas Srinivas]

And that means getting delinked from the issue

[Pietro Monticone]

Ok

[Shreyas Srinivas]

Amazing job btw. I expected that it would take much longer to have this whole thing automated out

[Shreyas Srinivas]

You've done all this in one day

[Shreyas Srinivas]

Brilliant

[Pietro Monticone]

The task "withdraw PR #PR_NUMBER: move task card from 'In Progress' to 'Claimed Tasks'" is done.

[Pietro Monticone]

There is still a lot to optimise and polish, but it seems to work decently now.

[Shreyas Srinivas]

That automates everything we need for now

[Shreyas Srinivas]

I think in a couple of weeks we should write an addendum on managing large scale lean projects with blueprint. I see a clear structure for documenting this and collecting the GitHub action scripts we used. Maybe they could become part of the blueprint template

[Shreyas Srinivas]

Or maybe a fork called blueprint-template++ for large scale collabs

[Shreyas Srinivas]

@Terence Tao : this could be a sequel to your blogpost from last year

[Terence Tao]

Certainly I'm going to try to document my "user experience" as much as possible, for instance in the thoughts and impressions thread. I recently got contacted by the editors of a proof formalization journal on whether I wanted to contribute a paper reporting on PFR but I felt that as it had been almost a year since the main activity of that project, it was too late to try to scramble to document everything (although we did at least have a retrospective thread that had some information, and also the tour blog post you mentioned). For this project I definitely foresee a paper coming out of it, which is why I am trying to be proactive in recording thoughts before they fade away. I hope you also continue contributing your own impressions to that thread!

[Terence Tao]

I think it is also good that we are working on improving CONTRIBUTING.md continuously as we progress. I'm trying to make a point of mentioning even small speedbumps. An example: I started a list of scripts on README.md and just added a note to CONTRIBUTING.md to encourage contributors of code to also update README.md with their pull request so that their new tool gets some visibility. Similarly for contributors of generated files (who can also contribute a blueprint chapter outlining their methodology).

[Pietro Monticone]

Shreyas Srinivas said:

I think with this we have already automated the current workflow. The awaiting-review task will come in handy if we are flooded with PRs

Is the awaiting-review automated labelling working as wanted or some more work is needed?

[Shreyas Srinivas]

I would label it as optional for now, because there aren't too many PRs. I guess this can change when more self contained and smaller tasks are posted a la PFR

[Shreyas Srinivas]

OTOH, for large collaborations we want to separate "in progress" PRs from PRs awaiting review having passed CI

[Shreyas Srinivas]

This is to give maintainers a queue of PRs to review and merge

[Shreyas Srinivas]

@Pietro Monticone : sorry, I didn't realise that you mean you already added it

[Shreyas Srinivas]

For the moment I think the number of PRs has been small enough that they are getting reviewed rather quickly, but @Joachim Breitner : maybe we could trial this with your PR?

[Pietro Monticone]

Shreyas Srinivas said:

Pietro Monticone : sorry, I didn't realise that you mean you already added it

No I didn't add it. It's seems there is another workflow file I have never touched.

[Shreyas Srinivas]

I added that one. It only creates the label awaiting-review on the PR. It doesn't move the issue to the PR review status

[Pietro Monticone]

Ok, I will work on it later today or tomorrow

[Shreyas Srinivas]

It's not urgent

[Pietro Monticone]

Next week, then.

[Pietro Monticone]

I temporarily disabled this action to avoid interferences with the awaiting-review.yml I am working on.

[Shreyas Srinivas]

okay. thanks for the heads up

[Shreyas Srinivas]

so for the awaiting reviews task, we must check that the CI actually builds and that the awaiting-review label has been added.

[Pietro Monticone]

The task "awaiting-review: add label and move task card from 'In Progress' to 'PRs in Review'" is done.

[Shreyas Srinivas]

:bow: :bow: :bow:

[Pietro Monticone]

This pair {issue, PR} showcases the entire workflow we have at the moment.

Again, not at all perfect, but decent enough. Now the development is faster because it's basically copy-pasting-tweaking previous project-interacting workflows.

[Shreyas Srinivas]

Thanks a lot for putting your time into this. When I started the project I assumed that I would be adding one automation per day in my spare time between other work. We should document this setup.

[Pietro Monticone]

In the next days I will optimise, polish and document those scripts of course.

[Shreyas Srinivas]

I envision a markdown document structured as follows:

1. An brief introduction of the process we are replicating and the reasons for doing this..
2. An automation types section: Here we need two subsections. In the first I can explain github's default workflows iand in the second, you could give a brief explanation of how github actions works and how to write one's own actions.
3. An expanded version of the contribution process I have put into CONTRIBUTION.md. Here we additionally explain how the automation is used in each step. We also provided a flow chart view of the whole thing. Here you could describe the scripts you wrote as well.
4. A comparison and reflection section: This should ideally be written by @Terence Tao who compares this process with the PFR and relates his experiences in terms of workload and process.

Programmers already know all this. But in the math formalisation world, the best practices are still evolving and providing some detailed "steps" can be helpful.

[Shreyas Srinivas]

We would also benefit from a scripts section that just collects the action scripts in one place.