Project Dashboard

Stream: FLT

[Pietro Monticone]

I am setting up the whole dashboard-based infrastructure we are developing for EquationalTheories.

It should be ready in a few days, but the contribution guide will be the following:

Contributing to the FLT Project

Thank you for your interest in contributing to the FLT Project! This guide provides detailed instructions on how to effectively and efficiently contribute to the project.

Project Coordination

The project is managed using a GitHub project dashboard, which tracks tasks through various stages, from assignment to completion.

How to Contribute

Contributions to the project are made through GitHub pull requests (PRs) that correspond to specific tasks outlined in the project's issues. The following instructions detail the process for claiming and completing tasks.

1. Task Identification

• Tasks are posted as GitHub issues and can be found in the Unclaimed column of the project dashboard.
• Each issue represents a specific task to be completed. The issue title and description contain relevant details and requirements.

2. Claiming a Task

• To claim a task, comment the single word claim on the relevant GitHub issue.
• If no other user is assigned, you will automatically be assigned to the task, and the issue will move to the Claimed column.
• You may only claim one task at a time. If you decide not to work on a task after claiming it, comment the single word disclaim on the issue. This will unassign you and return the issue to the Unclaimed column, making it available for others to claim.

3. Working on the Task

Once you are assigned to an issue, begin working on the corresponding task. You should create a new branch from the main branch to develop your solution.

4. Submitting a Pull Request

• When you are ready to submit your solution, create a PR from your working branch to the project’s main branch.
• After submitting the PR, comment the single phrase propose PR #PR_NUMBER on the original issue. This links your PR to the task, and the task will move to the In Progress column on the dashboard.
• A task can only move to In Progress if it has been claimed by the user proposing the PR.

5. Withdrawing or Updating a PR

• If you need to withdraw your PR, comment the single phrase withdraw PR #PR_NUMBER on the issue. The task will return to the Claimed column, but you will remain assigned to the issue.
• To submit an updated PR after withdrawal, comment the single phrase propose PR #NEW_PR_NUMBER following the same process outlined in step 4.

6. Review Process

• After finishing the task and ensuring your PR is ready for review, comment the single word awaiting-review on the PR. This will add the awaiting-review label to your PR and move the task from In Progress to the In Review column of the dashboard.
• The project maintainers will review the PR. They may request changes, approve the PR, or provide feedback.

7. Task Completion

• Once the PR is approved and merged, the task will automatically move to the Completed column.
• If further adjustments are needed after merging, a new issue will be created to track additional work.

[Pietro Monticone]

For those interested, here is the PR building the dashboard-based infrastructure mentioned above: FLT#153.

I'll test the whole workflow in an {issue, PR} pair.

[Pietro Monticone]

It throws a bureaucratic error message:

Resource protected by organization SAML enforcement. You must grant your Personal Access token access to this organization.

It just means we need more personal access token permissions from the ImperialCollegeLondon Github organisation to make the Github actions control the task cards transitions.

Here is what they need to do https://docs.github.com/en/enterprise-cloud@latest/authentication/authenticating-with-saml-single-sign-on/authorizing-a-personal-access-token-for-use-with-saml-single-sign-on

[Notification Bot]

3 messages were moved here from #FLT > Outstanding Tasks, V5: Frobenius elements by Pietro Monticone.

[Pietro Monticone]

We are a bureaucratic permission + a GraphQL query away from actually completing the implementation of the dashboard-based workflow in FLT.

[Pietro Monticone]

Now all the dashboard-based workflow files and the new CONTRIBUTING page are ready for deployment.

We are just waiting the bureaucratic permission from the ImperialCollegeLondon GitHub organisation owners.

Related: #Equational > WORKFLOW UPDATES

[Kim Morrison]

Pietro Monticone said:

We are just waiting the bureaucratic permission from the ImperialCollegeLondon GitHub organisation owners.

Hopefully Kevin has reminded said owners that he may need to move this extremely high profile project elsewhere if this doesn't happen promptly. :-)

[Terence Tao]

"I have formalized a truly marvelous proof, which the permissions of this repository are too narrow to contain."

[Shreyas Srinivas]

Ah I see that we have convinced other projects to adopt our approach @Pietro Monticone

[Shreyas Srinivas]

For the Equational theories project, I did not use the "PR ready for merge" project status, because the incoming PR rate was small. But you might want to alter this workflow for FLT. The idea behind this status was that reviewers would mark PRs with a ready-for-merge label and maintainers can process only this queue and merge PRs in batches.

