From dcf74b0d897e31adbd7ef82f10c06769be88959c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 8 May 2024 15:04:25 +1000 Subject: [PATCH] chore: Std -> Batteries renaming (#4108) --- .github/ISSUE_TEMPLATE/bug_report.md | 2 +- .github/workflows/pr-release.yml | 32 ++++++++++++------------- doc/BoolExpr.lean | 2 +- doc/dev/release_checklist.md | 16 ++++++------- doc/monads/states.lean | 2 +- src/Init/Data/Array/Lemmas.lean | 2 +- src/Init/Data/List/Lemmas.lean | 7 ------ src/Init/Omega/Coeffs.lean | 2 +- src/Init/Tactics.lean | 4 ++-- src/Lean/Meta/Tactic/LibrarySearch.lean | 2 +- tests/lean/librarySearch.lean | 4 ++-- 11 files changed, 34 insertions(+), 41 deletions(-) diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md index 0e75ac87ec..2c66085703 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -11,7 +11,7 @@ assignees: '' * [ ] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues). - * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4. + * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries. ### Description diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index ef5a2f8bba..1c15eda08e 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -126,11 +126,11 @@ jobs: if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then echo "The merge base of this PR coincides with the nightly release" - STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" + BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")" MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" - if [[ -n "$STD_REMOTE_TAGS" ]]; then - echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." + if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then + echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." MESSAGE="" if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then @@ -140,8 +140,8 @@ jobs: MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now." fi else - echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." - MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now." + echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." + MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now." fi else @@ -151,7 +151,7 @@ jobs: git -C lean4.git fetch origin nightly-with-mathlib NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")" - MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." + MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." fi if [[ -n "$MESSAGE" ]]; then @@ -223,27 +223,27 @@ jobs: description: description, }); - # We next automatically create a Std branch using this toolchain. - # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean - # Instead this is taken care of by Mathlib CI, which will fail if Std fails. + # We next automatically create a Batteries branch using this toolchain. + # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean + # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails. - name: Cleanup workspace if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' run: | sudo rm -rf ./* - # Checkout the Std repository with all branches - - name: Checkout Std repository + # Checkout the Batteries repository with all branches + - name: Checkout Batteries repository if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' uses: actions/checkout@v3 with: - repository: leanprover/std4 + repository: leanprover-community/batteries token: ${{ secrets.MATHLIB4_BOT }} ref: nightly-testing fetch-depth: 0 # This ensures we check out all tags and branches. - name: Check if tag exists if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' - id: check_std_tag + id: check_batteries_tag run: | git config user.name "leanprover-community-mathlib4-bot" git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" @@ -251,7 +251,7 @@ jobs: if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then BASE="nightly-testing-${MOST_RECENT_NIGHTLY}" else - echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'." + echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'." BASE=nightly-testing fi @@ -268,7 +268,7 @@ jobs: else echo "Branch already exists, pushing an empty commit." git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} - # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes. + # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes. # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.) git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" @@ -321,7 +321,7 @@ jobs: git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain git add lean-toolchain - sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean + sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean git add lakefile.lean git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" else diff --git a/doc/BoolExpr.lean b/doc/BoolExpr.lean index ae9d02cbd4..b577ecc33e 100644 --- a/doc/BoolExpr.lean +++ b/doc/BoolExpr.lean @@ -1,4 +1,4 @@ -open Std +open Batteries open Lean inductive BoolExpr where diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 90638b041a..2e0b06b576 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example. - Toolchain bump PR - Create and push the tag - Merge the tag into `stable` - - [Std](https://github.com/leanprover-community/std4) + - [Batteries](https://github.com/leanprover-community/batteries) - No dependencies - Toolchain bump PR - Create and push the tag - Merge the tag into `stable` - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4) - - Dependencies: `Std` + - Dependencies: `Batteries` - Note on versions and branches: - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`, which does not refer to the toolchain being used. @@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example. - Toolchain bump PR - Create and push the tag, following the version convention of the repository - [Aesop](https://github.com/leanprover-community/aesop) - - Dependencies: `Std` + - Dependencies: `Batteries` - Toolchain bump PR including updated Lake manifest - Create and push the tag - Merge the tag into `stable` @@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example. - Create and push the tag - There is no `stable` branch; skip this step - [Mathlib](https://github.com/leanprover-community/mathlib4) - - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph` + - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph` - Toolchain bump PR notes: - In addition to updating the `lean-toolchain` and `lakefile.lean`, in `.github/workflows/build.yml.in` in the `lean4checker` section update the line @@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. - Decide which nightly release you want to turn into a release candidate. We will use `nightly-2024-02-29` in this example. -- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly. - - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29` +- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly. + - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29` in their `lean-toolchain`. - The steps required to reach that state are beyond the scope of this checklist, but see below! - Create the release branch from this nightly tag: @@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. - We do this for the same list of repositories as for stable releases, see above. As above, there are dependencies between these, and so the process above is iterative. It greatly helps if you can merge the `bump/v4.7.0` PRs yourself! - - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag + - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push. - Make an announcement! @@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work # Preparing `bump/v4.7.0` branches While not part of the release process per se, -this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions. +this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions. Please read https://leanprover-community.github.io/contribute/tags_and_branches.html diff --git a/doc/monads/states.lean b/doc/monads/states.lean index 0265fbe6c6..85ef83104f 100644 --- a/doc/monads/states.lean +++ b/doc/monads/states.lean @@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost current player, and it has a random generator. -/ -open Std (HashMap) +open Batteries (HashMap) abbrev TileIndex := Nat × Nat -- a 2D index inductive TileState where diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 900b23b4fc..a3356b7410 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -943,7 +943,7 @@ theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h : omega termination_by stop - start --- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Std.Data.Array.Init.Monadic` +-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic` theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) : any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by dsimp [any, anyM, Id.run] diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 00070de044..a694cce91e 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -16,13 +16,6 @@ namespace List open Nat -/-! -# Bootstrapping theorems for lists - -These are theorems used in the definitions of `Std.Data.List.Basic` and tactics. -New theorems should be added to `Std.Data.List.Lemmas` if they are not needed by the bootstrap. --/ - attribute [simp] concat_eq_append append_assoc @[simp] theorem get?_nil : @get? α [] n = none := rfl diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean index ba1ca48e2c..57e35f6705 100644 --- a/src/Init/Omega/Coeffs.lean +++ b/src/Init/Omega/Coeffs.lean @@ -68,7 +68,7 @@ abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs /-- Shim for `.enum.find?`. -/ abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat := -- List.findIdx? f xs - -- We could avoid `Std.Data.List.Basic` by using the less efficient: + -- We could avoid `Batteries.Data.List.Basic` by using the less efficient: xs.enum.find? (f ·.2) |>.map (·.1) /-- Shim for `IntList.bmod`. -/ abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index bf58d089ca..57dd085ed3 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -835,7 +835,7 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic /-- `repeat tac` repeatedly applies `tac` to the main goal until it fails. That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited. -The `Std` library provides `repeat'` which repeats separately in each subgoal. +The `Batteries` library provides `repeat'` which repeats separately in each subgoal. -/ syntax "repeat " tacticSeq : tactic macro_rules @@ -1266,7 +1266,7 @@ Optional arguments passed via a configuration argument as `solve_by_elim (config but it is often useful to change to `.reducible`, so semireducible definitions will not be unfolded when trying to apply a lemma. -See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options +See also the doc-comment for `Lean.Meta.Tactic.Backtrack.BacktrackConfig` for the options `proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`. Both `apply_assumption` and `apply_rules` are implemented via these hooks. -/ diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean index f7b23466c8..3145c38e07 100644 --- a/src/Lean/Meta/Tactic/LibrarySearch.lean +++ b/src/Lean/Meta/Tactic/LibrarySearch.lean @@ -160,7 +160,7 @@ An exception ID that indicates further speculation on candidate lemmas should st and current results should be returned. -/ private builtin_initialize abortSpeculationId : InternalExceptionId ← - registerInternalExceptionId `Std.Tactic.LibrarySearch.abortSpeculation + registerInternalExceptionId `Lean.Meta.LibrarySearch.abortSpeculation /-- Called to abort speculative execution in library search. diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean index 3688efadb0..474828fb15 100644 --- a/tests/lean/librarySearch.lean +++ b/tests/lean/librarySearch.lean @@ -1,7 +1,7 @@ -- Enable this option for tracing: --- set_option trace.Tactic.stdLibrarySearch true +-- set_option trace.Tactic.librarySearch true -- And this option to trace all candidate lemmas before application. --- set_option trace.Tactic.stdLibrarySearch.lemmas true +-- set_option trace.Tactic.librarySearch.lemmas true -- Many of the tests here are quite volatile, -- and when changes are made to `solve_by_elim` or `exact?`,