Merge remote-tracking branch 'upstream/nightly' into binaryRec

leanprover · Apr 24, 2024 · 1895b4c · 1895b4c
2 parents be1256f + 41697dc
commit 1895b4c
Show file tree

Hide file tree

Showing 592 changed files with 153,081 additions and 90,220 deletions.
diff --git a/.github/workflows/check-stage0.yml b/.github/workflows/check-stage0.yml
@@ -0,0 +1,27 @@
+name: Check for stage0 updates on the merge queue
+
+# We only want to run this on merge_group checks, but github uses the same
+# list of requires checks for PR → queue and queue → master, so
+# this needs to run (without doing anything) for pull_request as well.
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'merge_group'
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 2
+    - run: |
+        if git diff HEAD^..HEAD --name-only -- stage0 |
+          grep -q -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in'
+        then
+          echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi
+      shell: bash
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,6 +21,11 @@
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/runtime/io.cpp @joehendrix
+/src/Init/Data/ @semorrison
+/src/Init/Data/Array/Lemmas.lean @digama0
+/src/Init/Data/List/Lemmas.lean @digama0
+/src/Init/Data/List/BasicAux.lean @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
 /src/Lean/Elab/Tactic/RCases.lean @digama0
 /src/Init/RCases.lean @digama0
 /src/Lean/Elab/Tactic/Ext.lean @digama0
@@ -39,3 +44,4 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
+
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`.
@@ -70,18 +79,29 @@ v4.8.0 (development in progress)
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 * Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, metavariables pretty print as `?_`,
-  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
+  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
   [#3798](https://github.com/leanprover/lean4/pull/3798).
 
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
   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).
+
+* The `#guard_msgs` command now supports showing a diff between the expected and actual outputs. This feature is currently
+  disabled by default, but can be enabled with `set_option guard_msgs.diff true`. Depending on user feedback, this option
+  may default to `true` in a future version of Lean.
 
 Breaking changes:
 
@@ -112,6 +132,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/doc/examples/Certora2022/ex8.lean b/doc/examples/Certora2022/ex8.lean
@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

diff --git a/doc/examples/ICERM2022/ctor.lean b/doc/examples/ICERM2022/ctor.lean
@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
     else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
+      mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic => 
+elab "ctor" idx:num : tactic =>
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by 
+example (p : Prop) : p := by
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 1
-  exact h -- Error 
-
+  exact h -- Error
diff --git a/doc/examples/ICERM2022/meta.lean b/doc/examples/ICERM2022/meta.lean
@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     IO.println s!"{declName} : {← ppExpr val}"
-    
+
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,17 +30,17 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
+  if a < b then
     a
-  else 
+  else
     b
 
 set_option trace.Meta.debug true in
 #eval ex3 ``myMin
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `a nat fun a =>
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,15 +66,17 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `a nat fun a => do
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-       
+
 set_option trace.Meta.debug true in
 #eval ex5