perf: use structural equality at ACLt

closes #3705

test: for issue

.github/workflows/ci.yml

@@ -62,7 +62,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": false,
                 "quick": false,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -76,7 +76,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": true,
                 "quick": true,
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
@@ -98,7 +98,8 @@ jobs:
                 // exclude seriously slow tests
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
               },
-              {
+              // TODO: suddenly started failing in CI
+              /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
                 "quick": false,
@@ -106,7 +107,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
                 // exclude seriously slow/problematic tests (laketests crash)
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },
+              },*/
               {
                 "name": "macOS",
                 "os": "macos-latest",
@@ -140,12 +141,10 @@ jobs:
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
-                // also, the liasolver test hits “too many exported symbols”
-                "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
+                "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
-                // TEMP while compiler tests are deactivated
-                "binary-check": "true"
+                "binary-check": "ldd"
               },
               {
                 "name": "Linux aarch64",
@@ -155,7 +154,7 @@ jobs:
                 "quick": false,
                 "cross": true,
                 "cross_target": "aarch64-unknown-linux-gnu",
-                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
+                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
               },
@@ -253,7 +252,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
+        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -384,8 +383,14 @@ jobs:
           cd build/stage1
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
-          ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: build/stage1/test-results.xml
+        # prefix `if` above with `always` so it's run even if tests failed
+        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
@@ -447,9 +452,10 @@ jobs:
     name: Build matrix complete
     runs-on: ubuntu-latest
     needs: build
-    if: ${{ always() }}
+    # mark as merely cancelled not failed if builds are cancelled
+    if: ${{ !cancelled() }}
     steps:
-    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
+    - if: contains(needs.*.result, 'failure')
       uses: actions/github-script@v7
       with:
         script: |

.github/workflows/nix-ci.yml

@@ -77,7 +77,13 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build $NIX_BUILD_ARGS .#test -o push-test
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: push-test/test-results.xml
+        if: always()
+        continue-on-error: true
       - name: Build manual
         run: |
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc

.github/workflows/pr-release.yml

@@ -126,21 +126,19 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-
-            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              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
-
             STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.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."
               MESSAGE=""
