Merge branch 'lean4' into update-mathlib-pr-workflow

Author: kim-em

data/community.md

@@ -83,7 +83,11 @@ These guidelines apply to the
 [Lean Zulip chat](https://leanprover.zulipchat.com/)
 and the [leanprover-community GitHub organization](https://github.com/leanprover-community/).
 
-To clarify the above: actions that can result in suspension or banning from the Lean community Zulip include harassment, discriminatory or disrespectful behavior, sustained off-topic or disruptive posts, repeated low effort posts, use of the community to complete coursework or work tasks, use of sock-puppet accounts, DM spam, unsolicited mass DMs to users, significant use of AI without attribution, posting of "slop" AI-generated code accompanied by unjustified and incorrect claims about said code, and ignoring moderator guidance. This list is not exhaustive and the maintainers retain broad discretion in user moderation.
+To clarify the above: actions that can result in suspension or banning from the Lean community Zulip include harassment, discriminatory or disrespectful behavior, sustained off-topic or disruptive posts, repeated low effort posts, use of the community to complete coursework or work tasks, use of sock-puppet accounts, DM spam, unsolicited mass DMs to users, significant use of AI without attribution, unrequested posting of "slop" AI-generated code, making unjustified and incorrect claims about AI-generated code, and ignoring moderator guidance.
+
+This is not a free code review service. Posts that amount to 'look at my project' without a specific question or prior community involvement will be removed and the poster suspended.
+
+This list is not exhaustive and the maintainers retain broad discretion in user moderation.
 
 Repeated violations will result in temporary suspensions, which will increase in length if the behavior continues. Egregious individual incidents will result in bans.
 

templates/contribute/index.md

@@ -61,6 +61,14 @@ style violations documented in this guide are welcome. Other stylistic PRs that
 approval by the authors of the affected files may be closed. We invite authors to instead discuss the proposed
 change on Zulip and, when significant consensus among reviewers is reached, to open a PR to the style guide.
 
+## Use of AI
+
+Using artificial intelligence tools to generate code is becoming more and more common. While this can be practical, their use also poses ethical, ecological, legal and social concerns. We recognise that there are strong differences in opinion on this topic, and do not enforce a strict ban. That said, while individual action alone will not address these concerns, we ask you to consider the effects of your AI use and if it is truly necessary.
+
+If you use artificial intelligence (such as, by using github's copilot mode, asking an LLM like ChatGPT or using an agent like Codex, Claude or Gemini), please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors.
+
+It is essential that you can vouch for all the code submitted in a PR, and understand all the content written by an AI. If you don't, then it is possible that the PR actually has negative value to the community, and you are expecting others to do the real work for you!
+
 ## Working on mathlib
 
 We use `git` to manage and version control `mathlib`.
@@ -154,11 +162,15 @@ Labels can only be edited directly by "GitHub collaborators", which is approxima
 However, anyone can add/remove the labels below by writing the following commands in a comment on the PR (each on its own line):
 - `awaiting-author` will add the **"awaiting-author"** label
 - `-awaiting-author` will remove the **"awaiting-author"** label
+- `awaiting-zulip` will add the **"awaiting-zulip"** label
+- `-awaiting-zulip` will remove the **"awaiting-zulip"** label. Use this once a decision has been reached and has been implemented.
 - `WIP` will add the **"WIP"** label
 - `-WIP` will remove the **"WIP"** label
 - `easy` will add the **"easy"** label
 - `-easy` will remove the **"easy"** label
-- Similarly, the labels for use by contributors upstreaming work from the downstream projects **brownian**, **carleson**, **CFT**, **FLT**, **sphere-packing** and **toric** can also be added and removed in the same way.
+- `help-wanted`, `-help-wanted`, `please-adopt`, `-please-adopt` can be used to mark a PR in need of external input.
+- Similarly, the labels for use by contributors upstreaming work from the downstream projects **brownian**, **carleson**, **CFT**, **FLT**, **infinity-cosmos**, **sphere-packing** and **toric** can also be added and removed in the same way.
+- Any topic label of the form `t-*` (e.g. `t-topology`), as well as the labels `CI` and `IMO`,  can also be added and removed in the same way. PRs are auto-labeled based on their contents, but sometimes the auto-labeling is incorrect or incomplete so this lets you manually override it. See [available topic labels](https://github.com/leanprover-community/mathlib4/labels?q=t-).
 
 This list is exhaustive.  If you would like to add a different label, please, bring it up on Zulip!
 

templates/contribute/style.md

@@ -740,3 +740,10 @@ We allow, but discourage, contributors from simultaneously renaming declarations
 In this case, no deprecation attribute is required for X, but it is for W.
 
 Named instances do not require deprecations. Deprecated declarations can be deleted after 6 months.
+
+### Avoid `nonrec`
+
+The `nonrec` keyword tells Lean to assume that apparently recursive calls in the declaration body
+are not actually recursive, and instead look for declarations in other namespaces with the same name.
+Avoid `nonrec` when the recursive call conflicts with another declaration *in a namespace*, because then adding the namespace to that declaration is more informative (to both Lean and the user). If it conflicts with a declaration in the root namespace, then both `nonrec` and `_root_.[...]` are acceptable. Sometimes avoiding `nonrec` requires forgoing the use of dot notation within the body of that declaration.
+(There are currently many places in Mathlib that break this rule.)

templates/contribute/tags_and_branches.md

@@ -1,6 +1,6 @@
 # The Lean Github ecosystem
 
-Documentation of the branches, tags, and CI workflows relevant for making pull requests to Lean, Std, and
+Documentation of the branches, tags, and CI workflows relevant for making pull requests to Lean, Batteries, and
 Mathlib.
 
 * [Things you need to know](#things-you-need-to-know) is relevant for everyone
@@ -35,23 +35,23 @@ Mathlib.
 * Every PR automatically receives a toolchain after it builds successfully. The PR will then have label `toolchain-available`.
   To use PR #NNNN in a project, your `lean-toolchain` file should contain
   `leanprover/lean4-pr-releases:pr-release-NNNN`.
-* For any PR that potentially affects Std or Mathlib, you should base your PR off the HEAD of the `nightly-with-mathlib` branch.
+* For any PR that potentially affects Batteries or Mathlib, you should base your PR off the HEAD of the `nightly-with-mathlib` branch.
   In that case, a `lean-pr-testing-NNNN` Mathlib branch is created, described in detail below, and results from this branch are
   reported via comments in the PR discussion.
 
-### `leanprover/std4` (aka 'Std')
+### `leanprover-community/batteries` (aka 'Batteries')
 
 * Development occurs on `main`.
-* Std uses the latest stable release or release candidate in its `lean-toolchain`.
+* Batteries uses the latest stable release or release candidate in its `lean-toolchain`.
   * Because we release `v4.X+1.0-rc1` immediately after releasing `v4.X.0`,
-    Std is only very briefly on stable releases.
+    Batteries is only very briefly on stable releases.
 * The first commit on `main` which uses a new toolchain is tagged with the version number of that
   toolchain (e.g. `v4.2.0`).
 * There is a branch `stable` which follows the `v4.X.0` tags.
-* Std has a branch `bump/v4.X.0` for the upcoming stable release of Lean,
+* Batteries has a branch `bump/v4.X.0` for the upcoming stable release of Lean,
   * which contains adaptations for breaking changes that have been approved by the maintainers
   * and which will be using a `leanprover-lean4:nightly-YYYY-MM-DD` toolchain.
-* Std has a branch `nightly-testing` which
+* Batteries has a branch `nightly-testing` which
   * uses a recent nightly release (this is updated automatically)
   * has all commits from `main` merged into it automatically
   * may have any changes from `bump/v4.X.0` merged into it manually
@@ -64,53 +64,53 @@ Mathlib.
   * Thus if `nightly-testing-YYYY-MM-DD` exists, we know that on it:
     * the `lean-toolchain` is `leanprover/lean4:nightly-YYYY-MM-DD`, and
     * CI succeeds.
-* When changes are required to Std to adapt to a breaking change in Lean,
+* When changes are required to Batteries to adapt to a breaking change in Lean,
   you will need to make a branch, and later open a PR from that branch.
   (Note that the steps below happen automatically at Mathlib,
-  but need to be done manually for Std.)
+  but need to be done manually for Batteries.)
   * If the change was made in `leanprover/lean4#NNNN`,
-    then the Std adaptation branch should be called `lean-pr-testing-NNNN`.
-  * The Std adaptation branch should be based off the tag `nightly-testing-YYYY-MM-DD`
+    then the Batteries adaptation branch should be called `lean-pr-testing-NNNN`.
+  * The Batteries adaptation branch should be based off the tag `nightly-testing-YYYY-MM-DD`
     where `YYYY-MM-DD` is the date of the nightly release that your Lean PR is based off.
   * If the `nightly-testing-YYYY-MM-DD` tag does not yet exist, you will need to wait
     (and possibly move forward to a subsequent nightly).
     Contact @semorrison for assistance if needed.
-  * Ideally you will push the `lean-pr-testing-NNNN` branch to the main Std repository;
+  * Ideally you will push the `lean-pr-testing-NNNN` branch to the main Batteries repository;
     we can provide write access if needed.
   * The `lean-toolchain` on this branch must contain `leanprover/lean4-pr-releases:pr-release-NNNN`.
   * You may open a PR from the `lean-pr-testing-NNNN` branch, either before or after
     making the required adaptations.
   * When opening the PR, remember to set the base branch to `nightly-testing`.
   * Please label the PR with the `v4.X.0` and 'depends on core changes' labels.
     (Or ask for this to be done if you don't have write access.)
-  * Once the Lean PR has been merged and published in a nightly release, the Std adaptation PR
+  * Once the Lean PR has been merged and published in a nightly release, the Batteries adaptation PR
     * should have its `lean-toolchain` updated to `leanprover/lean4:nightly-YYYY-MM-DD`
     * its changes may be merged manually into `nightly-testing` as needed to keep `nightly-testing`
       working (do not change the base and merge the PR, we still need it).
-  * Once the Std adaptation PR has been approved,
+  * Once the Batteries adaptation PR has been approved,
     a maintainer will merge it into `bump/v4.X.0` (not `nightly-testing-YYYY-MM-DD`).
 * It is always allowed to merge `bump/v4.X.0` into `nightly-testing`, but not conversely.
   (Changes to `bump/v4.X.0` have been reviewed, but changes to `nightly-testing` may not have been.)
-* When it is time to update Std to a new Lean release,
+* When it is time to update Batteries to a new Lean release,
   *hopefully* all that is required is to make a new PR
   consisting of squash merging `bump/v4.X.0` to `main`.
 
 ### `leanprover-community/mathlib4` (aka 'Mathlib')
 
-* Everything said above about Std applies to Mathlib, except:
+* Everything said above about Batteries applies to Mathlib, except:
   * Development occurs on `master`.
   * PRs to Mathlib should be made from forks. Mathlib's `.olean` cache now works with PRs from forks.
 * The `lean-pr-testing-NNNN`, `nightly-testing`, `nightly-testing-*` tags, and `bump/v4*` branches
   all live at `leanprover-community/mathlib4-nightly-testing`, which is a fork of mathlib4.
   If you will regularly need write access to these branches, you can ask in the
   [nightly-testing channel](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing)
   on Zulip to be added to the `nightly-testing` GitHub team.
-* Note that the `nightly-testing` branch of Mathlib may use the `nightly-testing` branch of Std as required.
-* Similarly a `bump/v4.X.0` branch of Mathlib may use the `bump/v4.X.0` branch of Std as required.
+* Note that the `nightly-testing` branch of Mathlib may use the `nightly-testing` branch of Batteries as required.
+* Similarly a `bump/v4.X.0` branch of Mathlib may use the `bump/v4.X.0` branch of Batteries as required.
 * Branches `lean-pr-testing-NNNN` are automatically created for any Lean PR that passes CI,
-  and is based off a nightly release. (Unlike for Std, where they must be created manually.)
-* Mathlib adaptation PRs on `lean-pr-testing-NNNN` branches may need to change the Std dependency
-  to use a `lean-pr-testing-NNNN` branch of Std, if Std also experiences breakages.
+  and is based off a nightly release. (Unlike for Batteries, where they must be created manually.)
+* Mathlib adaptation PRs on `lean-pr-testing-NNNN` branches may need to change the Batteries dependency
+  to use a `lean-pr-testing-NNNN` branch of Batteries, if Batteries also experiences breakages.
 
 ### Mathlib nightly and bump branches
 
@@ -150,7 +150,7 @@ To make this process as smooth as possible, we follow the following procedure:
 * For every PR to Lean, we attempt to run Mathlib CI against the resulting toolchain.
 * For this to work, you will need to rebase your PR onto the `nightly-with-mathlib` branch.
   The `nightly-with-mathlib` branch points to the latest nightly lean release which passes mathlib CI,
-  and for which a `nightly-testing-YYYY-MM-DD` tag exists on Mathlib (and possibly Std).
+  and for which a `nightly-testing-YYYY-MM-DD` tag exists on Mathlib (and possibly Batteries).
 * The bot will create a `lean-pr-testing-NNNN` branch at `leanprover-community/mathlib4-nightly-testing`
   from the `nightly-testing-YYYY-MM-DD` tag, or push an empty commit to it if it already exists.
 * Subsequent CI results from that Mathlib branch will be reported back to the Lean PR
@@ -164,4 +164,4 @@ To make this process as smooth as possible, we follow the following procedure:
   to wait for `nightly-with-mathlib` to be updated and rebase onto that.
 
 
-<img src="img/tags_and_branches.png" alt="Overview of branches at Mathlib/Std" width="80%"/>
+<img src="img/tags_and_branches.png" alt="Overview of branches at Mathlib/Batteries" width="80%"/>