[Shreyas Srinivas]

You want a merge-after-CI comment which will merge PRs from "PRs in Review" and move them to "Completed Tasks". I miss this label from Mathlib in equational_theories.

[Shreyas Srinivas]

one more suggestion: the contributing.md file should instruct how to propose new tasks and get them added to the project task list.

[Pietro Monticone]

The incoming PR rate (450 in 3 weeks) for ET didn’t feel very small honestly :sweat_smile:.

Jokes aside, I’ll definitely consider incorporating those if needed.

[Shreyas Srinivas]

At any point we have had 10 active PRs

[Shreyas Srinivas]

Not counting maintainer PRs.

[Shreyas Srinivas]

The reason I am suggesting this batch merging step for FLT is that it is a longer term project and might evolve a distinction between those who only review PRs and those who merge them

[Shreyas Srinivas]

In contrast, in EQ, Terence Tao, you, and I were reviewing and merging all the PRs

[Shreyas Srinivas]

And even there I came to the conclusion that we could have used help from more reviewers

[Shreyas Srinivas]

Another tip: add the project dashboard link to the blueprint and get a zulip linkifier for it

[Pietro Monticone]

I have tested the new dashboard-based workflow:

• Project dashboard
• Test issue: FLT#178
• Test PR: FLT#154

It can be adopted from now on.

[Kevin Buzzard]

Thank you Pietro for all your work on this and sorry that Imperial took so long to press various buttons!

[Shreyas Srinivas]

Btw, @Kevin Buzzard : please let me know how the workflow works out for you.

[Shreyas Srinivas]

We plan to write a section in the equational theories paper which is like an experience report for mathematicians on workflow management for math collaborations using these tools

[Shreyas Srinivas]

and your feedback will be very useful

[Kevin Buzzard]

Right now what's been going on is that I've been avoiding having to learn about the workflow because we've had administrative issues due to the fact that I chose to host it on Imperial's github organization and asking them to click buttons turned out to take a lot longer than asking the leanprover community organization to click buttons :-) But all the buttons are clicked now. So I will start switching to this workflow and let's see what happens.

[Kevin Buzzard]

I tried claiming a task here https://github.com/ImperialCollegeLondon/FLT/issues/307#issuecomment-2573771583 and it didn't move on the dashboard. Did I do something wrong?

[Pietro Monticone]

No, it doesn't seem you did anything wrong. It throws an error when it tries to retrieve the project ID. Let me take a look.

[Pietro Monticone]

I'm debugging the issue. Best guess: PAT_TOKEN expiration.

[Kevin Buzzard]

Oh does this email which I ignored

Hey @kbuzzard,

Your personal access token (classic) "FLT classic personal access token" with project and repo scopes has expired.

If this token is still needed, visit https://github.com/settings/tokens/1801993316/regenerate to generate an equivalent.

If you run into problems, please contact support by visiting https://github.com/contact

Thanks,
The GitHub Team

have anything to do with it?

[Pietro Monticone]

Yep

[Kevin Buzzard]

Hang on, I'll generate a new one

[Kevin Buzzard]

OK it's working again. Thanks a lot Pietro!

[Django Peeters]

I've just finished a proof of unitsrat_meet_unitszHat from the blueprint, which I started working on before the dashboard was made, but I don't see it among the tasks. What do I need to do?

[Ruben Van de Velde]

If you have the proof, make a pr!

[Django Peeters]

Will do!

[Kevin Buzzard]

Yes please! I never taskified that project; that was when I was experimenting with a different definition of the adeles.

Recently I proved (on paper) that one definition of the finite adeles of a number field $K$ is $K\otimes_{\Z}\widehat{\Z}$, with the $\widehat{\Z}$-module topology. This experiment from the blueprint was testing the feasibility of using this as a definition. The one argument against having this as a definition is that it's not the definition in the books but it's a joy to work with and I wonder whether it might be easier to use this as the definition and then to prove that it's isomorphic both topologically and algebraically to the definition in the books.

[David Michael Roberts]

Having a better definition than what's in 'the books' feels to me something I'd see in a lecture by Scholze.

[Pietro Monticone]

FLT#332 by @Django Peeters is ready to merge now.

[Kevin Buzzard]

Thanks! I'll review it first

[Pietro Monticone]

Sure, sorry. I meant “ready for review”.