Merge branch 'master' of https://github.com/leanprover/lean4 into nor…

…malize_crlf

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,9 +9,15 @@ assignees: ''
 
 ### Prerequisites
 
-* [ ] 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.
+Please put an X between the brackets as you perform the following steps:
+
+* [ ] 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 Mathlib or Batteries.
+* [ ] Test your test case against the latest nightly release, for example on
+      https://live.lean-lang.org/#project=lean-nightly
+      (You can also use the settings there to switch to “Lean nightly”)
 
 ### Description
 
@@ -33,8 +39,8 @@ assignees: ''
 
 ### Versions
 
-[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
-[OS version]
+[Output of `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
 
 ### Additional Information
 

.github/workflows/ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -41,12 +40,18 @@ jobs:
     steps:
       - name: Run quick CI?
         id: set-quick
-        env:
-          quick: ${{
-            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
-           }}
+        # We do not use github.event.pull_request.labels.*.name here because
+        # re-running a run does not update that list, and we do want to be able to
+        # rerun the workflow run after settings the `full-ci` label.
         run: |
-          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
+          if [ "${{ github.event_name }}" == 'pull_request' ]
+          then
+            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
+          else
+            echo "quick=false" >> "$GITHUB_OUTPUT"
+          fi
+        env:
+          GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix

.github/workflows/nix-ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:

.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,35 +223,35 @@ 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"
 
           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

.github/workflows/restart-on-label.yml

@@ -0,0 +1,31 @@
+name: Restart by label
+on:
+  pull_request_target:
+    types:
+      - unlabeled
+      - labeled
+jobs:
+  restart-on-label:
+    runs-on: ubuntu-latest
+    if: contains(github.event.label.name, 'full-ci')
+    steps:
+    - run: |
+        # Finding latest CI workflow run on current pull request
+        # (unfortunately cannot search by PR number, only base branch,
+        # and that is't even unique given PRs from forks, but the risk
+        # of confusion is low and the danger is mild)
+        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
+          --limit 1 --json databaseId --jq '.[0].databaseId')
+        echo "Run id: ${run_id}"
+        gh run view "$run_id"
+        echo "Cancelling (just in case)"
+        gh run cancel "$run_id" || echo "(failed)"
+        echo "Waiting for 10s"
+        sleep 10
+        echo "Rerunning"
+        gh run rerun "$run_id"
+      shell: bash
+      env:
+        head_ref: ${{ github.head_ref }}
+        GH_TOKEN: ${{ github.token }}
+        GH_REPO: ${{ github.repository }}

RELEASES.md

@@ -11,7 +11,18 @@ of each version.
 v4.9.0 (development in progress)
 ---------
 
-v4.8.0 
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
@@ -144,6 +155,18 @@ fact.def :
 
 * `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
 
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
 v4.7.0
 ---------
 

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-open Std
+open Batteries
 open Lean
 
 inductive BoolExpr where

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
 

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

src/Init.lean

@@ -34,3 +34,4 @@ import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
 import Init.MacroTrace
+import Init.Grind

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]

src/Init/Data/Array/Subarray.lean

@@ -15,14 +15,14 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array]
+@[deprecated Subarray.array (since := "2024-04-13")]
 abbrev Subarray.as (s : Subarray α) : Array α := s.array
 
-@[deprecated Subarray.start_le_stop]
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
-@[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 

src/Init/Data/BitVec/Basic.lean

@@ -34,7 +34,8 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
+@[deprecated (since := "2024-04-12")]
+protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
@@ -73,7 +74,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-@[deprecated isLt]
+@[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
 /-- Theorem for normalizing the bit vector literal representation. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -184,4 +184,18 @@ theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
 
+/-! ### Inequalities (le / lt) -/
+
+theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by
+  simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, ← decide_not,
+    Nat.not_le, decide_eq_decide]
+  rw [Nat.mod_eq_of_lt (by omega)]
+  omega
+
+theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
+  simp [BitVec.ule, BitVec.ult, ← decide_not]
+
+theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
+  simp [ule_eq_not_ult, ult_eq_not_carry]
+
 end BitVec