new task list

Stream: Infinity-Cosmos

[Emily Riehl]

Thanks to @Pietro Monticone I've set up a new task list following the updated workflow described here:

https://github.com/emilyriehl/infinity-cosmos/blob/main/CONTRIBUTING.md

It's not clear whether I've done this optimally. In particular, I wasn't certain how to
(i) include work in progress
(ii) include work where the task is more focused on PRing something to mathlib than PRing something to our repository and
(iii) indicate dependencies among tasks. Right now I've done this in the text description, which may also indicate how serious the dependencies are.

Suggestions about restructuring or other edits are very welcome.

For any of the tasks, if it would be helpful to discuss more details, please let me know. I have been working on expanding the blueprint but have not done so uniformly so some proofs are given with more detail than others. Please feel free to ask me to flesh out anything that is unclear.

[Pietro Monticone]

1. Work in Progress

If @username is working on a task #X and opened a PR #Y to solve it, then you could just treat it as any other task:

1. Create the related issue
2. @username claims it (or you assign @username)
3. @username propose #Y

2. Upstream Tasks

Unfortunately cross-repository automatic issue-closing via PR merges is not implemented by default in GitHub so we cant't link an InfinityCosmos issue to a Mathlib PR directly, but I could implement it at some point in the future if we convince ourselves it's really necessary.

For the time being, you could just:

1. Create a label named upstream here and apply it to the upstreaming task #X in order to effectively distinguish it from ordinary tasks
2. Manually close as completed #X when the related Mathlib PR gets merged

3. Task Dependencies

If task #X depends on task #Y then you can classify #Y ("child" task) as a sub-issue of #X ("parent" task).

For example, since cosmos#116 depends on cosmos#112, I have just classified cosmos#112 as a sub-issue of cosmos#116.

112-child-task

116-parent-task