+
+              if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
+                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."    
+              else
+                echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+                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."
@@ -151,7 +149,8 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            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_SHA\`."
+            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "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
 
           if [[ -n "$MESSAGE" ]]; then

CODEOWNERS

@@ -13,6 +13,7 @@
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @semorrison
 /src/Lean/Elab/Tactic/ @semorrison
+/src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
 /src/Lean/PrettyPrinter/ @Kha

RELEASES.md

@@ -11,21 +11,26 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
+* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
+
+  The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
+
+  In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
+
 * Lean now generates an error if the type of a theorem is **not** a proposition.
 
 * 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).
 
-* New command `derive_functinal_induction`:
+* Funcitonal induction principles.
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
+
+  For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
     | n+1, 0 => ackermann n 1
     | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  derive_functional_induction ackermann
   ```
   we get
   ```
@@ -35,6 +40,49 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
+* The termination checker now recognizes more recursion patterns without an
+  explicit `termination_by`. In particular the idiom of counting up to an upper
+  bound, as in
+  ```
+  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
+    if _ : i < arr.size then
+      Array.sum arr (i+1) (acc + arr[i])
+    else
+      acc
+  ```
+  is recognized without having to say `termination_by arr.size - i`.
+
+* 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`.
+
+* Now structure instances pretty print with parent structures' fields inlined.
+  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
+  Setting option `pp.structureInstances.flatten` to false turns this off.
+
+* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
+  to enable pretty printing function applications using generalized field notation (defaults to true).
+  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.
+  [#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).
+
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
@@ -62,6 +110,8 @@ 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`.
+
 v4.7.0
 ---------
 

default.nix

@@ -1,9 +0,0 @@
-# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
-{ nix = (import ./shell.nix {}).nix; } //
-(import (
-  fetchTarball {
-    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
-    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
-) {
-  src =  ./.;
-}).defaultNix

doc/flake.nix

@@ -27,7 +27,7 @@
         src = inputs.mdBook;
         cargoDeps = drv.cargoDeps.overrideAttrs (_: {
           inherit src;
-          outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
+          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
         });
         doCheck = false;
       });

doc/make/index.md

@@ -12,7 +12,7 @@ Platform-Specific Setup
 - [Windows (msys2)](msys2.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
-- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
+- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
 
 Generic Build Instructions
 --------------------------

flake.lock

@@ -1,12 +1,31 @@
 {
   "nodes": {
-    "flake-utils": {
+    "flake-compat": {
+      "flake": false,
       "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "lastModified": 1673956053,
+        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -18,11 +37,11 @@
     "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1676498134,
-        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
+        "lastModified": 1709737301,
+        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
         "owner": "leanprover",
         "repo": "lean4-mode",
-        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
+        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
         "type": "github"
       },
       "original": {
@@ -31,34 +50,35 @@
         "type": "github"
       }
     },
-    "lowdown-src": {
+    "libgit2": {
       "flake": false,
       "locked": {
-        "lastModified": 1633514407,
-        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "lastModified": 1697646580,
+        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
+        "owner": "libgit2",
+        "repo": "libgit2",
+        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
         "type": "github"
       },
       "original": {
-        "owner": "kristapsdz",
-        "repo": "lowdown",
+        "owner": "libgit2",
+        "repo": "libgit2",
         "type": "github"
       }
     },
     "nix": {
       "inputs": {
-        "lowdown-src": "lowdown-src",
+        "flake-compat": "flake-compat",
+        "libgit2": "libgit2",
         "nixpkgs": "nixpkgs",
         "nixpkgs-regression": "nixpkgs-regression"
       },
       "locked": {
-        "lastModified": 1657097207,
-        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "lastModified": 1711102798,
+        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
         "owner": "NixOS",
         "repo": "nix",
-        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "rev": "a22328066416650471c3545b0b138669ea212ab4",
         "type": "github"
       },
       "original": {
@@ -69,16 +89,33 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1653988320,
-        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
+        "lastModified": 1709083642,
+        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixos-22.05-small",
+        "ref": "release-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -101,11 +138,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
@@ -120,7 +157,23 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
       }
     }
   },

flake.nix

@@ -2,6 +2,9 @@
   description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  # old nixpkgs used for portable release with older glibc (2.27)
+  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
+  inputs.nixpkgs-old.flake = false;
   inputs.flake-utils.url = "github:numtide/flake-utils";
   inputs.nix.url = "github:NixOS/nix";
   inputs.lean4-mode = {
@@ -17,14 +20,41 @@
   #  inputs.lean4-mode.follows = "lean4-mode";
   #};
 
-  outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = import nixpkgs {
         inherit system;
         # for `vscode-with-extensions`
         config.allowUnfree = true;
       };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old = import nixpkgs-old { inherit system; };
+      # An old nixpkgs for creating releases with an old glibc
+      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
+
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
+
+      devShellWithDist = pkgsDist: pkgs.mkShell.override {
+	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+	} ({
+	  buildInputs = with pkgs; [
+	    cmake gmp ccache
+	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+	    # TODO: only add when proven to not affect the flakification
+	    #pkgs.python3
+	  ];
+	  # https://github.com/NixOS/nixpkgs/issues/60919
+	  hardeningDisable = [ "all" ];
+	  # more convenient `ctest` output
+	  CTEST_OUTPUT_ON_FAILURE = 1;
+	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+	  GMP = pkgsDist.gmp.override { withStatic = true; };
+	  GLIBC = pkgsDist.glibc;
+	  GLIBC_DEV = pkgsDist.glibc.dev;
+	  GCC_LIB = pkgsDist.gcc.cc.lib;
+	  ZLIB = pkgsDist.zlib;
+	  GDB = pkgsDist.gdb;
+	});
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
@@ -49,7 +79,10 @@
       };
       defaultPackage = lean-packages.lean-all;
 
-      inherit (lean-packages) devShell;
+      # The default development shell for working on lean itself
+      devShells.default = devShellWithDist pkgs;
+      devShells.oldGlibc = devShellWithDist pkgsDist-old;
+      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
 
       checks.lean = lean-packages.test;
     }) // rec {

nix/bootstrap.nix

@@ -65,7 +65,7 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.so $out/lib/lean
+      mv lib/lean/*.{so,dylib} $out/lib/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -170,10 +170,11 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
-          touch $out
+          mkdir $out
+          mv test-results.xml $out
         '';
       };
       update-stage0 =

nix/buildLeanPackage.nix

@@ -176,7 +176,7 @@ with builtins; let
       # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
       ln -s ${drv.c}/${drv.cPath} src.c
       # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
     '';
   };
   mkMod = mod: deps:

shell.nix

@@ -1,27 +0,0 @@
-let
-  flake = (import ./default.nix);
-  flakePkgs = flake.packages.${builtins.currentSystem};
-in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
-# use `shell` as default
-(attribs: attribs.shell // attribs) rec {
-  shell = pkgs.mkShell.override {
-    stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
-  } (rec {
-    buildInputs = with pkgs; [
-      cmake gmp ccache
-      flakePkgs.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-    ];
-    # https://github.com/NixOS/nixpkgs/issues/60919
-    hardeningDisable = [ "all" ];
-    # more convenient `ctest` output
-    CTEST_OUTPUT_ON_FAILURE = 1;
-  } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-    GMP = pkgsDist.gmp.override { withStatic = true; };
-    GLIBC = pkgsDist.glibc;
-    GLIBC_DEV = pkgsDist.glibc.dev;
-    GCC_LIB = pkgsDist.gcc.cc.lib;
-    ZLIB = pkgsDist.zlib;
-    GDB = pkgsDist.gdb;
-  });
-  nix = flake.devShell.${builtins.currentSystem};
-}

src/CMakeLists.txt

@@ -503,13 +503,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 # set up libInit_shared only on Windows; see also stdlib.make.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
   set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()

src/Init.lean

@@ -33,3 +33,4 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
+import Init.MacroTrace

src/Init/ByCases.lean

@@ -21,9 +21,9 @@ macro_rules
 
 /-! ## if-then-else -/
 
-@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
+@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
+@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
 
 theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
 

src/Init/Control/ExceptCps.lean

@@ -18,6 +18,7 @@ namespace ExceptCpsT
 def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
   x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
 
+set_option linter.unusedVariables false in  -- `s` unused
 @[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error

src/Init/Conv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.Meta
+import Init.Tactics
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -201,7 +201,7 @@ macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
   with inaccessible names to the given names.
 * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
-macro (name := case) tk:"case " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case) tk:"case " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case%$tk $args|* =>%$arr conv' => ($s); all_goals rfl)
 
 /--
@@ -210,7 +210,7 @@ has been solved after applying `tac`, nor admits the goal if `tac` failed.
 Recall that `case` closes the goal using `sorry` when `tac` fails, and
 the tactic execution is not interrupted.
 -/
-macro (name := case') tk:"case' " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
+macro (name := case') tk:"case' " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case'%$tk $args|* =>%$arr conv' => $s)
 
 /--

src/Init/Core.lean

@@ -19,7 +19,7 @@ which applies to all applications of the function).
 -/
 @[simp] def inline {α : Sort u} (a : α) : α := a
 
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -165,6 +165,7 @@ whose first component is `a : α` and whose second component is `b : β a`
 It is sometimes known as the dependent sum type, since it is the type level version
 of an indexed summation.
 -/
+@[pp_using_anonymous_constructor]
 structure Sigma {α : Type u} (β : α → Type v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
   (This will usually require a type ascription to determine `β`
@@ -190,6 +191,7 @@ which can cause problems for universe level unification,
 because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
 `PSigma` is usually only used in automation that constructs pairs of arbitrary types.
 -/
+@[pp_using_anonymous_constructor]
 structure PSigma {α : Sort u} (β : α → Sort v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
   (This will usually require a type ascription to determine `β`
@@ -1594,7 +1596,7 @@ protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
 The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
 then they have equal equivalence classes.
 -/
-def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
+theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
   Quot.sound
 
 /--

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.Fin.Basic
 import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
-import Init.Util
+import Init.GetElem
 universe u v w
 
 namespace Array
@@ -59,6 +59,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
@@ -456,24 +458,12 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec loop (i : Nat) (j : Nat) (inv : i + j = as.size) : Option Nat :=
-    if hlt : j < as.size then
-      match i, inv with
-      | 0, inv => by
-        apply False.elim
-        rw [Nat.zero_add] at inv
-        rw [inv] at hlt
-        exact absurd hlt (Nat.lt_irrefl _)
-      | i+1, inv =>
-        if p as[j] then
-          some j
-        else
-          have : i + (j+1) = as.size := by
-            rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-          loop i (j+1) this
-    else
-      none
-  loop as.size 0 rfl
+  let rec loop (j : Nat) :=
+    if h : j < as.size then
+      if p as[j] then some j else loop (j + 1)
+    else none
+    termination_by as.size - j
+  loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 a.findIdx? fun a => a == v
@@ -727,33 +717,36 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     termination_by as.size - i
   go 0 #[]
 
-def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
-  if h : i < a.size then
-    let idx  : Fin a.size := ⟨i, h⟩;
-    let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    let a' := a.swap idx idx1
-    eraseIdxAux (i+1) a'
+/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  if h : i.val + 1 < a.size then
+    let a' := a.swap ⟨i.val + 1, h⟩ i
+    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+    have : a'.size - i' < a.size - i := by
+      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
+    a'.feraseIdx i'
   else
     a.pop
-termination_by a.size - i
+termination_by a.size - i.val
 
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  eraseIdxAux (i.val + 1) a
+theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+  induction a, i using Array.feraseIdx.induct with
+  | @case1 a i h a' _ _ ih =>
+    unfold feraseIdx
+    simp [h, a', ih]
+  | case2 a i h =>
+    unfold feraseIdx
+    simp [h]
 
+/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
+
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
 def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if i < a.size then eraseIdxAux (i+1) a else a
-
-def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size) : { r : Array α // r.size = a.size - 1 } :=
-  if h : i < r.size then
-    let idx  : Fin r.size := ⟨i, h⟩;
-    let idx1 : Fin r.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
-    eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
-  else
-    ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
-termination_by r.size - i
-
-def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
-  eraseIdxSzAux a (i.val + 1) a rfl
+  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with

src/Init/Data/Array/Subarray.lean

@@ -32,6 +32,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
+
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Basic.lean

@@ -618,4 +618,14 @@ section normalization_eqs
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
 
+/-- Converts a list of `Bool`s to a big-endian `BitVec`. -/
+def ofBoolListBE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => cons b (ofBoolListBE bs)
+
+/-- Converts a list of `Bool`s to a little-endian `BitVec`. -/
+def ofBoolListLE : (bs : List Bool) → BitVec bs.length
+| [] => 0#0
+| b :: bs => concat (ofBoolListLE bs) b
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -41,12 +41,36 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
   have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
   omega
 
+@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb x i = false := by
+  rw [getMsb]
+  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
+  omega
+
 theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
+theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
+  rw [getMsb]
+
+theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
+  rw [getMsb]
+  by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
+    simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
+  · congr
+    omega
+  all_goals
+    apply getLsb_ge
+    omega
+
 -- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsg_eq`.
 @[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
@@ -96,6 +120,8 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
+@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -290,6 +316,19 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
 
+@[simp] theorem getMsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsb (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsb x (i - (m - n))) := by
+  simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
+  by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
+    by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
+  all_goals
+    simp only [h₁, h₂, h₃, h₄]
+    simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
+      Bool.false_and, Bool.and_self] <;>
+    (try apply getLsb_ge) <;>
+    (try apply (getLsb_ge _ _ _).symm) <;>
+    omega
+
 @[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
   simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@@ -480,6 +519,24 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp [h]
   omega
 
+/-! ### cast -/
+
+@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+  ext
+  simp_all [lt_of_getLsb]
+
 /-! ### shiftLeft -/
 
 @[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@@ -529,6 +586,11 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     <;> simp_all
     <;> (rw [getLsb_ge]; omega)
 
+@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
+  have : n ≤ i + n := by omega
+  simp_all [shiftLeftZeroExtend_eq]
+
 @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
@@ -553,11 +615,18 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
     getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
-  simp [append_def]
+  simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
+@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
+    getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
+  simp [append_def]
+  by_cases h : n ≤ i
+  · simp [h]
+  · simp [h]
+
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
@@ -586,6 +655,31 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
   simp [cons]
 
+@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
+  ext i
+  simp only [getLsb_not, getLsb_append, cond_eq_if]
+  split
+  · simp_all
+  · simp_all; omega
+
+@[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
+@[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
+    (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
+  ext i
+  simp only [getLsb_append, cond_eq_if]
+  split <;> simp [*]
+
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -630,6 +724,13 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
+@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
+  rw [← BitVec.msb, msb_cons]
+
+@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
+  simp [cons, cond_eq_if]
+  omega
+
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
   apply eq_of_getLsb_eq
@@ -650,6 +751,21 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
     · simp_all
     · omega
 
+@[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
+  simp [cons]
+
+@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
+@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
+    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
+  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+
 /-! ### concat -/
 
 @[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -825,7 +941,7 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
-/- ! ### intMax -/
+/-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
 def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
@@ -839,4 +955,20 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
     omega
   simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
 
+/-! ### ofBoolList -/
+
+@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
+
+@[simp] theorem getLsb_ofBoolListBE :
+    (ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getLsb_eq_getMsb]
+
+@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
+  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
+
+@[simp] theorem getMsb_ofBoolListLE :
+    (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getMsb_eq_getLsb]
+
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -195,18 +199,6 @@ instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 /-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 0).toUInt64 <<< 0x38 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
   (bs.get! 6).toUInt64 <<< 0x30 |||
@@ -216,3 +208,15 @@ def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   (bs.get! 2).toUInt64 <<< 0x10 |||
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

src/Init/Data/Channel.lean

@@ -41,7 +41,7 @@ Sends a message on an `Channel`.
 
 This function does not block.
 -/
-def Channel.send (v : α) (ch : Channel α) : BaseIO Unit :=
+def Channel.send (ch : Channel α) (v : α) : BaseIO Unit :=
   ch.atomically do
     let st ← get
     if st.closed then return

src/Init/Data/Fin/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
-import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise.Basic
-import Init.Coe
 
 open Nat
 
@@ -170,9 +168,3 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
 end Fin
-
-instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem xs i h := getElem xs i.1 h
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Data/FloatArray/Basic.lean

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
+
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/Int/DivModLemmas.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Data.Int.DivMod
 import Init.Data.Int.Order
 import Init.Data.Nat.Dvd
+import Init.RCases
 
 /-!
 # Lemmas about integer division needed to bootstrap `omega`.

src/Init/Data/Int/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Conv
-import Init.PropLemmas
+import Init.NotationExtra
 
 namespace Int
 

src/Init/Data/Int/Order.lean

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Lemmas
 import Init.ByCases
-import Init.RCases
 
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
@@ -999,7 +998,8 @@ theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by
   refine fun a b => subNatNat_elim a b.succ
     (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
     (fun i n (e : (n + i).succ = _) => ?_) rfl
-  · rintro i n rfl
+  · intro i n h
+    subst h
     rw [Nat.add_comm _ i, Nat.add_assoc]
     exact Nat.le_add_right i (b.succ + b).succ
   · apply succ_le_succ

src/Init/Data/List.lean

@@ -8,3 +8,4 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
+import Init.Data.List.Impl

src/Init/Data/List/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
@@ -54,15 +55,6 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
-instance : GetElem (List α) Nat α fun as i => i < as.length where
-  getElem as i h := as.get ⟨i, h⟩
-
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
-  rfl
-
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
-  rfl
-
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]
@@ -458,7 +450,7 @@ contains the longest initial segment for which `p` returns true
 and the second part is everything else.
 
 * `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
-* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
+* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
 -/
 @[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
   loop as []
@@ -520,11 +512,6 @@ def drop : Nat → List α → List α
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
-  match as, i with
-  | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
-
 /--
 `O(min n |xs|)`. Returns the first `n` elements of `xs`, or the whole list if `n` is too large.
 * `take 0 [a, b, c, d, e] = []`

src/Init/Data/List/Impl.lean

@@ -0,0 +1,261 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Lemmas
+
+/-!
+## Tail recursive implementations for `List` definitions.
+
+Many of the proofs require theorems about `Array`,
+so these are in a separate file to minimize imports.
+-/
+
+namespace List
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where
+  /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
+  unless `n ≥ l.length` in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::xs, 0, acc => acc.toListAppend (a::xs)
+  | x::xs, n+1, acc => go xs n (acc.push x)
+
+@[csimp] theorem set_eq_setTR : @set = @setTR := by
+  funext α l n a; simp [setTR]
+  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
+    setTR.go l a xs n acc = acc.data ++ xs.set n a
+  | [], _ => fun h => by simp [setTR.go, set, h]
+  | x::xs, 0 => by simp [setTR.go, set]
+  | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
+  exact (go #[] _ _ rfl).symm
+
+/-- Tail recursive version of `erase`. -/
+@[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where
+  /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Array α → List α
+  | [], _ => l
+  | x::xs, acc => bif x == a then acc.toListAppend xs else go xs (acc.push x)
+
+@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
+  funext α _ l a; simp [eraseTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc h
+  | nil => simp [List.erase, eraseTR.go, h]
+  | cons x xs IH =>
+    simp [List.erase, eraseTR.go]
+    cases x == a <;> simp
+    · rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `eraseIdx`. -/
+@[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where
+  /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
+  unless `a` is not present in which case it returns `l` -/
+  go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::as, 0, acc => acc.toListAppend as
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
+  funext α l n; simp [eraseIdxTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc h
+  | nil => simp [eraseIdx, eraseIdxTR.go, h]
+  | cons x xs IH =>
+    match n with
+    | 0 => simp [eraseIdx, eraseIdxTR.go]
+    | n+1 =>
+      simp [eraseIdx, eraseIdxTR.go]
+      rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `bind`. -/
+@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
+  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | x::xs, acc => go xs (acc ++ f x)
+
+@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
+  funext α β as f
+  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
+    | [], acc => by simp [bindTR.go, bind]
+    | x::xs, acc => by simp [bindTR.go, bind, go xs]
+  exact (go as #[]).symm
+
+/-- Tail recursive version of `join`. -/
+@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
+
+@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
+  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
+
+/-- Tail recursive version of `filterMap`. -/
+@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
+  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
+  @[specialize] go : List α → Array β → List β
+  | [], acc => acc.toList
+  | a::as, acc => match f a with
+    | none => go as acc
+    | some b => go as (acc.push b)
+
+@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
+  funext α β f l
+  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
+    | [], acc => by simp [filterMapTR.go, filterMap]
+    | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
+  exact (go l #[]).symm
+
+/-- Tail recursive version of `replace`. -/
+@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
+  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
+  unless `b` is not found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+
+@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
+  funext α _ l b c; simp [replaceTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [replace, replaceTR.go]
+  | cons x xs IH =>
+    simp [replace, replaceTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `take`. -/
+@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
+  unless `n ≥ xs.length` in which case it returns `l`. -/
+  @[specialize] go : List α → Nat → Array α → List α
+  | [], _, _ => l
+  | _::_, 0, acc => acc.toList
+  | a::as, n+1, acc => go as n (acc.push a)
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext α n l; simp [takeTR]
+  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs generalizing n with intro acc
+  | nil => cases n <;> simp [take, takeTR.go]
+  | cons x xs IH =>
+    cases n with simp [take, takeTR.go]
+    | succ n => intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `takeWhile`. -/
+@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
+  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
+  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
+  @[specialize] go : List α → Array α → List α
+  | [], _ => l
+  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
+
+@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
+  funext α p l; simp [takeWhileTR]
+  suffices ∀ xs acc, l = acc.data ++ xs →
+      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
+    (this l #[] (by simp)).symm
+  intro xs; induction xs with intro acc
+  | nil => simp [takeWhile, takeWhileTR.go]
+  | cons x xs IH =>
+    simp [takeWhile, takeWhileTR.go]; split <;> simp [*]
+    · intro h; rw [IH]; simp; simp; exact h
+
+/-- Tail recursive version of `foldr`. -/
+@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
+
+@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
+
+/-- Tail recursive version of `zipWith`. -/
+@[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where
+  /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/
+  go : List α → List β → Array γ → List γ
+  | a::as, b::bs, acc => go as bs (acc.push (f a b))
+  | _, _, acc => acc.toList
+
+@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
+  funext α β γ f as bs
+  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
+    | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
+    | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
+  exact (go as bs #[]).symm
+
+/-- Tail recursive version of `unzip`. -/
+def unzipTR (l : List (α × β)) : List α × List β :=
+  l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
+
+@[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
+  funext α β l; simp [unzipTR]; induction l <;> simp [*]
+
+/-- Tail recursive version of `enumFrom`. -/
+def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
+  let arr := l.toArray
+  (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
+
+@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
+  funext α n l; simp [enumFromTR, -Array.size_toArray]
+  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
+      simp [enumFrom, f]
+  rw [Array.foldr_eq_foldr_data]
+  simp [go]
+
+theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
+  | 0 => rfl
+  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
+    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
+
+/-- Tail recursive version of `dropLast`. -/
+@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
+
+@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
+  funext α l; simp [dropLastTR]
+
+/-- Tail recursive version of `intersperse`. -/
+def intersperseTR (sep : α) : List α → List α
+  | [] => []
+  | [x] => [x]
+  | x::y::xs => x :: sep :: y :: xs.foldr (fun a r => sep :: a :: r) []
+
+@[csimp] theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR := by
+  funext α sep l; simp [intersperseTR]
+  match l with
+  | [] | [_] => rfl
+  | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
+
+/-- Tail recursive version of `intercalate`. -/
+def intercalateTR (sep : List α) : List (List α) → List α
+  | [] => []
+  | [x] => x
+  | x::xs => go sep.toArray x xs #[]
+where
+  /-- Auxiliary for `intercalateTR`:
+  `intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)` -/
+  go (sep : Array α) : List α → List (List α) → Array α → List α
+  | x, [], acc => acc.toListAppend x
+  | x, y::xs, acc => go sep y xs (acc ++ x ++ sep)
+
+@[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by
+  funext α sep l; simp [intercalate, intercalateTR]
+  match l with
+  | [] => rfl
+  | [_] => simp
+  | x::y::xs =>
+    let rec go {acc x} : ∀ xs,
+      intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
+    | [] => by simp [intercalateTR.go]
+    | _::_ => by simp [intercalateTR.go, go]
+    simp [intersperse, go]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -266,6 +266,12 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
+@[simp] theorem getD_nil : getD [] n d = d := rfl
+
+@[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
+
+@[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -705,3 +711,5 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
   | _ :: l, i + 1, j + 1 => by
     have g : i ≠ j := h ∘ congrArg (· + 1)
     simp [get_set_ne l g]
+
+end List

src/Init/Data/Option/Basic.lean

@@ -37,6 +37,13 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none,   _ => none
   | some a, b => b a
 
+/-- Runs `f` on `o`'s value, if any, and returns its result, or else returns `none`.  -/
+@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
+  if let some a := o then
+    return (← f a)
+  else
+    return none
+
 @[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
   if let some a := o then
     return some (← f a)

src/Init/Data/Ord.lean

@@ -6,6 +6,7 @@ Authors: Dany Fabian, Sebastian Ullrich
 
 prelude
 import Init.Data.String
+import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
@@ -87,11 +88,24 @@ def isGE : Ordering → Bool
 
 end Ordering
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x = y` corresponds to `Ordering.eq`.
+-/
 @[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
 
+/--
+Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
+`x == y` corresponds to `Ordering.eq`.
+-/
+@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
+  if x < y then .lt
+  else if x == y then .eq
+  else .gt
+
 /--
 Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
 first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
@@ -105,6 +119,7 @@ class Ord (α : Type u) where
 
 export Ord (compare)
 
+set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compare `x` and `y` by comparing `f x` and `f y`.
 -/
@@ -147,6 +162,13 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
+instance [Ord α] : Ord (Option α) where
+  compare
+  | none,   none   => .eq
+  | none,   some _ => .lt
+  | some _, none   => .gt
+  | some x, some y => compare x y
+
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
@@ -194,7 +216,7 @@ protected def opposite (ord : Ord α) : Ord α where
 /--
 `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
 -/
-protected def on (ord : Ord β) (f : α → β) : Ord α where
+protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -210,4 +232,13 @@ returns 'equal', by `ord₂`.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
+/--
+Creates an order which compares elements of an `Array` in lexicographic order.
+-/
+protected def arrayOrd [a : Ord α] : Ord (Array α) where
+  compare x y :=
+    let _ : LT α := a.toLT
+    let _ : BEq α := a.toBEq
+    compareOfLessAndBEq x.toList y.toList
+
 end Ord

src/Init/Data/String/Extra.lean

@@ -62,4 +62,40 @@ namespace Iterator
 
 end Iterator
 
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 end String

src/Init/Ext.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
+import Init.Data.ToString.Macro
 import Init.TacticsExtra
 import Init.RCases
 

src/Init/GetElem.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Util
+
+@[never_extract]
+private def outOfBounds [Inhabited α] : α :=
+  panic! "index out of bounds"
+
+/--
+The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of return
+value `elem` and side conditions `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`.
+
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
+
+The proof side-condition `valid xs i` is automatically dispatched by the
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
+-/
+class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+              (valid : outParam (coll → idx → Prop)) where
+  /--
+  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
+  are proof side conditions to the application, they will be automatically
+  inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent, but here are some
+  important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
+    `default : α` if the index is not valid.
+  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
+    is not valid.
+  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
+    index is valid.
+  -/
+  getElem (xs : coll) (i : idx) (h : valid xs i) : elem
+
+  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
+
+@[inherit_doc getElem]
+syntax:max term noWs "[" withoutPosition(term) "]" : term
+macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
+
+@[inherit_doc getElem]
+syntax term noWs "[" withoutPosition(term) "]'" term:max : term
+macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
+
+/--
+The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
+returns `none` if `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+
+/--
+The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
+panics `i` is out of bounds.
+-/
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
+
+class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+
+  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+
+export LawfulGetElem (getElem?_def getElem!_def)
+
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
+  rw [getElem?_def]
+  exact dif_pos h
+
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
+  rw [getElem?_def]
+  exact dif_neg h
+
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
+    c[i]! = c[i]'h := by
+  simp only [getElem!_def, getElem?_def, h]
+
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
+  simp only [getElem!_def, getElem?_def, h]
+
+namespace Fin
+
+instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
+  getElem xs i h := getElem xs i.1 h
+  getElem? xs i := getElem? xs i.val
+  getElem! xs i := getElem! xs i.val
+
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
+
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+    a[i] = a[i.1] := rfl
+
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
+
+@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
+
+end Fin
+
+namespace List
+
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
+@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+  rfl
+
+@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+  rfl
+
+theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+  match as, i with
+  | _::_, 0   => rfl
+  | _::_, i+1 => get_drop_eq_drop _ i _
+
+end List
+
+namespace Array
+
+instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
+end Array
+
+namespace Lean.Syntax
+
+instance : GetElem Syntax Nat Syntax fun _ _ => True where
+  getElem stx i _ := stx.getArg i
+
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
+end Lean.Syntax

src/Init/MacroTrace.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Extra notation that depends on Init/Meta
+-/
+
+prelude
+import Init.Data.ToString.Macro
+import Init.Meta
+
+namespace Lean
+
+macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
+  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+
+end Lean

src/Init/Meta.lean

@@ -9,7 +9,6 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
-import Init.Data.String.Extra
 
 namespace Lean
 
@@ -105,43 +104,6 @@ def idBeginEscape := '«'
 def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
-
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 namespace Name
 
 def getRoot : Name → Name
@@ -947,6 +909,11 @@ def _root_.Substring.toName (s : Substring) : Name :=
       else
         Name.mkStr n comp
 
+/--
+Converts a `String` to a hierarchical `Name` after splitting it at the dots.
+
+`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
+-/
 def _root_.String.toName (s : String) : Name :=
   s.toSubstring.toName
 
@@ -1227,14 +1194,6 @@ instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
 
 end Lean.Syntax
 
-set_option linter.unusedVariables.funArgs false in
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the given tactic.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
-
 /-! # Helper functions for manipulating interpolated strings -/
 
 namespace Lean.Syntax

src/Init/NotationExtra.lean

@@ -6,14 +6,12 @@ Authors: Leonardo de Moura
 Extra notation that depends on Init/Meta
 -/
 prelude
-import Init.Meta
+import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
-import Init.Data.ToString
 import Init.Conv
-namespace Lean
+import Init.Meta
 
-macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
-  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+namespace Lean
 
 -- Auxiliary parsers and functions for declaring notation with binders
 
@@ -224,35 +222,35 @@ macro tk:"calc" steps:calcSteps : conv =>
   | _ => throw ()
 
 @[app_unexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"]
+  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++  a.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"]
+  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString)]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString ++ "." ++ a8.getString)]
   | _  => throw ()
 
 @[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

src/Init/Omega/Int.lean

@@ -50,6 +50,9 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
   simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
+theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
+  Int.ofNat_zero_le _
+
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
@@ -134,11 +137,13 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
+  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

src/Init/Omega/LinearCombo.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.Omega.Coeffs
+import Init.Data.ToString.Macro
 
 /-!
 # Linear combinations

src/Init/Prelude.lean

@@ -488,6 +488,7 @@ attribute [unbox] Prod
 Similar to `Prod`, but `α` and `β` can be propositions.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
+@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α
@@ -509,6 +510,7 @@ structure MProd (α β : Type u) where
 constructed and destructed like a pair: if `ha : a` and `hb : b` then
 `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
 -/
+@[pp_using_anonymous_constructor]
 structure And (a b : Prop) : Prop where
   /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
   intro ::
@@ -575,6 +577,7 @@ a pair-like type, so if you have `x : α` and `h : p x` then
 `⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
 you can also make it explicit using `s.1` or `s.val`.
 -/
+@[pp_using_anonymous_constructor]
 structure Subtype {α : Sort u} (p : α → Prop) where
   /-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
   type. You can also write this as `s.1`, or simply as `s` when the type is
@@ -1194,7 +1197,12 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a / b` computes the result of dividing `a` by `b`.
   The meaning of this notation is type-dependent.
   * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
-  * For `Nat` and `Int`, `a / b` rounds toward 0.
+  * For `Nat`, `a / b` rounds downwards.
+  * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
+    It is implemented as `Int.ediv`, the unique function satisfiying
+    `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
+    Other rounding conventions are available using the functions
+    `Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
   * For `Float`, `a / 0` follows the IEEE 754 semantics for division,
     usually resulting in `inf` or `nan`. -/
   hDiv : α → β → γ
@@ -1206,7 +1214,8 @@ This enables the notation `a % b : γ` where `a : α`, `b : β`.
 class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`.
   The meaning of this notation is type-dependent.
-  * For `Nat` and `Int`, `a % 0` is defined to be `a`. -/
+  * For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
+    and `a % 0` is defined to be `a`. -/
   hMod : α → β → γ
 
 /--
@@ -1809,6 +1818,7 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
 `Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
 It is the "canonical type with `n` elements".
 -/
+@[pp_using_anonymous_constructor]
 structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
   written as `i.1` or just `i` when the target type is known. -/
@@ -2533,43 +2543,6 @@ def panic {α : Type u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
-/--
-The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
-When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
-of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
-`dom` is whatever proof side conditions are required to make this applicable.
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
-
-The proof side-condition `dom xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
--/
-class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
-  /--
-  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
-  If there are proof side conditions to the application, they will be automatically
-  inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent,
-  but here are some important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
-    does array indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
-    with proof side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
-  * `arr[i]!`: panics if the side goal is false
-  * `arr[i]?`: returns `none` if the side goal is false
-  * `arr[i]'h`: uses `h` to prove the side goal
-  -/
-  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
-
-export GetElem (getElem)
-
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
@@ -2627,9 +2600,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
-instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
-
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.
@@ -2745,7 +2715,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
@@ -3482,20 +3452,31 @@ instance : Hashable String where
 namespace Lean
 
 /--
-Hierarchical names. We use hierarchical names to name declarations and
-for creating unique identifiers for free variables and metavariables.
+Hierarchical names consist of a sequence of components, each of
+which is either a string or numeric, that are written separated by dots (`.`).
 
-You can create hierarchical names using the following quotation notation.
+Hierarchical names are used to name declarations and for creating
+unique identifiers for free variables and metavariables.
+
+You can create hierarchical names using a backtick:
 ```
 `Lean.Meta.whnf
 ```
-It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`
-You can use double quotes to request Lean to statically check whether the name
+It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.
+
+You can use double backticks to request Lean to statically check whether the name
 corresponds to a Lean declaration in scope.
 ```
 ``Lean.Meta.whnf
 ```
 If the name is not in scope, Lean will report an error.
+
+There are two ways to convert a `String` to a `Name`:
+
+ 1. `Name.mkSimple` creates a name with a single string component.
+
+ 2. `String.toName` first splits the string into its dot-separated
+    components, and then creates a hierarchical name.
 -/
 inductive Name where
   /-- The "anonymous" name. -/
@@ -3546,7 +3527,9 @@ abbrev mkNum (p : Name) (v : Nat) : Name :=
   Name.num p v
 
 /--
-Short for `.str .anonymous s`.
+Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.
+
+This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
 -/
 abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
@@ -3884,9 +3867,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
   | Syntax.node _ _ args => args.getD i Syntax.missing
   | _                    => Syntax.missing
 
-instance : GetElem Syntax Nat Syntax fun _ _ => True where
-  getElem stx i _ := stx.getArg i
-
 /-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`. -/
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with
@@ -4581,6 +4561,12 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
 Resolves the given name to an overload list of global definitions.
 The `List String` in each alternative is the deduced list of projections
 (which are ambiguous with name components).
+
+Remark: it will not trigger actions associated with reserved names. Recall that Lean
+has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
+containing stating that `foo` is equal to its definition. The action associated with `foo.def`
+automatically proves the theorem. At the macro level, the name is resolved, but the action is not
+executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n

src/Init/PropLemmas.lean

@@ -21,7 +21,7 @@ set_option linter.missingDocs true -- keep it documented
   | rfl, rfl, _ => rfl
 
 @[simp] theorem eq_true_eq_id : Eq True = id := by
-  funext _; simp only [true_iff, id.def, eq_iff_iff]
+  funext _; simp only [true_iff, id_def, eq_iff_iff]
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
   cases propext (iff_of_true hp hq); rfl

src/Init/RCases.lean

@@ -5,7 +5,8 @@ Authors: Mario Carneiro, Jacob von Raumer
 -/
 prelude
 import Init.Tactics
-import Init.NotationExtra
+import Init.Meta
+
 
 /-!
 # Recursive cases (`rcases`) tactic and related tactics
@@ -127,7 +128,7 @@ the input expression). An `rcases` pattern has the following grammar:
   and so on.
 * A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
   while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
+* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
   or a nested disjunction like `a ∨ b ∨ c`.
 
 A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,

src/Init/Simproc.lean

@@ -11,22 +11,23 @@ namespace Lean.Parser
 A user-defined simplification procedure used by the `simp` tactic, and its variants.
 Here is an example.
 ```lean
-simproc reduce_add (_ + _) := fun e => do
-  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
-  let some n ← getNatValue? (e.getArg! 4) | return none
-  let some m ← getNatValue? (e.getArg! 5) | return none
-  return some (.done { expr := mkNatLit (n+m) })
+theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]
+
+open Lean Meta Simp
+simproc ↓ shortCircuitAnd (And _ _) := fun e => do
+  let_expr And p q := e | return .continue
+  let r ← simp p
+  let_expr False := r.expr | return .continue
+  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
+  return .done { expr := r.expr, proof? := some proof }
 ```
-The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The `simp` tactic invokes `shortCircuitAnd` whenever it finds a term of the form `And _ _`.
 The simplification procedures are stored in an (imperfect) discrimination tree.
 The procedure should **not** assume the term `e` perfectly matches the given pattern.
 The body of a simplification procedure must have type `Simproc`, which is an alias for
-`Expr → SimpM (Option Step)`.
+`Expr → SimpM Step`
 You can instruct the simplifier to apply the procedure before its sub-expressions
-have been simplified by using the modifier `↓` before the procedure name. Example.
-```lean
-simproc ↓ reduce_add (_ + _) := fun e => ...
-```
+have been simplified by using the modifier `↓` before the procedure name.
 Simplification procedures can be also scoped or local.
 -/
 syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command

src/Init/System/FilePath.lean

@@ -73,7 +73,21 @@ private def posOfLastSep (p : FilePath) : Option String.Pos :=
   p.toString.revFind pathSeparators.contains
 
 def parent (p : FilePath) : Option FilePath :=
-  FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
+  if p.isAbsolute then
+    let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
+    if p.toString.length == lengthOfRootDirectory then
+      -- `p` is a root directory
+      none
+    else if posOfLastSep p == String.Pos.mk (lengthOfRootDirectory - 1) then
+      -- `p` is a direct child of the root
+      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
+    else
+      -- `p` is an absolute path with at least two subdirectories
+      extractParentPath
+  else
+    -- `p` is a relative path
+    extractParentPath
 
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with

src/Init/Tactics.lean

@@ -224,7 +224,7 @@ the first matching constructor, or else fails.
 syntax (name := constructor) "constructor" : tactic
 
 /--
-Applies the second constructor when
+Applies the first constructor when
 the goal is an inductive type with exactly two constructors, or fails otherwise.
 ```
 example : True ∨ False := by
@@ -354,6 +354,9 @@ macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
     with_annotate_state $tk skip
     all_goals $y:tactic)
 
+/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
+syntax (name := fail) "fail" (ppSpace str)? : tactic
+
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations. -/
 syntax (name := eqRefl) "eq_refl" : tactic
 
@@ -365,10 +368,23 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| eq_refl)
+macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
+macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
+/--
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
+-/
+syntax (name := applyRfl) "apply_rfl" : tactic
+
+macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
+
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -899,9 +915,6 @@ example : ∀ x : Nat, x = x := by unhygienic
 -/
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
-/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail" (ppSpace str)? : tactic
-
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
 and if the file is re-elaborated and the input matches, the tactic is not re-run and
@@ -1310,6 +1323,22 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
+/--
+Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
+-/
+syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
+
+/--
+`rw?` tries to find a lemma which can rewrite the goal.
+
+`rw?` should not be left in proofs; it is a search tool, like `apply?`.
+
+Suggestions are printed as `rw [h]` or `rw [← h]`.
+
+You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
+-/
+syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic
+
 /--
 `show_term tac` runs `tac`, then prints the generated term in the form
 "exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
@@ -1493,16 +1522,16 @@ macro "get_elem_tactic" : tactic =>
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )
 
-@[inherit_doc getElem]
-syntax:max term noWs "[" withoutPosition(term) "]" : term
-macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
-
-@[inherit_doc getElem]
-syntax term noWs "[" withoutPosition(term) "]'" term:max : term
-macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
 /--
 Searches environment for definitions or theorems that can be substituted in
 for `exact?% to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
+
+set_option linter.unusedVariables.funArgs false in
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

src/Init/Util.lean

@@ -73,19 +73,6 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
-@[never_extract]
-private def outOfBounds [Inhabited α] : α :=
-  panic! "index out of bounds"
-
-@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
-  if h : _ then getElem xs i h else outOfBounds
-
-@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
-  if h : _ then some (getElem xs i h) else none
-
-macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
-macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
-
 /--
   Marks given value and its object graph closure as multi-threaded if currently
   marked single-threaded. This will make reference counter updates atomic and

src/Lean.lean

@@ -24,6 +24,7 @@ import Lean.Eval
 import Lean.Structure
 import Lean.PrettyPrinter
 import Lean.CoreM
+import Lean.ReservedNameAction
 import Lean.InternalExceptionId
 import Lean.Server
 import Lean.ScopedEnvExtension

src/Lean/AuxRecursor.lean

@@ -34,7 +34,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   || declName == ``Eq.ndrec
   || declName == ``Eq.ndrecOn
 
-def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
+def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
   | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -663,7 +663,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
     (name : String := "") : M llvmctx (LLVM.Value llvmctx) :=
   match getExternEntryFor extData `c with
   | some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
-  | some (ExternEntry.inline "llvm" _pat) => throw "Unimplemented codegen of inline LLVM"
+  | some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
   | some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
   | some (ExternEntry.foreign _ extFn)  => emitSimpleExternalCall builder extFn ps ys retty name
   | _ => throw s!"Failed to emit extern application '{f}'."

src/Lean/Compiler/ImplementedByAttr.lean

@@ -17,7 +17,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
   getParam := fun declName stx => do
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
-    let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
+    let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
     let fnDecl ← getConstInfo fnName
     unless decl.levelParams.length == fnDecl.levelParams.length do
       throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"

src/Lean/Compiler/InitAttr.lean

@@ -44,7 +44,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
-        let initFnName ← Elab.resolveGlobalConstNoOverloadWithInfo initFnName
+        let initFnName ← Elab.realizeGlobalConstNoOverloadWithInfo initFnName
         let initDecl ← getConstInfo initFnName
         match getIOTypeArg initDecl.type with
         | none => throwError "initialization function '{initFnName}' must have type of the form `IO <type>`"

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -346,7 +346,7 @@ We call this whenever we enter a new local function. It clears both the
 current join point and the list of candidates since we can't lift join
 points outside of functions as explained in `mergeJpContextIfNecessary`.
 -/
-def withNewFunScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
+def withNewFunScope (x : ExtendM α): ExtendM α := do
   withReader (fun ctx => { ctx with currentJp? := none, candidates := {} }) do
     withNewScope do
       x
@@ -412,7 +412,7 @@ where
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)
     | .fun decl k =>
-      let decl ← withNewFunScope decl do
+      let decl ← withNewFunScope do
         decl.updateValue (← go decl.value)
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)

src/Lean/CoreM.lean

@@ -219,7 +219,7 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
   unless max == 0 do
     let numHeartbeats ← IO.getNumHeartbeats
     if numHeartbeats - (← read).initHeartbeats > max then
-      throwMaxHeartbeat moduleName optionName max
+      throwMaxHeartbeat (.mkSimple moduleName) optionName max
 
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats

src/Lean/Data/HashMap.lean

@@ -212,6 +212,8 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
+instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/Json/Basic.lean

@@ -10,6 +10,8 @@ import Init.Data.Range
 import Init.Data.OfScientific
 import Init.Data.Hashable
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 
 -- mantissa * 10^-exponent

src/Lean/Data/JsonRpc.lean

@@ -183,6 +183,9 @@ structure ResponseError (α : Type u) where
 instance [ToJson α] : CoeOut (ResponseError α) Message :=
   ⟨fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)⟩
 
+instance : CoeOut (ResponseError Unit) Message :=
+  ⟨fun r => Message.responseError r.id r.code r.message none⟩
+
 instance : Coe String RequestID := ⟨RequestID.str⟩
 instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩
 

src/Lean/Data/Lsp/Basic.lean

@@ -52,7 +52,7 @@ instance : LE Range := leOfOrd
 structure Location where
   uri : DocumentUri
   range : Range
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 structure LocationLink where
   originSelectionRange? : Option Range

src/Lean/Data/Lsp/Diagnostics.lean

@@ -25,7 +25,7 @@ open Json
 
 inductive DiagnosticSeverity where
   | error | warning | information | hint
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
@@ -45,7 +45,7 @@ instance : ToJson DiagnosticSeverity := ⟨fun
 inductive DiagnosticCode where
   | int (i : Int)
   | string (s : String)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticCode := ⟨fun
   | num (i : Int) => return DiagnosticCode.int i
@@ -62,7 +62,7 @@ inductive DiagnosticTag where
   | unnecessary
   /-- Deprecated or obsolete code. Rendered with a strike-through. -/
   | deprecated
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
@@ -80,7 +80,7 @@ instance : ToJson DiagnosticTag := ⟨fun
 structure DiagnosticRelatedInformation where
   location : Location
   message : String
-  deriving Inhabited, BEq, ToJson, FromJson
+  deriving Inhabited, BEq, ToJson, FromJson, Ord
 
 /-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.
 
@@ -113,6 +113,29 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
+local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
+
+/-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
+private structure DiagnosticWith.UserVisible (α : Type) where
+  range               : Range
+  fullRange?          : Option Range
+  severity?           : Option DiagnosticSeverity
+  code?               : Option DiagnosticCode
+  source?             : Option String
+  message             : α
+  tags?               : Option (Array DiagnosticTag)
+  relatedInformation? : Option (Array DiagnosticRelatedInformation)
+  deriving Ord
+
+/-- Extracts user-visible properties from the given `DiagnosticWith`. -/
+private def DiagnosticWith.UserVisible.ofDiagnostic (d : DiagnosticWith α)
+    : DiagnosticWith.UserVisible α :=
+  { d with }
+
+/-- Compares `DiagnosticWith` instances modulo non-user-facing properties. -/
+def compareByUserVisible [Ord α] (a b : DiagnosticWith α) : Ordering :=
+  compare (DiagnosticWith.UserVisible.ofDiagnostic a) (DiagnosticWith.UserVisible.ofDiagnostic b)
+
 abbrev Diagnostic := DiagnosticWith String
 
 /-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics). -/

