CONTRIBUTING.md

Stream: Equational

[Terence Tao]

I think the workflow is becoming clearer now, especially with the recent creation of AllEqations.lean, the suggestion of @Edward van de Meent to incorporate the proof_wanted feature of Lean, and the move to Github Issues to manage tasks. I have thus started a first draft of the CONTRIBUTING.md file to try to codify how we want contributions to proceed going forward. Suggestions and feedback welcome!

[Shreyas Srinivas]

I think the contribution file should link to the project dashboard and explain the process of claiming issues

[Terence Tao]

That sounds good. Would you be able to edit the file directly to add the links? Right now I just linked to the relevant Zulip thread but a direct explanation is probably better.

[Shreyas Srinivas]

Yeah I can do that.

[Shreyas Srinivas]

Another point : about the decentralisation, a github project can manage any number of repositories. I am still learning the strange language github uses for automating the project task actions. But if someone pitches in, we should be able to assign tasks, link PRs and move tasks to the correct column automatically

[Shreyas Srinivas]

Done

[Vlad Tsyrklevich]

One more thought I just had, is that we should ask that contributions are reduced to their transitive reduction (e.g. fewest number of implications). If they don't do it over all of Lean, then at least doing it among their own theorems would be useful. It may be nice to say this for now, and when there is slightly more tooling for pulling out all implications then providing a handy command to do so. I'll PR if no one objects.

[Terence Tao]

This sounds like a good idea to me. Having tooling both to expand out to a maximal set of implications, and also reduce to a minimal spanning set of implications, both sound useful to have. Please go ahead and update the language in CONTRIBUTING.md accordingly.

[Shreyas Srinivas]

Unless we provide the tooling to reduce transitive implications, it may not be easy for authors to do this, especially in auto-generated proofs

[Terence Tao]

Well, we can express a preference then for putting a reduced set implications in the Lean file (but perhaps a completed set of implications in some other data file that is not loaded by Lean). But it is not essential that it is maximally reduced, just that efforts are made to make it lightweight

[Shreyas Srinivas]

Let me see if I can arrive at a first approximation of the problem: Given a graph of implications, we want to break cycles and topologically sort the resultant DAG

[Vlad Tsyrklevich]

Shreyas Srinivas said:

Unless we provide the tooling to reduce transitive implications, it may not be easy for authors to do this, especially in auto-generated proofs

I have some tooling upstream that will give you the transitive reduction of a graph given a CSV of the graph edges. The rest is just filtering, which I assume the authors should be capable of

[Vlad Tsyrklevich]

Shreyas Srinivas said:

Let me see if I can arrive at a first approximation of the problem: Given a graph of implications, we want to break cycles and topologically sort the resultant DAG

See scripts/transitive_reduction.rb

[Shreyas Srinivas]

can you embed it in lean such that it will throw a warning on theorems

[Terence Tao]

This sounds like something which should already be standard (e.g., in TAOCP)

[Vlad Tsyrklevich]

(There is also the opposite, scripts/transitive_closure.rb to generate the maximal list of implications)

[Shreyas Srinivas]

Lean has a nice way of doing FFI, but I think you'd find it easier to call the scripts from the shell and read the resultant output file into lean

[Vlad Tsyrklevich]

Shreyas Srinivas said:

can you embed it in lean such that it will throw a warning on theorems

It is not that fast, and more over, we already have some overlap. I think once we have tools to generate lists of implications, we can tell submitters to filter out duplicates

[Vlad Tsyrklevich]

Ah, I am remembering the timing of looking at massive unreduced data sets. For reduced graphs it's actually fairly fast. Definitely can fit in CI, even on large data sets it was <1 min.

[Shreyas Srinivas]

Terence Tao said:

This sounds like something which should already be standard (e.g., in TAOCP)

It starts out simple. But what you really need is a dynamic algorithm. as you add nodes to the graph and edges (dependencies), you need the algorithm to update its minimal and maximal implication structures. Dynamic algorithms are only good if they compute much faster than their static counterparts.

[Shreyas Srinivas]

Dynamic algorithms on graphs seem simple when you only insert nodes or edges, but things get complicated node and edge deletions are involved.

[Terence Tao]

Well the main thing I guess is to not lose an order of magnitude in the number of things Lean has to verify in order to compile everything. Losing 10% is probably no big deal though.

[Shreyas Srinivas]

It would be interesting to implement these ruby scripts in lean using the metaprogramming facilities to track dependencies among lean declarations

[Shreyas Srinivas]

We might then be able to use this graph to search and find a directed path between two statements to prove implications between new statements

[Shreyas Srinivas]

Term rewriting algorithms in lean would be an interesting experiment

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

One more thought I just had, is that we should ask that contributions are reduced to their transitive reduction (e.g. fewest number of implications). If they don't do it over all of Lean, then at least doing it among their own theorems would be useful. It may be nice to say this for now, and when there is slightly more tooling for pulling out all implications then providing a handy command to do so. I'll PR if no one objects.

https://github.com/teorth/equational_theories/pull/91

[Pietro Monticone]

I have just found a bit more time to rewrite the description of our dashboard-based project coordination in the CONTRIBUTING guide as follows:

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 Outstanding Tasks 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 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 Tasks column.
• You may only claim one task at a time. If you decide not to work on a task after claiming it, comment disclaim on the issue. This will unassign you and return the issue to the Unclaimed Outstanding Tasks 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 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 withdraw PR #PR_NUMBER on the issue. The task will return to the Claimed Tasks column, but you will remain assigned to the issue.
• To submit an updated PR after withdrawal, comment 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 awaiting-review on the PR. This will add the awaiting-review label to your PR and move the task from In Progress to the PRs 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.

Additional Guidelines and Notes

1. Please adhere to the issue claiming process. If an issue is already assigned to another contributor, refrain from working on it without prior communication with the current claimant. This ensures a collaborative and respectful workflow that values each contributor’s efforts.
2. Be aware that this contribution process is still in an experimental phase. As a result, occasional issues and inefficiencies may arise. We are committed to continuously refining the process, and your constructive feedback is highly appreciated. You can share your thoughts and suggestions on the Lean Zulip chat channel.
3. Until the integration of sufficient CI automation, the management of the project dashboard is handled manually by the maintainers. We ask for your patience and understanding as we work to keep the process running smoothly.

[Pietro Monticone]

In the next few days I'll probably do the same for the Blueprint instructions.