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

…r-tactic
leanprover · Apr 18, 2024 · a616565 · a616565
2 parents 293070b + df1e6ba
commit a616565
Show file tree

Hide file tree

Showing 506 changed files with 129,507 additions and 80,549 deletions.
diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml
@@ -10,7 +10,7 @@ jobs:
 
     - name: Verify .lean files start with a copyright header.
       run: |
-        FILES=$(find . -type d \( -path "./tests" -o -path "./doc" -o -path "./src/lake/examples" -o -path "./src/lake/tests" -o -path "./build" -o -path "./nix" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+        FILES=$(find ./src -type d \( -path "./src/lake/examples" -o -path "./src/lake/tests" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
         if [ -n "$FILES" ]; then
           echo "Found .lean files which do not have a copyright header:"
           echo "$FILES"

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
@@ -150,7 +150,7 @@ jobs:
             git -C lean4.git log -10 origin/master
 
             git -C lean4.git fetch origin nightly-with-mathlib 
-            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "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\`."
           fi
 

diff --git a/CODEOWNERS b/CODEOWNERS
@@ -21,3 +21,23 @@
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/runtime/io.cpp @joehendrix
+/src/Lean/Elab/Tactic/RCases.lean @digama0
+/src/Init/RCases.lean @digama0
+/src/Lean/Elab/Tactic/Ext.lean @digama0
+/src/Init/Ext.lean @digama0
+/src/Lean/Elab/Tactic/Simpa.lean @digama0
+/src/Lean/Elab/Tactic/NormCast.lean @digama0
+/src/Lean/Meta/Tactic/NormCast.lean @digama0
+/src/Lean/Meta/Tactic/TryThis.lean @digama0
+/src/Lean/Elab/Tactic/SimpTrace.lean @digama0
+/src/Lean/Elab/Tactic/NoMatch.lean @digama0
+/src/Lean/Elab/Tactic/ShowTerm.lean @digama0
+/src/Lean/Elab/Tactic/Repeat.lean @digama0
+/src/Lean/Meta/Tactic/Repeat.lean @digama0
+/src/Lean/Meta/CoeAttr.lean @digama0
+/src/Lean/Elab/GuardMsgs.lean @digama0
+/src/Lean/Elab/Tactic/Guard.lean @digama0
+/src/Init/Guard.lean @digama0
+/src/Lean/Server/CodeActions/ @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
+
diff --git a/RELEASES.md b/RELEASES.md
@@ -21,7 +21,7 @@ v4.8.0 (development in progress)
 
 * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
 
-* Funcitonal induction principles.
+* Functional induction principles.
 
   Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
 
@@ -57,6 +57,15 @@ v4.8.0 (development in progress)
   ```
   is recognized without having to say `termination_by arr.size - i`.
 
+* Shorter instances names. There is a new algorithm for generating names for anonymous instances.
+  Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%.
+  With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters.
+  The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm.
+  While the new algorithm produces names that are 1.2% less unique,
+  it avoids cross-project collisions by adding a module-based suffix
+  when it does not refer to declarations from the same "project" (modules that share the same root).
+  PR [#3089](https://github.com/leanprover/lean4/pull/3089).
+
 * Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
   rather than `{a := x, b := y, c := z}`.
   This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
@@ -80,8 +89,15 @@ v4.8.0 (development in progress)
   Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
   rather than `Nat.zero` and `Nat.succ n`.
   Added option `tactic.customEliminators` to control whether to use custom eliminators.
-  [#3629](https://github.com/leanprover/lean4/pull/3629) and
-  [#3655](https://github.com/leanprover/lean4/pull/3655).
+  Added a hack for `rcases`/`rintro`/`obtain` to use the custom eliminator for `Nat`.
+  [#3629](https://github.com/leanprover/lean4/pull/3629),
+  [#3655](https://github.com/leanprover/lean4/pull/3655), and
+  [#3747](https://github.com/leanprover/lean4/pull/3747).
+
+* The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
+  For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,
+  and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
+  PR [#3883](https://github.com/leanprover/lean4/pull/3883).
 
 Breaking changes:
 
@@ -112,6 +128,12 @@ fact.def :
 
 * The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
 
+* The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.
+
+* The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
+
+* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
+
 v4.7.0
 ---------
 

diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md
@@ -21,7 +21,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - Reconcile discrepancies in the `v4.6.0` section,
     usually via copy and paste and a commit to `releases/v4.6.0`.
 - `git tag v4.6.0`
-- `git push origin v4.6.0`
+- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
     looking for the `v4.6.0` tag.
@@ -34,48 +34,76 @@ We'll use `v4.6.0` as the intended release version as a running example.
     (e.g. `v4.6.0-rc1`), and quickly sanity check.
 - Next, we will move a curated list of downstream repos to the latest stable release.
   - For each of the repositories listed below:
-    - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`.
-      The PR title should be "chore: bump toolchain to v4.6.0".
-      Since the `v4.6.0` release should be functionally identical to the last release candidate,
-      which the repository should already be on, this PR is a no-op besides changing the toolchain.
-    - Once this is merged, create the tag `v4.6.0` from `master`/`main` and push it.
-    - Merge the tag `v4.6.0` into the stable branch.
+    - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
+      - Update the toolchain file
+      - In the Lakefile, if there are dependencies on specific version tags of dependencies that you've already pushed as part of this process, update them to the new tag.
+        If they depend on `main` or `master`, don't change this; you've just updated the dependency, so it will work and be saved in the manifest
+      - Run `lake update`
+      - The PR title should be "chore: bump toolchain to v4.6.0".
+    - Merge the PR once CI completes.
+    - Create the tag `v4.6.0` from `master`/`main` and push it.
+    - Merge the tag `v4.6.0` into the `stable` branch and push it.
   - We do this for the repositories:
     - [lean4checker](https://github.com/leanprover/lean4checker)
-      - `lean4checker` uses a different version tagging scheme: use `toolchain/v4.6.0` rather than `v4.6.0`.
-    - [Std](https://github.com/leanprover-community/repl)
+      - No dependencies
+      - Note: `lean4checker` uses a different version tagging scheme: use `toolchain/v4.6.0` rather than `v4.6.0`.
+      - Toolchain bump PR
+      - Create and push the tag
+      - Merge the tag into `stable`
+    - [Std](https://github.com/leanprover-community/std4)
+      - No dependencies
+      - Toolchain bump PR
+      - Create and push the tag
+      - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
-      - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
-        which does not refer to the toolchain being used.
-      - Make a new release in this sequence after merging the toolchain bump PR.
-      - `ProofWidgets` does not maintain a `stable` branch.
+      - Dependencies: `Std`
+      - 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.
+        - Make a new release in this sequence after merging the toolchain bump PR.
+        - `ProofWidgets` does not maintain a `stable` branch.
+      - Toolchain bump PR
+      - Create and push the tag, following the version convention of the repository
     - [Aesop](https://github.com/leanprover-community/aesop)
+      - Dependencies: `Std`
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - Merge the tag into `stable`
+    - [doc-gen4](https://github.com/leanprover/doc-gen4)
+      - Dependencies: exist, but they're not part of the release workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
+    - [import-graph](https://github.com/leanprover-community/import-graph)
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [Mathlib](https://github.com/leanprover-community/mathlib4)
-      - In addition to updating the `lean-toolchain` and `lakefile.lean`,
-        in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
-        `git checkout toolchain/v4.6.0` to the appropriate tag,
-        and then run `.github/workflows/mk_build_yml.sh`.
+      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `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
+          `git checkout toolchain/v4.6.0` to the appropriate tag,
+          and then run `.github/workflows/mk_build_yml.sh`. Coordinate with
+          a Mathlib maintainer to get this merged.
+        - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
+        - Create and push the tag
+        - Create a new branch from the tag, push it, and open a pull request against `stable`.
+          Coordinate with a Mathlib maintainer to get this merged.
     - [REPL](https://github.com/leanprover-community/repl)
+      - Dependencies: `Mathlib` (for test code)
       - Note that there are two copies of `lean-toolchain`/`lakefile.lean`:
-        in the root, and in `test/Mathlib/`.
-  - Note that there are dependencies between these packages:
-    you should update the lakefile so that you are using the `v4.6.0` tag of upstream repositories
-    (or the sequential tag for `ProofWidgets4`), and run `lake update` before committing.
-  - This means that this process is sequential; each repository must have its bump PR merged,
-    and the new tag pushed, before you can make the PR for the downstream repositories.
-    - `lean4checker` has no dependencies
-    - `Std` has no dependencies
-    - `Aesop` depends on `Std`
-    - `ProofWidgets4` depends on `Std`
-    - `Mathlib` depends on `Aesop`, `ProofWidgets4`, and `lean4checker` (and transitively on `Std`)
-    - `REPL` depends on `Mathlib` (this dependency is only for testing).
+        in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - Merge the tag into `stable`
 - Merge the release announcement PR for the Lean website - it will be deployed automatically
 - Finally, make an announcement!
   This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
   Please see previous announcements for suggested language.
   You will want a few bullet points for main topics from the release notes.
   Link to the blog post from the Zulip announcement.
-  Please also make sure that whoever is handling social media knows the release is out.
+- Make sure that whoever is handling social media knows the release is out.
 
 ## Optimistic(?) time estimates:
 - Initial checks and push the tag: 30 minutes.

diff --git a/script/collideProfiles.lean b/script/collideProfiles.lean
@@ -0,0 +1,28 @@
+import Lean.Util.Profiler
+
+/-!
+
+Usage:
+```sh
+lean --run ./script/collideProfiles.lean **/*.lean.json ... > merged.json
+```
+
+Merges multiple `trace.profiler.output` profiles into a single one while deduplicating samples with
+the same stack. This is useful for building cumulative profiles of medium-to-large projects because
+Firefox Profiler cannot handle hundreds of tracks and the deduplication will also ensure that the
+profile is small enough for uploading.
+
+As ordering of samples is not meaningful after this transformation, only "Call Tree" and "Flame
+Graph" are useful for such profiles.
+-/
+
+open Lean
+
+def main (args : List String) : IO Unit := do
+  let profiles ← args.toArray.mapM fun path => do
+    let json ← IO.FS.readFile ⟨path⟩
+    let profile ← IO.ofExcept $ Json.parse json
+    IO.ofExcept <| fromJson? profile
+  -- NOTE: `collide` should not be interpreted
+  let profile := Firefox.Profile.collide profiles
+  IO.println <| Json.compress <| toJson profile
diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
@@ -20,8 +20,29 @@ def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α)
 
 export Functor (discard)
 
+/--
+An `Alternative` functor is an `Applicative` functor that can "fail" or be "empty"
+and a binary operation `<|>` that “collects values” or finds the “left-most success”.
+
+Important instances include
+* `Option`, where `failure := none` and `<|>` returns the left-most `some`.
+* Parser combinators typically provide an `Applicative` instance for error-handling and
+  backtracking.
+  
+Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
+-/
+-- NB: List instance is in mathlib. Once upstreamed, add
+-- * `List`, where `failure` is the empty list and `<|>` concatenates.
 class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
+  /--
+  Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
+  from failures. See `Alternative` for more details.
+  -/
   failure : {α : Type u} → f α
+  /--
+  Depending on the `Alternative` instance, collects values or recovers from `failure`s by
+  returning the leftmost success. Can be written using the `<|>` operator syntax.
+  -/
   orElse  : {α : Type u} → f α → (Unit → f α) → f α
 
 instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orElse⟩
@@ -30,9 +51,15 @@ variable {f : Type u → Type v} [Alternative f] {α : Type u}
 
 export Alternative (failure)
 
+/--
+If the proposition `p` is true, does nothing, else fails (using `failure`).
+-/
 @[always_inline, inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
   if p then pure () else failure
 
+/--
+Returns `some x` if `f` succeeds with value `x`, else returns `none`.
+-/
 @[always_inline, inline] def optional (x : f α) : f (Option α) :=
   some <$> x <|> pure none
 

diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
@@ -12,6 +12,15 @@ open Function
 @[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
   rfl
 
+/--
+The `Functor` typeclass only contains the operations of a functor.
+`LawfulFunctor` further asserts that these operations satisfy the laws of a functor,
+including the preservation of the identity and composition laws:
+```
+id <$> x = x
+(h ∘ g) <$> x = h <$> g <$> x
+```
+-/
 class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
   map_const          : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β
   id_map   (x : f α) : id <$> x = x
@@ -24,6 +33,16 @@ attribute [simp] id_map
 @[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
   id_map x
 
+/--
+The `Applicative` typeclass only contains the operations of an applicative functor.
+`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor:
+```
+pure id <*> v = v
+pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
+pure f <*> pure x = pure (f x)
+u <*> pure y = pure (· y) <*> u
+```
+-/
 class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where
   seqLeft_eq  (x : f α) (y : f β)     : x <* y = const β <$> x <*> y
   seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
@@ -42,6 +61,18 @@ attribute [simp] map_pure seq_pure
 @[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x := by
   simp [pure_seq]
 
+/--
+The `Monad` typeclass only contains the operations of a monad.
+`LawfulMonad` further asserts that these operations satisfy the laws of a monad,
+including associativity and identity laws for `bind`:
+```
+pure x >>= f = f x
+x >>= pure = x
+x >>= f >>= g = x >>= (fun x => f x >>= g)
+```
+
+`LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
+-/
 class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where
   bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
   bind_map       {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x

diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
@@ -235,13 +235,13 @@ end StateT
 
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    dsimp only [EStateM.instMonad, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)