src/Lean/Data/Lsp/Internal.lean

@@ -24,44 +24,50 @@ Identifier of a reference.
 -/
 inductive RefIdent where
   /-- Named identifier. These are used in all references that are globally available. -/
-  | const : Name → RefIdent
+  | const (moduleName : Name) (identName : Name) : RefIdent
   /-- Unnamed identifier. These are used for all local references. -/
-  | fvar  : FVarId → RefIdent
+  | fvar (moduleName : Name) (id : FVarId) : RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
-/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
-def toString : RefIdent → String
-  | RefIdent.const n => s!"c:{n}"
-  | RefIdent.fvar id => s!"f:{id.name}"
+instance : ToJson FVarId where
+  toJson id := toJson id.name
 
-/--
-Converts the string representation of a reference identifier back to a reference identifier.
-The string representation must have been created by `RefIdent.toString`.
--/
-def fromString (s : String) : Except String RefIdent := do
-  let sPrefix := s.take 2
-  let sName := s.drop 2
-  -- See `FromJson Name`
-  let name ← match sName with
-    | "[anonymous]" => pure Name.anonymous
-    | _ =>
-      let n := sName.toName
-      if n.isAnonymous then throw s!"expected a Name, got {sName}"
-      else pure n
-  match sPrefix with
-    | "c:" => return RefIdent.const name
-    | "f:" => return RefIdent.fvar <| FVarId.mk name
-    | _ => throw "string must start with 'c:' or 'f:'"
+instance : FromJson FVarId where
+  fromJson? s := return ⟨← fromJson? s⟩
+
+/-- Shortened representation of `RefIdent` for more compact serialization. -/
+inductive RefIdentJsonRepr
+  /-- Shortened representation of `RefIdent.const` for more compact serialization. -/
+  | c (m n : Name)
+  /-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/
+  | f (m : Name) (i : FVarId)
+  deriving FromJson, ToJson
+
+/-- Converts `id` to its compact serialization representation. -/
+def toJsonRepr : (id : RefIdent) → RefIdentJsonRepr
+  | const moduleName identName => .c moduleName identName
+  | fvar moduleName id => .f moduleName id
+
+/-- Converts `repr` to `RefIdent`. -/
+def fromJsonRepr : (repr : RefIdentJsonRepr) → RefIdent
+  | .c m n => const m n
+  | .f m i => fvar m i
+
+/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/
+def fromJson? (s : Json) : Except String RefIdent :=
+  return fromJsonRepr (← Lean.FromJson.fromJson? s)
+
+/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/
+def toJson (id : RefIdent) : Json :=
+  Lean.ToJson.toJson <| toJsonRepr id
 
 instance : FromJson RefIdent where
-  fromJson?
-    | (s : String) => fromString s
-    | j => Except.error s!"expected a String, got {j}"
+  fromJson? := fromJson?
 
 instance : ToJson RefIdent where
-  toJson ident := toString ident
+  toJson := toJson
 
 end RefIdent
 
@@ -84,6 +90,7 @@ structure RefInfo.Location where
   range       : Lsp.Range
   /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
   parentDecl? : Option RefInfo.ParentDecl
+deriving Inhabited
 
 /-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
 structure RefInfo where
@@ -146,17 +153,18 @@ instance : FromJson RefInfo where
 def ModuleRefs := HashMap RefIdent RefInfo
 
 instance : ToJson ModuleRefs where
-  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
+  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
 
 instance : FromJson ModuleRefs where
   fromJson? j := do
     let node ← j.getObj?
     node.foldM (init := HashMap.empty) fun m k v =>
-      return m.insert (← RefIdent.fromString k) (← fromJson? v)
+      return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
-/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
-
-Contains the file's definitions and references. -/
+/--
+Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
+Contains the definitions and references of the file managed by a worker.
+-/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
@@ -164,4 +172,22 @@ structure LeanIleanInfoParams where
   references : ModuleRefs
   deriving FromJson, ToJson
 
+/--
+Used in the `$/lean/importClosure` watchdog <- worker notification.
+Contains the full import closure of the file managed by a worker.
+-/
+structure LeanImportClosureParams where
+  /-- Full import closure of the file. -/
+  importClosure : Array DocumentUri
+  deriving FromJson, ToJson
+
+/--
+Used in the `$/lean/importClosure` watchdog -> worker notification.
+Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
+-/
+structure LeanStaleDependencyParams where
+  /-- The dependency that is stale. -/
+  staleDependency : DocumentUri
+  deriving FromJson, ToJson
+
 end Lean.Lsp

src/Lean/Data/Lsp/Ipc.lean

@@ -64,9 +64,10 @@ def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request
   (←stdout).readLspRequestAs expectedMethod α
 
 /--
-  Reads response, discarding notifications in between. This function is meant
-  purely for testing where we use `collectDiagnostics` explicitly if we do care
-  about such notifications. -/
+Reads response, discarding notifications and server-to-client requests in between.
+This function is meant purely for testing where we use `collectDiagnostics` explicitly
+if we do care about such notifications.
+-/
 partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     IpcM (Response α) := do
   let m ← (←stdout).readLspMessage
@@ -79,20 +80,28 @@ partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     else
       throw $ userError s!"Expected id {expectedID}, got id {id}"
   | .notification .. => readResponseAs expectedID α
-  | _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
+  | .request .. => readResponseAs expectedID α
+  | .responseError .. => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
 
 def waitForExit : IpcM UInt32 := do
   (←read).wait
 
-/-- Waits for the worker to emit all diagnostics for the current document version
-and returns them as a list. -/
+/--
+Waits for the worker to emit all diagnostic notifications for the current document version and
+returns the last notification, if any.
+
+We used to return all notifications but with debouncing in the server, this would not be
+deterministic anymore as what messages are dropped depends on wall-clock timing.
+ -/
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
-: IpcM (List (Notification PublishDiagnosticsParams)) := do
+: IpcM (Option (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
+  loop
+where
+  loop := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then return []
+      if id == waitForDiagnosticsId then return none
       else loop
     | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
@@ -100,10 +109,9 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
       else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
+      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", diagnosticParam⟩
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
     | _ => loop
-  loop
 
 def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do
   let proc ← Process.spawn {

src/Lean/Data/Lsp/TextSync.lean

@@ -38,7 +38,7 @@ structure DidOpenTextDocumentParams where
 
 structure TextDocumentChangeRegistrationOptions where
   documentSelector? : Option DocumentSelector := none
-  syncKind : TextDocumentSyncKind
+  syncKind          : TextDocumentSyncKind
   deriving FromJson
 
 inductive TextDocumentContentChangeEvent where
@@ -61,13 +61,18 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
     | TextDocumentContentChangeEvent.fullChange text => [⟨"text", toJson text⟩]⟩
 
 structure DidChangeTextDocumentParams where
-  textDocument : VersionedTextDocumentIdentifier
+  textDocument   : VersionedTextDocumentIdentifier
   contentChanges : Array TextDocumentContentChangeEvent
   deriving ToJson, FromJson
 
+structure DidSaveTextDocumentParams where
+  textDocument : TextDocumentIdentifier
+  text?        : Option String
+  deriving ToJson, FromJson
+
 -- TODO: missing:
 -- WillSaveTextDocumentParams, TextDocumentSaveReason,
--- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
+-- TextDocumentSaveRegistrationOptions
 
 structure SaveOptions where
   includeText : Bool
@@ -81,11 +86,11 @@ structure DidCloseTextDocumentParams where
 
 /-- NOTE: This is defined twice in the spec. The latter version has more fields. -/
 structure TextDocumentSyncOptions where
-  openClose : Bool
-  change : TextDocumentSyncKind
-  willSave : Bool
+  openClose         : Bool
+  change            : TextDocumentSyncKind
+  willSave          : Bool
   willSaveWaitUntil : Bool
-  save? : Option SaveOptions := none
+  save?             : Option SaveOptions
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Lsp/Window.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marc Huisinga
+-/
+prelude
+import Lean.Data.Json
+
+open Lean
+
+inductive MessageType where
+  | error
+  | warning
+  | info
+  | log
+
+instance : FromJson MessageType where
+  fromJson?
+    | (1 : Nat) => .ok .error
+    | (2 : Nat) => .ok .warning
+    | (3 : Nat) => .ok .info
+    | (4 : Nat) => .ok .log
+    | _         => .error "Unknown MessageType ID"
+
+instance : ToJson MessageType where
+  toJson
+    | .error   => 1
+    | .warning => 2
+    | .info    => 3
+    | .log     => 4
+
+structure ShowMessageParams where
+  type    : MessageType
+  message : String
+  deriving FromJson, ToJson
+
+structure MessageActionItem where
+  title : String
+  deriving FromJson, ToJson
+
+structure ShowMessageRequestParams where
+  type     : MessageType
+  message  : String
+  actions? : Option (Array MessageActionItem)
+  deriving FromJson, ToJson
+
+def ShowMessageResponse := Option MessageActionItem
+  deriving FromJson, ToJson

src/Lean/Data/Name.lean

@@ -7,8 +7,6 @@ prelude
 import Init.Data.Ord
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 namespace Name
 -- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
 @[export lean_name_hash_exported] def hashEx : Name → UInt64 :=

src/Lean/Data/NameMap.lean

@@ -11,8 +11,6 @@ import Lean.Data.SSet
 import Lean.Data.Name
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 def NameMap (α : Type) := RBMap Name α Name.quickCmp
 
 @[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp

src/Lean/Data/Parsec.lean

@@ -5,7 +5,7 @@ Author: Dany Fabian
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 
 namespace Lean
 

src/Lean/Data/PersistentArray.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
+import Init.Data.ToString.Macro
 
 universe u v w
 
@@ -71,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.BasicAux
+import Init.Data.ToString.Macro
 
 namespace Lean
 universe u v w w'
@@ -154,6 +155,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
@@ -226,8 +229,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let ⟨keys', keq⟩ := keys.eraseIdx' idx
-      let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)

src/Lean/Data/Position.lean

@@ -38,9 +38,6 @@ structure FileMap where
   The first entry is always `0` and the last always the index of the last character.
   In particular, if the last character is a newline, that index will appear twice. -/
   positions : Array String.Pos
-  /-- The line numbers associated with the `positions`.
-  Has the same length as `positions` and is always of the form `#[1, 2, …, n-1, n-1]`. -/
-  lines     : Array Nat
   deriving Inhabited
 
 class MonadFileMap (m : Type → Type) where
@@ -50,40 +47,50 @@ export MonadFileMap (getFileMap)
 
 namespace FileMap
 
+/-- The last line should always be `positions.size - 1`. -/
+def getLastLine (fmap : FileMap) : Nat :=
+  fmap.positions.size - 1
+
+/-- The line numbers associated with the `positions` of the `FileMap`.
+`fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]`
+where `n` is the `size` of `positions`. -/
+def getLine (fmap : FileMap) (x : Nat) : Nat :=
+  min (x + 1) fmap.getLastLine
+
 partial def ofString (s : String) : FileMap :=
-  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap :=
-    if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }
+  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) : FileMap :=
+    if s.atEnd i then { source := s, positions := ps.push i }
     else
       let c := s.get i
       let i := s.next i
-      if c == '\n' then loop i (line+1) (ps.push i) (lines.push (line+1))
-      else loop i line ps lines
-  loop 0 1 (#[0]) (#[1])
+      if c == '\n' then loop i (line+1) (ps.push i)
+      else loop i line ps
+  loop 0 1 (#[0])
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
-  | { source := str, positions := ps, lines := lines } =>
+  | { source := str, positions := ps } =>
     if ps.size >= 2 && pos <= ps.back then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
       let rec loop (b e : Nat) :=
         let posB := ps[b]!
-        if e == b + 1 then { line := lines.get! b, column := toColumn posB 0 }
+        if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }
         else
           let m := (b + e) / 2;
           let posM := ps.get! m;
-          if pos == posM then { line := lines.get! m, column := 0 }
+          if pos == posM then { line := fmap.getLine m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
       loop 0 (ps.size -1)
-    else if lines.isEmpty then
+    else if ps.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨lines.back, (pos - ps.back).byteIdx⟩
+      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=

src/Lean/Data/Rat.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Basic
+import Init.Data.ToString.Macro
 import Init.Data.Int.DivMod
 import Init.Data.Nat.Gcd
 namespace Lean

src/Lean/Data/Xml/Basic.lean

@@ -5,6 +5,8 @@ Author: Dany Fabian
 -/
 prelude
 import Lean.Data.RBMap
+import Init.Data.ToString.Macro
+
 namespace Lean
 namespace Xml
 

src/Lean/DeclarationRange.lean

@@ -48,14 +48,14 @@ def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : Declaratio
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   return declRangeExt.find? (← getEnv) declName
 
-def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
+def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv
   let ranges ← if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
     findDeclarationRangesCore? declName.getPrefix
   else
     findDeclarationRangesCore? declName
   match ranges with
-  | none => return (← builtinDeclRanges.get (m := IO)).find? declName
+  | none => return (← builtinDeclRanges.get (m := BaseIO)).find? declName
   | some _ => return ranges
 
 end Lean

src/Lean/DocString.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.DeclarationRange
 import Lean.MonadEnv
+import Init.Data.String.Extra
 
 namespace Lean
 
@@ -13,10 +14,10 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
 
 def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
-  modifyEnv fun env => docStringExt.insert env declName (removeLeadingSpaces docString)
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
 def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with

src/Lean/Elab/App.lean

@@ -1035,7 +1035,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName _ _ =>
-      let fullName := `Function ++ fieldName
+      let fullName := Name.str `Function fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
@@ -1060,9 +1060,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
+      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
         return LValResolution.const baseStructName structName fullName
-      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
+      else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
         return LValResolution.const structName' structName' fullName
       else
         throwLValError e eType
@@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   if baseName == `Function then
     return (← whnfR type).isForall
-  else if type.consumeMData.isAppOf baseName then
+  else if type.cleanupAnnotations.isAppOf baseName then
     return true
   else
     return (← whnfR type).isAppOf baseName

src/Lean/Elab/BuiltinCommand.lean

@@ -55,7 +55,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
 
 private def checkAnonymousScope : List Scope → Option Name
   | { header := "", .. } :: _ => none
-  | { header := h, .. }  :: _ => some h
+  | { header := h, .. }  :: _ => some <| .mkSimple h
   | _                         => some .anonymous -- should not happen
 
 private def checkEndHeader : Name → List Scope → Option Name
@@ -64,7 +64,7 @@ private def checkEndHeader : Name → List Scope → Option Name
     if h == s then
       (.str · s) <$> checkEndHeader p scopes
     else
-      some h
+      some <| .mkSimple h
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
@@ -536,7 +536,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
     -- show signature for `#check id`/`#check @id`
     if let `($id:ident) := term then
       try
-        for c in (← resolveGlobalConstWithInfos term) do
+        for c in (← realizeGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -760,7 +760,7 @@ def elabRunMeta : CommandElab := fun stx =>
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
-    let declName ← resolveGlobalConstNoOverloadWithInfo id
+    let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
       throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then

src/Lean/Elab/BuiltinTerm.lean

@@ -223,7 +223,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
 
 @[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
-  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
+  return toExpr (← realizeGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?

src/Lean/Elab/Command.lean

@@ -141,7 +141,8 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap (.joinSep traceMsg.toList "\n") .information pos endPos
+    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
+    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 
 private def addTraceAsMessages : CommandElabM Unit := do
@@ -268,11 +269,6 @@ instance : MonadRecDepth CommandElabM where
   getRecDepth      := return (← read).currRecDepth
   getMaxRecDepth   := return (← get).maxRecDepth
 
-register_builtin_option showPartialSyntaxErrors : Bool := {
-  defValue := false
-  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
-}
-
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
@@ -321,11 +317,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages
     let mut msgs := (← get).messages
-    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
-    if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
-      -- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
-      msgs := ⟨msgs.msgs.filter fun msg =>
-        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder || tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
     modify fun st => { st with

src/Lean/Elab/DeclModifiers.lean

@@ -27,6 +27,8 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{declName}' has already been declared"
     | some declName => throwError "private declaration '{declName}' has already been declared"
+  if isReservedName env declName then
+    throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
     throwError "a private declaration '{declName}' has already been declared"

src/Lean/Elab/Declaration.lean

@@ -42,7 +42,7 @@ private def isNamedDef (stx : Syntax) : Bool :=
     let decl := stx[1]
     let k := decl.getKind
     k == ``Lean.Parser.Command.abbrev ||
-    k == ``Lean.Parser.Command.def ||
+    k == ``Lean.Parser.Command.definition ||
     k == ``Lean.Parser.Command.theorem ||
     k == ``Lean.Parser.Command.opaque ||
     k == ``Lean.Parser.Command.axiom ||
@@ -95,7 +95,7 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
   let scpView := extractMacroScopes name
   match scpView.name with
   | .str .anonymous _ => return none
-  | .str pre shortName => return some (pre, setDefName stx { scpView with name := shortName }.review)
+  | .str pre shortName => return some (pre, setDefName stx { scpView with name := .mkSimple shortName }.review)
   | _ => return none
 
 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
@@ -166,7 +166,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
+  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
   return {
     ref             := decl
     shortDeclName   := name
@@ -354,7 +354,7 @@ def elabMutual : CommandElab := fun stx => do
     -/
     let declNames ←
        try
-         resolveGlobalConst ident
+         realizeGlobalConst ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then

src/Lean/Elab/DefView.lean

@@ -142,7 +142,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
   declKind == ``Parser.Command.abbrev ||
-  declKind == ``Parser.Command.def ||
+  declKind == ``Parser.Command.definition ||
   declKind == ``Parser.Command.theorem ||
   declKind == ``Parser.Command.opaque ||
   declKind == ``Parser.Command.instance ||
@@ -152,7 +152,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
   let declKind := stx.getKind
   if declKind == ``Parser.Command.«abbrev» then
     return mkDefViewOfAbbrev modifiers stx
-  else if declKind == ``Parser.Command.def then
+  else if declKind == ``Parser.Command.definition then
     return mkDefViewOfDef modifiers stx
   else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx

src/Lean/Elab/Deriving/Basic.lean

@@ -100,10 +100,10 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
-     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
+     let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← resolveGlobalConstNoOverloadWithInfo cls
+         let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,12 +118,12 @@ structure DerivingClassView where
   className : Name
   args? : Option (TSyntax ``Parser.Term.structInst)
 
-def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
+def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
   match optDeriving with
   | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
     let mut ret := #[]
     for cls in classes, args? in argss? do
-      let className ← resolveGlobalConstNoOverloadWithInfo cls
+      let className ← realizeGlobalConstNoOverloadWithInfo cls
       ret := ret.push { ref := cls, className := className, args? }
     return ret
   | _ => return #[]

src/Lean/Elab/Deriving/Ord.lean

@@ -84,6 +84,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   for i in [:ctx.typeInfos.size] do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual
+     set_option match.ignoreUnusedAlts true
      $auxDefs:command*
     end)
 

src/Lean/Elab/Frontend.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Lean.Elab.Import
-import Lean.Elab.Command
+import Lean.Language.Lean
 import Lean.Util.Profile
 import Lean.Server.References
 
@@ -40,7 +39,19 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
 
 def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
   runCommandElabM do
+    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     Command.elabCommandTopLevel stx
+    let mut msgs := (← get).messages
+    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check
+    -- in general
+    if !Language.Lean.showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors &&
+        stx.hasMissing then
+      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
+      -- parse error
+      msgs := ⟨msgs.msgs.filter fun msg =>
+        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
+          tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
+    modify ({ · with messages := initMsgs ++ msgs })
 
 def updateCmdPos : FrontendM Unit := do
   modify fun s => { s with cmdPos := s.parserState.pos }
@@ -86,12 +97,8 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   pure (s.commandState.env, s.commandState.messages)
 
 builtin_initialize
-  registerOption `printMessageEndPos { defValue := false, descr := "print end position of each message in addition to start position" }
   registerTraceClass `Elab.info
 
-def getPrintMessageEndPos (opts : Options) : Bool :=
-  opts.getBool `printMessageEndPos false
-
 @[export lean_run_frontend]
 def runFrontend
     (input : String)
@@ -102,26 +109,50 @@ def runFrontend
     (ileanFileName? : Option String := none)
     : IO (Environment × Bool) := do
   let inputCtx := Parser.mkInputContext input fileName
-  let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  -- allow `env` to be leaked, which would live until the end of the process anyway
-  let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-  let env := env.setMainModule mainModuleName
-  let mut commandState := Command.mkState env messages opts
+  -- TODO: replace with `#lang` processing
+  if /- Lean #lang? -/ true then
+    -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
+    -- overhead of passing the environment between snapshots until we actually make good use of it
+    -- outside the server
+    let (header, parserState, messages) ← Parser.parseHeader inputCtx
+    -- allow `env` to be leaked, which would live until the end of the process anyway
+    let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
+    let env := env.setMainModule mainModuleName
+    let mut commandState := Command.mkState env messages opts
 
-  if ileanFileName?.isSome then
-    -- Collect InfoTrees so we can later extract and export their info to the ilean file
-    commandState := { commandState with infoState.enabled := true }
+    if ileanFileName?.isSome then
+      -- Collect InfoTrees so we can later extract and export their info to the ilean file
+      commandState := { commandState with infoState.enabled := true }
 
-  let s ← IO.processCommands inputCtx parserState commandState
-  for msg in s.commandState.messages.toList do
-    IO.print (← msg.toString (includeEndPos := getPrintMessageEndPos opts))
+    let s ← IO.processCommands inputCtx parserState commandState
+    for msg in s.commandState.messages.toList do
+      IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
 
+    if let some ileanFileName := ileanFileName? then
+      let trees := s.commandState.infoState.trees.toArray
+      let references ←
+        Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
+      let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
+      IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
+
+    return (s.commandState.env, !s.commandState.messages.hasErrors)
+
+  let ctx := { inputCtx with mainModuleName, opts, trustLevel }
+  let processor := Language.Lean.process
+  let snap ← processor none ctx
+  let snaps := Language.toSnapshotTree snap
+  snaps.runAndReport opts
   if let some ileanFileName := ileanFileName? then
-    let trees := s.commandState.infoState.trees.toArray
+    let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
     let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
     IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
 
-  pure (s.commandState.env, !s.commandState.messages.hasErrors)
+  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
+  -- TODO: remove default when reworking cmdline interface in Lean; currently the only case
+  -- where we use the environment despite errors in the file is `--stats`
+  let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
+  pure (env, !hasErrors)
+
 
 end Lean.Elab

src/Lean/Elab/GenInjective.lean

@@ -10,8 +10,8 @@ import Lean.Meta.Injective
 namespace Lean.Elab.Command
 
 @[builtin_command_elab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
+    let declName ← realizeGlobalConstNoOverloadWithInfo stx[1]
     Meta.mkInjectiveTheorems declName
 
 end Lean.Elab.Command

src/Lean/Elab/InfoTree/Main.lean

@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Meta.PPGoal
+import Lean.ReservedNameAction
 
 namespace Lean.Elab.CommandContextInfo
 
@@ -94,16 +95,18 @@ partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMa
     | none      => hole id
     | some tree => substitute tree assignment
 
-def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-  let x := x.run { lctx := lctx } { mctx := info.mctx }
+/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
+def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
   /-
     We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
     have been used in `lctx` and `info.mctx`.
   -/
-  let ((a, _), _) ←
+  (·.1) <$>
     x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
            { env := info.env, ngen := info.ngen }
-  return a
+
+def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
+  (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
 
 def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext :=
   { env  := info.env, mctx := info.mctx, lctx := lctx,
@@ -184,7 +187,7 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
 def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
-  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}"
+  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
 
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
@@ -279,31 +282,28 @@ def addConstInfo [MonadEnv m] [MonadError m]
     expectedType?
   }
 
-/-- This does the same job as `resolveGlobalConstNoOverload`; resolving an identifier
+/-- This does the same job as `realizeGlobalConstNoOverload`; resolving an identifier
 syntax to a unique fully resolved name or throwing if there are ambiguities.
 But also adds this resolved name to the infotree. This means that when you hover
 over a name in the sourcefile you will see the fully resolved name in the hover info.-/
-def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
-  let n ← resolveGlobalConstNoOverload id
+def realizeGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
+  let n ← realizeGlobalConstNoOverload id
   if (← getInfoState).enabled then
     -- we do not store a specific elaborator since identifiers are special-cased by the server anyway
     addConstInfo id n expectedType?
   return n
 
-/-- Similar to `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
-def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
-  let ns ← resolveGlobalConst id
+/-- Similar to `realizeGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
+def realizeGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
+  let ns ← realizeGlobalConst id
   if (← getInfoState).enabled then
     for n in ns do
       addConstInfo id n expectedType?
   return ns
 
-/-- Similar to `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
-def resolveGlobalNameWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (ref : Syntax) (id : Name) : m (List (Name × List String)) := do
-  let ns ← resolveGlobalName id
+/-- Similar to `realizeGlobalName`, but it also adds the resolved name to the info tree. -/
+def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
+  let ns ← realizeGlobalName id
   if (← getInfoState).enabled then
     for (n, _) in ns do
       addConstInfo ref n

src/Lean/Elab/InfoTree/Types.lean

@@ -157,12 +157,13 @@ structure FieldRedeclInfo where
 
 /--
 Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
-due to `pp.deepTerms false`. Omission needs to be treated differently from regular terms because
+due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
 it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
 Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
 regular delaboration settings.
 -/
-structure OmissionInfo extends TermInfo
+structure OmissionInfo extends TermInfo where
+  reason : String
 
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where

src/Lean/Elab/InheritDoc.lean

@@ -20,7 +20,7 @@ builtin_initialize
       | `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
-        let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
+        let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
         if (← findDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findDocString? (← getEnv) declName

src/Lean/Elab/MutualDef.lean

@@ -833,7 +833,7 @@ where
     for header in headers, view in views do
       if let some classNamesStx := view.deriving? then
         for classNameStx in classNamesStx do
-          let className ← resolveGlobalConstNoOverload classNameStx
+          let className ← realizeGlobalConstNoOverload classNameStx
           withRef classNameStx do
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -317,14 +317,6 @@ def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCo
 def tryContradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.contradictionCore { genDiseq := true }
 
-structure UnfoldEqnExtState where
-  map : PHashMap Name Name := {}
-  deriving Inhabited
-
-/- We generate the unfold equation on demand, and do not save them on .olean files. -/
-builtin_initialize unfoldEqnExt : EnvExtension UnfoldEqnExtState ←
-  registerEnvExtension (pure {})
-
 /--
   Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.
   `mvarId` is the goal to be proved. It is a goal of the form
@@ -370,9 +362,8 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
-  let env ← getEnv
   withOptions (tactic.hygienic.set · false) do
-    let baseName := mkPrivateName env declName
+    let baseName := declName
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -380,7 +371,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := baseName ++ `def
+      let name := Name.str baseName unfoldThmSuffix
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
@@ -388,13 +379,8 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       return name
 
 def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
-  let env ← getEnv
-  if let some eq := unfoldEqnExt.getState env |>.map.find? declName then
-    return some eq
-  else if let some info := getInfo? () then
-    let eq ← mkUnfoldEq declName info
-    modifyEnv fun env => unfoldEqnExt.modifyState env fun s => { s with map := s.map.insert declName eq }
-    return some eq
+  if let some info := getInfo? () then
+    return some (← mkUnfoldEq declName info)
   else
     return none
 

src/Lean/Elab/PreDefinition/Main.lean

@@ -105,6 +105,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       See issue #2321
       -/
       let preDef ← eraseRecAppSyntax preDefs[0]!
+      ensureEqnReservedNamesAvailable preDef.declName
       if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -63,12 +63,12 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes #[info.declName] goal.mvarId!
-  let baseName := mkPrivateName (← getEnv) info.declName
+  let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
@@ -81,6 +81,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
+  ensureEqnReservedNamesAvailable preDef.declName
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -101,6 +101,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
         -/
         registerEqnsInfo preDef recArgPos
     addSmartUnfoldingDef preDef recArgPos
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation
 
 builtin_initialize

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
+import Lean.Meta.ArgsPacker.Basic
 
 namespace Lean.Elab.WF
 open Meta
@@ -17,6 +18,7 @@ structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
   fixedPrefixSize : Nat
+  argsPacker      : ArgsPacker
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -107,7 +109,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
-  let baseName := mkPrivateName (← getEnv) declName
+  let baseName := declName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -117,7 +119,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
     let (type, value) ← removeUnusedEqnHypotheses type value
@@ -129,7 +131,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
+    (argsPacker : ArgsPacker) : MetaM Unit := do
+  preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
   Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
@@ -140,7 +144,8 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       let declNames := preDefs.map (·.declName)
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
-          eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
+          eqnInfoExt.insert env preDef.declName { preDef with
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -8,12 +8,12 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Cleanup
+import Lean.Meta.ArgsPacker
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
-import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Data.Array
 
 namespace Lean.Elab.WF
@@ -172,26 +172,28 @@ know which function is making the call.
 The close coupling with how arguments are packed and termination goals look like is not great,
 but it works for now.
 -/
-def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
+def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do
   let mut r := mkArray numFuncs #[]
   for goal in goals do
-    let (.mdata _ (.app _ param)) ← goal.getType
-        | throwError "MVar does not look like like a recursive call"
-    let (funidx, _) ← unpackMutualArg numFuncs param
+    let type ← goal.getType
+    let (.mdata _ (.app _ param)) := type
+        | throwError "MVar does not look like a recursive call:{indentExpr type}"
+    let (funidx, _) ← argsPacker.unpack param
     r := r.modify funidx (·.push goal)
   return r
 
-def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
+def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
   let goals ← assignSubsumed goals
-  let goalss ← groupGoalsByFunction decrTactics.size goals
+  let goalss ← groupGoalsByFunction argsPacker decrTactics.size goals
   for goals in goalss, decrTactic? in decrTactics do
     Lean.Elab.Term.TermElabM.run' do
     match decrTactic? with
     | none => do
       for goal in goals do
+        let type ← goal.getType
         let some ref := getRecAppSyntax? (← goal.getType)
-          | throwError "MVar does not look like like a recursive call"
+          | throwError "MVar not annotated as a recursive call:{indentExpr type}"
         withRef ref <| applyDefaultDecrTactic goal
     | some decrTactic => withRef decrTactic.ref do
       unless goals.isEmpty do -- unlikely to be empty
@@ -205,8 +207,8 @@ def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Ex
           Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
-def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
-    (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
+def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
+    (wfRel : Expr) (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
@@ -229,7 +231,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr)
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do
         processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
-      let val ← solveDecreasingGoals decrTactics val
+      let val ← solveDecreasingGoals argsPacker decrTactics val
       mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -9,19 +9,20 @@ import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.TryThis
+import Lean.Meta.ArgsPacker
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.WF.TerminationHint
-import Lean.Elab.PreDefinition.WF.PackMutual
+import Lean.Elab.PreDefinition.WF.TerminationArgument
 import Lean.Data.Array
 
 
 /-!
 This module finds lexicographic termination arguments for well-founded recursion.
 
-Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations
+Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
+(e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
 until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
 if given, or the default `decreasing_tactic`.
 
@@ -59,6 +60,10 @@ The following optimizations are applied to make this feasible:
 The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”
 by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5
 <https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf>.
+
+We got the idea of considering the measure `e₂ - e₁` if we see `e₁ < e₂` from
+“Termination Analysis with Calling Context Graphs” by Panagiotis Manolios &
+Daron Vroon, https://doi.org/10.1007/11817963_36.
 -/
 
 set_option autoImplicit false
@@ -84,11 +89,11 @@ def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
   lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
 /--
-Given the original paramter names from `originalVarNames`, remove the fixed prefix and find
+Given the original parameter names from `originalVarNames`, find
 good variable names to be used when talking about termination arguments:
 Use user-given parameter names if present; use x1...xn otherwise.
 
-The names ought to accessible (no macro scopes) and new names  fresh wrt to the current environment,
+The names ought to accessible (no macro scopes) and fresh wrt to the current environment,
 so that with `showInferredTerminationBy` we can print them to the user reliably.
 We do that by appending `'` as needed.
 
@@ -97,8 +102,7 @@ shadow each other, and the guessed relation refers to the wrong one. In that
 case, the user gets to keep both pieces (and may have to rename variables).
 -/
 partial
-def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do
-  let xs := xs.extract fixedPrefixSize xs.size
+def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
   let mut ns : Array Name := #[]
   for h : i in [:xs.size] do
     let n := xs[i]
@@ -115,6 +119,77 @@ def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name)
       else
         freshen ns (n.appendAfter "'")
 
+/-- A termination measure with extra fields for use within GuessLex -/
+structure Measure extends TerminationArgument where
+  /--
+  Like `.fn`, but unconditionally with `sizeOf` at the right type.
+  We use this one when in `evalRecCall`
+  -/
+  natFn : Expr
+deriving Inhabited
+
+/-- String desription of this measure -/
+def Measure.toString (measure : Measure) : MetaM String := do
+  lambdaTelescope measure.fn fun xs e => do
+    let e ← mkLambdaFVars xs[measure.arity:] e -- undo overshooting
+    return (← ppExpr e).pretty
+
+/--
+Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.
+
+For non-mutual definitions, we omit `sizeOf` when the argument does not depend on
+the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.
+
+For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of
+type `Nat` (else we'd have to worry about differently-typed measures from different functions to
+line up).
+-/
+def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool := do
+  let t ← inferType x
+  if is_mutual
+  then
+    withReducible (isDefEq t (.const `Nat []))
+  else
+    try
+      if t.hasAnyFVar (fun fvar => args.contains (.fvar fvar)) then
+        pure false
+      else
+        let u ← getLevel t
+        let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
+        let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
+        isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi)
+    catch _ =>
+      pure false
+
+/-- Sets the user names for the given freevars in `xs`. -/
+def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
+  let mut lctx ←  getLCtx
+  for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
+  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+
+/-- Create one measure for each (eligible) parameter of the given predefintion.  -/
+def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+    (userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := do
+  let is_mutual : Bool := preDefs.size > 1
+  preDefs.mapIdxM fun funIdx preDef => do
+    lambdaTelescope preDef.value fun xs _ => do
+      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
+        let mut ret : Array Measure := #[]
+        for x in xs[fixedPrefixSize:] do
+          -- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
+          -- `Type`), then ignore this parameter
+          let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
+          if sizeOf.isLit then continue
+
+          let natFn ← mkLambdaFVars xs (← mkAppM ``sizeOf #[x])
+          -- Determine if we need to exclude `sizeOf` in the measure we show/pass on.
+          let fn ←
+            if  ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
+            then mkLambdaFVars xs x
+            else pure natFn
+          let extraParams := preDef.termination.extraParams
+          ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams }
+        return ret
 
 /-- Internal monad used by `withRecApps` -/
 abbrev M (recFnName : Name) (α β : Type) : Type :=
@@ -225,11 +300,11 @@ structure RecCallWithContext where
   ref : Syntax
   /-- Function index of caller -/
   caller : Nat
-  /-- Parameters of caller -/
+  /-- Parameters of caller (including fixed prefix) -/
   params : Array Expr
   /-- Function index of callee -/
   callee : Nat
-  /-- Arguments to callee -/
+  /-- Arguments to callee (including fixed prefix) -/
   args : Array Expr
   ctxt : SavedLocalContext
 
@@ -261,25 +336,72 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
           return (false, true)
     return (true, true)
 
-/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
+/--
+Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
 call site.
 -/
-def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat)
-    : MetaM (Array RecCallWithContext) := withoutModifyingState do
+def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
+    (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do
   addAsAxiom unaryPreDef
   lambdaTelescope unaryPreDef.value fun xs body => do
     unless xs.size == fixedPrefixSize + 1 do
       -- Maybe cleaner to have lambdaBoundedTelescope?
       throwError "Unexpected number of lambdas in unary pre-definition"
+    let ys := xs[:fixedPrefixSize]
     let param := xs[fixedPrefixSize]!
     withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
       unless args.size ≥ fixedPrefixSize + 1 do
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let (caller, params) ← unpackArg arities param
-      let (callee, args) ← unpackArg arities arg
-      RecCallWithContext.create (← getRef) caller params callee args
+      let (caller, params) ← argsPacker.unpack param
+      let (callee, args) ← argsPacker.unpack arg
+      RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
+
+/-- Is the expression a `<`-like comparison of `Nat` expressions -/
+def isNatCmp (e : Expr) : Option (Expr × Expr) :=
+  match_expr e with
+  | LT.lt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
+  | LE.le α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₁, e₂) else none
+  | GT.gt α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
+  | GE.ge α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none
+  | _ => none
+
+def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+    (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :
+    MetaM (Array (Array Measure)) := do
+  preDefs.mapIdxM fun funIdx preDef => do
+    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+    let mut measures := #[]
+    for rc in recCalls do
+      -- Only look at calls from the current function
+      unless rc.caller = funIdx do continue
+      -- Only look at calls where the parameters have not been refined
+      unless rc.params.all (·.isFVar) do continue
+      let xs := rc.params.map (·.fvarId!)
+      let varyingParams : Array FVarId := xs[fixedPrefixSize:]
+      measures ← rc.ctxt.run do
+        withUserNames rc.params[fixedPrefixSize:] userVarNamess[funIdx]! do
+        trace[Elab.definition.wf] "rc: {rc.caller} ({rc.params}) → {rc.callee} ({rc.args})"
+        let mut measures := measures
+        for ldecl in ← getLCtx do
+          if let some (e₁, e₂) := isNatCmp ldecl.type then
+            -- We only want to consider these expressions if they depend only on the function's
+            -- immediate arguments, so check that
+            if e₁.hasAnyFVar (! xs.contains ·) then continue
+            if e₂.hasAnyFVar (! xs.contains ·) then continue
+            -- If e₁ does not depend on any varying parameters, simply ignore it
+            let e₁_is_const := ! e₁.hasAnyFVar (varyingParams.contains ·)
+            let body := if e₁_is_const then e₂ else mkNatSub e₂ e₁
+            -- Avoid adding simple measures
+            unless body.isFVar do
+              let fn ← mkLambdaFVars rc.params body
+              -- Avoid duplicates
+              unless ← measures.anyM (isDefEq ·.fn fn) do
+                let extraParams := preDef.termination.extraParams
+                measures := measures.push { ref := .missing, fn, natFn := fn, arity, extraParams }
+        return measures
+    return measures
 
 /-- A `GuessLexRel` described how a recursive call affects a measure; whether it
 decreases strictly, non-strictly, is equal, or else.  -/
@@ -302,31 +424,18 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr
   | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
   | no_idea => unreachable!
 
-/--
-Given an expression `e`, produce `sizeOf e` with a suitable instance.
-NB: We must use the instance of the type of the function parameter!
-The concrete argument at hand may have a different (still def-eq) typ.
--/
-def mkSizeOf (e : Expr) : MetaM Expr := do
-  let ty ← inferType e
-  let lvl ← getLevel ty
-  let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty])
-  let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty,  inst, e]
-  check res
-  return res
-
 /--
 For a given recursive call, and a choice of parameter and argument index,
 try to prove equality, < or ≤.
 -/
-def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext)
-  (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
+def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure)
+  (rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
   rcc.ctxt.run do
-    let param := rcc.params[paramIdx]!
-    let arg := rcc.args[argIdx]!
+    let callerMeasure := callerMeasures[callerMeasureIdx]!
+    let calleeMeasure := calleeMeasures[calleeMeasureIdx]!
+    let param := callerMeasure.natFn.beta rcc.params
+    let arg := calleeMeasure.natFn.beta rcc.args
     trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})"
-    let arg ← mkSizeOf rcc.args[argIdx]!
-    let param ← mkSizeOf rcc.params[paramIdx]!
     for rel in [GuessLexRel.eq, .lt, .le] do
       let goalExpr := mkAppN rel.toNatRel #[arg, param]
       trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}"
@@ -359,32 +468,35 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext)
 /- A cache for `evalRecCall` -/
 structure RecCallCache where mk'' ::
   decrTactic? : Option DecreasingBy
+  callerMeasures : Array Measure
+  calleeMeasures : Array Measure
   rcc : RecCallWithContext
   cache : IO.Ref (Array (Array (Option GuessLexRel)))
 
 /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
-def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
+def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure))
     (rcc : RecCallWithContext) :
     BaseIO RecCallCache := do
   let decrTactic? := decrTactics[rcc.caller]!
-  let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
-  return { decrTactic?, rcc, cache }
+  let callerMeasures := measuress[rcc.caller]!
+  let calleeMeasures := measuress[rcc.callee]!
+  let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
+  return { decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
 
 /-- Run `evalRecCall` and cache there result -/
-def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
+def RecCallCache.eval (rc: RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
   -- Check the cache first
-  if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then
+  if let Option.some res := (← rc.cache.get)[callerMeasureIdx]![calleeMeasureIdx]! then
     return res
   else
-    let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx
-    rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
+    let res ← evalRecCall rc.decrTactic? rc.callerMeasures rc.calleeMeasures rc.rcc callerMeasureIdx calleeMeasureIdx
+    rc.cache.modify (·.modify callerMeasureIdx (·.set! calleeMeasureIdx res))
     return res
 
-
 /-- Print a single cache entry as a string, without forcing it -/
-def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
+def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM String := do
   let cachedEntries ← rcc.cache.get
-  return match cachedEntries[paramIdx]![argIdx]! with
+  return match cachedEntries[callerMeasureIdx]![calleeMeasureIdx]! with
   | .some rel => toString rel
   | .none => "_"
 
@@ -398,10 +510,10 @@ inductive MutualMeasure where
 
 /-- Evaluate a recursive call at a given `MutualMeasure` -/
 def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
-  | .args argIdxs => do
-    let paramIdx := argIdxs[rc.rcc.caller]!
-    let argIdx := argIdxs[rc.rcc.callee]!
-    rc.eval paramIdx argIdx
+  | .args taIdxs => do
+    let callerMeasureIdx := taIdxs[rc.rcc.caller]!
+    let calleeMeasureIdx := taIdxs[rc.rcc.callee]!
+    rc.eval callerMeasureIdx calleeMeasureIdx
   | .func funIdx => do
     if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
       return .lt
@@ -410,97 +522,29 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
     else
       return .eq
 
-/--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
-where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
-This is the case for types such as `Prop`, `Type u`, etc.
-These arguments should not be considered when guessing a well-founded relation.
-See `generateCombinations?`
--/
-def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let mut result := #[]
-    for x in xs[fixedPrefixSize:], i in [:xs.size] do
-      try
-        let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
-        if sizeOf.isLit then
-         result := result.push i
-      catch _ =>
-        result := result.push i
-    return result
 
 /--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
-where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff the
-`WellFoundedRelation` of `aᵢ` goes via `SizeOf`, and `aᵢ` does not depend on `y₁`….
+Generate all combination of measures. Assumes we have numbered the measures of each function,
+and their counts is in `numMeasures`.
 
-These are the parameters for which we omit an explicit call to `sizeOf` in the termination argument.
-
-We only use this in the non-mutual case; in the mutual case we would have to additional check
-if the parameters that line up in the actual `TerminationWF` have the same type.
--/
-def getSizeOfParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let xs  : Array Expr := xs[fixedPrefixSize:]
-    let mut result := #[]
-    for x in xs, i in [:xs.size] do
-      try
-        let t ← inferType x
-        if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then continue
-        let u ← getLevel t
-        let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
-        let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
-        if ← isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) then
-          result := result.push i
-      catch _ =>
-        pure ()
-    return result
-
-/--
-Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
-where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `aᵢ` is `Nat`.
-These are parameters where we can definitely omit the call to `sizeOf`.
--/
-def getNatParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
-  lambdaTelescope preDef.value fun xs _ => do
-    let xs  : Array Expr := xs[fixedPrefixSize:]
-    let mut result := #[]
-    for x in xs, i in [:xs.size] do
-      let t ← inferType x
-      if ← withReducible (isDefEq t (.const `Nat [])) then
-        result := result.push i
-    return result
-
-/--
-Generate all combination of arguments, skipping those that are forbidden.
-
-Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
+This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
 try first, when the mutually recursive functions have similar argument structures
 -/
-partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat)
-    (threshold : Nat := 32) : Option (Array (Array Nat)) :=
+partial def generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) :
+    Option (Array (Array Nat)) :=
   (do goUniform 0; go 0 #[]) |>.run #[] |>.2
 where
-  isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
-    if h : fidx < forbiddenArgs.size then
-       forbiddenArgs[fidx] |>.contains argIdx
-    else
-      false
-
   -- Enumerate all permissible uniform combinations
-  goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
-    if numArgs.all (argIdx < ·) then
-      unless forbiddenArgs.any (·.contains argIdx) do
-        modify (·.push (Array.mkArray numArgs.size argIdx))
-      goUniform (argIdx + 1)
+  goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit  := do
+    if numMeasures.all (idx < ·) then
+      modify (·.push (Array.mkArray numMeasures.size idx))
+      goUniform (idx + 1)
 
   -- Enumerate all other permissible combinations
   go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
-    if h : fidx < numArgs.size then
-      let n := numArgs[fidx]
-      for argIdx in [:n] do
-        unless isForbidden fidx argIdx do
-          withReader (·.push argIdx) (go (fidx + 1))
+    if h : fidx < numMeasures.size then
+      let n := numMeasures[fidx]
+      for idx in [:n] do withReader (·.push idx) (go (fidx + 1))
     else
       let comb ← read
       unless comb.all (· == comb[0]!) do
@@ -508,19 +552,19 @@ where
       if (← get).size > threshold then
         failure
 
-
 /--
-Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and
+Enumerate all meausures we want to try.
+
+All arguments (resp. combinations thereof) and
 possible orderings of functions (if more than one)
 -/
-def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) :
-    MetaM (Array MutualMeasure) := do
-  let some arg_measures := generateCombinations? forbiddenArgs arities
+def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do
+  let some arg_measures := generateCombinations? numTermArgs
       | throwError "Too many combinations"
 
   let func_measures :=
-    if arities.size > 1 then
-      (List.range arities.size).toArray
+    if numTermArgs.size > 1 then
+      (List.range numTermArgs.size).toArray
     else
       #[]
 
@@ -565,61 +609,6 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
     -- None found, we have to give up
     return .none
 
-/--
-Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
--/
-def mkTupleSyntax : Array Term → MetaM Term
-  | #[]  => `(())
-  | #[e] => return e
-  | es   => `(($(es[0]!), $(es[1:]),*))
-
-/--
-Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
-combination of these measures. The parameters are
-
-* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
-  the fixed prefix.  Used to determine if we need to fully qualify `sizeOf`.
-* `varNamess`: For each function in the clique, the parameter names to be used in the
-  termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
-* `measures`: The measures to be used.
--/
-def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
-  (needsNoSizeOf : Array (Array Nat)) (measures : Array MutualMeasure) : MetaM TerminationWF := do
-  varNamess.mapIdxM fun funIdx varNames => do
-    let idents := varNames.map mkIdent
-    let measureStxs ← measures.mapM fun
-      | .args varIdxs => do
-          let varIdx := varIdxs[funIdx]!
-          let v := idents[varIdx]!
-          if needsNoSizeOf[funIdx]!.contains varIdx then
-            `($v)
-          else
-            -- Print `sizeOf` as such, unless it is shadowed.
-            -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
-            -- But it could also be shadowed by an earlier parameter (including the fixed prefix),
-            -- so look for unqualified (single tick) occurrences in `originalVarNames`
-            let sizeOfIdent :=
-              if originalVarNamess[funIdx]!.any (· = `sizeOf) then
-                mkIdent ``sizeOf -- fully qualified
-              else
-                mkIdent (← unresolveNameGlobal ``sizeOf)
-            `($sizeOfIdent $v)
-      | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
-    let body ← mkTupleSyntax measureStxs
-    return { ref := .missing, vars := idents, body, synthetic := true }
-
-/--
-The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
-syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
-syntax with more information, or valid syntax with (possibly) unresolved variable names?
-The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
-we do that.
--/
-def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
-  elems.mapIdx fun funIdx elem => { elem with
-    vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size]
-    synthetic := false }
-
 /--
 Given a matrix (row-major) of strings, arranges them in tabular form.
 First column is left-aligned, others right-aligned.
@@ -664,21 +653,43 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
   return s!"{position.line}:{position.column}{endPosStr}"
 
 
+/-- How to present the measure in the table header, possibly abbreviated. -/
+def measureHeader (measure : Measure) : StateT (Nat × String) MetaM String := do
+  let s ← measure.toString
+  if s.length > 5 then
+    let (i, footer) ← get
+    let i := i + 1
+    let footer := footer ++ s!"#{i}: {s}\n"
+    set (i, footer)
+    pure s!"#{i}"
+  else
+    pure s
+
+def collectHeaders {α} (a : StateT (Nat × String) MetaM α) : MetaM (α × String) := do
+  let (x, (_, footer)) ← a.run (0, "")
+  pure (x,footer)
+
+
 /-- Explain what we found out about the recursive calls (non-mutual case) -/
-def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
-  let header := varNames.map (·.eraseMacroScopes.toString)
+def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do
+  let (header, footer) ← collectHeaders (measures.mapM measureHeader)
   let mut table : Array (Array String) := #[#[""] ++ header]
   for i in [:rcs.size], rc in rcs do
     let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
-    for argIdx in [:varNames.size] do
+    for argIdx in [:measures.size] do
       row := row.push (← rc.prettyEntry argIdx argIdx)
     table := table.push row
-
-  return formatTable table
+  let out := formatTable table
+  if footer.isEmpty then
+    return out
+  else
+    return out ++ "\n\n" ++ footer
 
 /-- Explain what we found out about the recursive calls (mutual case) -/
-def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
+def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure))
     (rcs : Array RecCallCache) : MetaM Format := do
+  let (headerss, footer) ← collectHeaders (measuress.mapM (·.mapM measureHeader))
+
   let mut r := Format.nil
 
   for rc in rcs do
@@ -687,46 +698,71 @@ def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name
     r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
       f!"at {← rc.rcc.posString}:\n"
 
-    let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
-    let mut table : Array (Array String) := #[#[""] ++ header]
+    let mut table : Array (Array String) := #[#[""] ++ headerss[caller]!]
     if caller = callee then
       -- For self-calls, only the diagonal is interesting, so put it into one row
       let mut row := #[""]
-      for argIdx in [:varNamess[caller]!.size] do
+      for argIdx in [:measuress[caller]!.size] do
         row := row.push (← rc.prettyEntry argIdx argIdx)
       table := table.push row
     else
-      for argIdx in [:varNamess[callee]!.size] do
+      for argIdx in [:measuress[callee]!.size] do
         let mut row := #[]
-        row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
-        for paramIdx in [:varNamess[caller]!.size] do
+        row := row.push headerss[callee]![argIdx]!
+        for paramIdx in [:measuress[caller]!.size] do
           row := row.push (← rc.prettyEntry paramIdx argIdx)
         table := table.push row
     r := r ++ formatTable table ++ "\n"
 
+  unless footer.isEmpty do
+    r := r ++ "\n\n" ++ footer
+
   return r
 
-def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
+def explainFailure (declNames : Array Name) (measuress : Array (Array Measure))
     (rcs : Array RecCallCache) : MetaM Format := do
   let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
     "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
   if declNames.size = 1 then
-    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
+    r := r ++ (← explainNonMutualFailure measuress[0]! rcs)
   else
-    r := r ++ (← explainMutualFailure declNames varNamess rcs)
+    r := r ++ (← explainMutualFailure declNames measuress rcs)
   return r
 
 /--
-Shows the termination measure used to the user, and implements `termination_by?`
+For `#[x₁, .., xₙ]` create `(x₁, .., xₙ)`.
 -/
-def reportWF (preDefs : Array PreDefinition) (wf : TerminationWF) : MetaM Unit := do
-  let extraParamss := preDefs.map (·.termination.extraParams)
-  let wf' := trimTermWF extraParamss wf
-  for preDef in preDefs, term in wf' do
+def mkProdElem (xs : Array Expr) : MetaM Expr := do
+  match xs.size with
+  | 0 => return default
+  | 1 => return xs[0]!
+  | _ =>
+    let n := xs.size
+    xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
+
+def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
+    (userVarNamess : Array (Array Name)) (measuress : Array (Array Measure))
+    (solution : Array MutualMeasure) : MetaM TerminationArguments := do
+  preDefs.mapIdxM fun funIdx preDef => do
+    let measures := measuress[funIdx]!
+    lambdaTelescope preDef.value fun xs _ => do
+      withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
+        let args := solution.map fun
+          | .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
+          | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
+        let fn ← mkLambdaFVars xs (← mkProdElem args)
+        let extraParams := preDef.termination.extraParams
+        return { ref := .missing, arity := xs.size, extraParams, fn}
+
+/--
+Shows the inferred termination argument to the user, and implements `termination_by?`
+-/
+def reportTermArgs (preDefs : Array PreDefinition) (termArgs : TerminationArguments) : MetaM Unit := do
+  for preDef in preDefs, termArg in termArgs do
     if showInferredTerminationBy.get (← getOptions) then
-      logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
+      logInfoAt preDef.ref m!"Inferred termination argument:\n{← termArg.delab}"
     if let some ref := preDef.termination.terminationBy?? then
-      Tactic.TryThis.addSuggestion ref (← term.unexpand)
+      Tactic.TryThis.addSuggestion ref (← termArg.delab)
 
 end GuessLex
 open GuessLex
@@ -738,43 +774,41 @@ Try to find a lexicographic ordering of the arguments for which the recursive de
 terminates. See the module doc string for a high-level overview.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
-    (fixedPrefixSize : Nat) :
-    MetaM TerminationWF := do
-  let originalVarNamess ← preDefs.mapM originalVarNames
-  let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·)
-  let arities := varNamess.map (·.size)
-  trace[Elab.definition.wf] "varNames is: {varNamess}"
+    (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
+    MetaM TerminationArguments := do
+  let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
+  trace[Elab.definition.wf] "varNames is: {userVarNamess}"
 
-  let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize)
-  let needsNoSizeOf ←
-    if preDefs.size = 1 then
-      preDefs.mapM (getSizeOfParams fixedPrefixSize)
-    else
-      preDefs.mapM (getNatParams fixedPrefixSize)
+  -- Collect all recursive calls and extract their context
+  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker
+  let recCalls := filterSubsumed recCalls
+
+  -- For every function, the measures we want to use
+  -- (One for each non-forbiddend arg)
+  let meassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess
+  let meassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls
+  let measuress := Array.zipWith meassures₁ meassures₂ (· ++ ·)
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last
-  let measures ← generateMeasures forbiddenArgs arities
+  let measures ← generateMeasures (measuress.map (·.size))
 
   -- If there is only one plausible measure, use that
   if let #[solution] := measures then
-    let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf #[solution]
-    reportWF preDefs wf
-    return wf
+    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution]
+    reportTermArgs preDefs termArgs
+    return termArgs
 
-  -- Collect all recursive calls and extract their context
-  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
-  let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
-    let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf solution
-    reportWF preDefs wf
-    return wf
+    let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution
+    reportTermArgs preDefs termArgs
+    return termArgs
   | .none =>
-    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
+    let explanation ← explainFailure (preDefs.map (·.declName)) measuress rcs
     Lean.throwError <| "Could not find a decreasing measure.\n" ++
       explanation ++ "\n" ++
       "Please use `termination_by` to specify a decreasing measure."

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.WF.TerminationHint
-import Lean.Elab.PreDefinition.WF.PackDomain
+import Lean.Elab.PreDefinition.WF.TerminationArgument
 import Lean.Elab.PreDefinition.WF.PackMutual
 import Lean.Elab.PreDefinition.WF.Preprocess
 import Lean.Elab.PreDefinition.WF.Rel
@@ -19,29 +18,15 @@ namespace Lean.Elab
 open WF
 open Meta
 
-private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) (fixedPrefixSize : Nat) : TermElabM Unit := do
+private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition)  : TermElabM Unit := do
   let us := preDefNonRec.levelParams.map mkLevelParam
   let all := preDefs.toList.map (·.declName)
   for fidx in [:preDefs.size] do
     let preDef := preDefs[fidx]!
-    let value ← lambdaTelescope preDef.value fun xs _ => do
-      let packedArgs : Array Expr := xs[fixedPrefixSize:]
-      let mkProd (type : Expr) : MetaM Expr := do
-        mkUnaryArg type packedArgs
-      let rec mkSum (i : Nat) (type : Expr) : MetaM Expr := do
-        if i == preDefs.size - 1 then
-          mkProd type
-        else
-          (← whnfD type).withApp fun f args => do
-            assert! args.size == 2
-            if i == fidx then
-              return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! (← mkProd args[0]!)
-            else
-              let r ← mkSum (i+1) args[1]!
-              return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
-      let Expr.forallE _ domain _ _ := (← instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable!
-      let arg ← mkSum 0 domain
-      mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg)
+    let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
+      let value := mkAppN (mkConst preDefNonRec.declName us) xs
+      let value ← argsPacker.curryProj value fidx
+      mkLambdaFVars xs value
     trace[Elab.definition.wf] "{preDef.declName} := {value}"
     addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all)
 
@@ -81,25 +66,49 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
   else
     return false
 
+/--
+Collect the names of the varying variables (after the fixed prefix); this also determines the
+arity for the well-founded translations, and is turned into an `ArgsPacker`.
+We use the term to determine the arity, but take the name from the type, for better names in the
+```
+fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
+```
+idiom.
+-/
+def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do
+  -- We take the arity from the term, but the names from the types
+  let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size
+  assert! fixedPrefixSize ≤ arity
+  if arity = fixedPrefixSize then
+    throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments"
+  forallBoundedTelescope preDef.type arity fun xs _ => do
+    assert! xs.size = arity
+    let xs : Array Expr := xs[fixedPrefixSize:]
+    xs.mapM (·.fvarId!.getUserName)
+
 def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
-  let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
+  let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef
     let fixedPrefixSize ← getFixedPrefix preDefs
     trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}"
+    let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·)
+    let argsPacker := { varNamess }
     let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) }
-    let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
-    return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
+    return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte)
 
-  let wf ← do
+  let wf : TerminationArguments ← do
     let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
-      guessLex preDefs unaryPreDef fixedPrefixSize
+      guessLex preDefs unaryPreDef fixedPrefixSize argsPacker
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
+      preDefsWith.mapIdxM fun funIdx predef => do
+        let arity := fixedPrefixSize + argsPacker.varNamess[funIdx]!.size
+        let hints := predef.termination
+        TerminationArgument.elab predef.declName predef.type arity hints.extraParams hints.terminationBy?.get!
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -109,12 +118,14 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
 
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
     let type ← whnfForall type
+    unless type.isForall do
+      throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
+        let value ← mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.termination.decreasingBy?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
@@ -126,13 +137,14 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   else
     withEnableInfoTree false do
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize
+    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 builtin_initialize registerTraceClass `Elab.definition.wf