Merge commit '3e79ddda27' into releases/v4.2.0

.github/workflows/backport.yml

@@ -0,0 +1,26 @@
+name: Backport
+on:
+  pull_request_target:
+    types:
+      - closed
+      - labeled
+
+jobs:
+  backport:
+    name: Backport
+    runs-on: ubuntu-latest
+    # Only react to merged PRs for security reasons.
+    # See https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request_target.
+    if: >
+      github.event.pull_request.merged
+      && (
+        github.event.action == 'closed'
+        || (
+          github.event.action == 'labeled'
+          && contains(github.event.label.name, 'backport')
+        )
+      )
+    steps:
+      - uses: tibdex/backport@v2
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/ci.yml

@@ -168,6 +168,15 @@ jobs:
             shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "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: EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*
+          - name: Web Assembly
+            os: ubuntu-latest
+            # Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
+            CMAKE_OPTIONS: -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX="" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake
+            wasm: true
+            cross: true
+            shell: bash -euxo pipefail {0}
+            # Just a few selected test because wasm is slow
+            CTEST_OPTIONS: -R "leantest_1007\.lean|leantest_Format\.lean|leanruntest\_1037.lean|leanruntest_ac_rfl\.lean"
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
@@ -192,7 +201,7 @@ jobs:
         uses: cachix/install-nix-action@v18
         with:
           install_url: https://releases.nixos.org/nix/nix-2.12.0/install
-        if: matrix.os == 'ubuntu-latest'
+        if: matrix.os == 'ubuntu-latest' && !matrix.wasm
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
@@ -204,6 +213,17 @@ jobs:
         run: |
           brew install ccache tree zstd coreutils gmp
         if: matrix.os == 'macos-latest'
+      - name: Setup emsdk
+        uses: mymindstorm/setup-emsdk@v11
+        with:
+          version: 3.1.44
+          actions-cache-folder: emsdk
+        if: matrix.wasm
+      - name: Install 32bit c libs
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y gcc-multilib g++-multilib ccache
+        if: matrix.wasm
       - name: Cache
         uses: actions/cache@v3
         with:
@@ -280,7 +300,7 @@ jobs:
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
           ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
-        if: ${{ !matrix.cross }}
+        if: matrix.wasm || !matrix.cross
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross }}

.github/workflows/pr-release.yml

@@ -81,6 +81,7 @@ jobs:
       # Mathlib CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously.
       - name: Cleanup workspace
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
           sudo rm -rf *
 
@@ -94,6 +95,7 @@ jobs:
           fetch-depth: 0
 
       - name: Check if branch exists
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: check_branch
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
@@ -119,5 +121,6 @@ jobs:
           fi
 
       - name: Push changes
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}

CMakeLists.txt

@@ -26,23 +26,10 @@ endforeach()
 include(ExternalProject)
 project(LEAN CXX C)
 
-if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  # For Emscripten, we build GMP before any of the stages and reuse it in all of them.
-  set(GMP_INSTALL_PREFIX ${CMAKE_BINARY_DIR}/gmp-root)
-  set(EMSCRIPTEN_FLAGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1 -O3")
-  ExternalProject_Add(
-    gmp
-    URL https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2
-    URL_HASH SHA256=eae9326beb4158c386e39a356818031bd28f3124cf915f8c5b1dc4c7a36b4d7c
-    BUILD_IN_SOURCE 1
-    CONFIGURE_COMMAND emconfigure ./configure "CFLAGS=${EMSCRIPTEN_FLAGS}" --host=wasm32-unknown-emscripten --disable-assembly --prefix=${GMP_INSTALL_PREFIX}
-    BUILD_COMMAND emmake make -j4
-    INSTALL_COMMAND emmake make install
-  )
-  set(EXTRA_DEPENDS "gmp")
-  list(APPEND CL_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
-  list(APPEND PLATFORM_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
+if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
+    set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
+
 ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src
@@ -57,7 +44,7 @@ ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage0
@@ -66,7 +53,7 @@ ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
@@ -76,7 +63,7 @@ ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2

RELEASES.md

@@ -11,6 +11,23 @@ v4.2.0
 ---------
 
 No breaking changes at present.
+v4.3.0 (development in progress)
+---------
+
+* [isDefEq cache for terms not containing metavariables.](https://github.com/leanprover/lean4/pull/2644).
+* [Cancel outstanding tasks on document edit in the language server](https://github.com/leanprover/lean4/pull/2648).
+* Make [`Environment.mk`](https://github.com/leanprover/lean4/pull/2604) and [`Environment.add`](https://github.com/leanprover/lean4/pull/2642) private, and add [`replay`](https://github.com/leanprover/lean4/pull/2617) as a safer alternative.
+* `IO.Process.output` no longer inherits the standard input of the caller.
+* [Do not inhibit caching](https://github.com/leanprover/lean4/pull/2612) of default-level `match` reduction.
+* [List the valid case tags](https://github.com/leanprover/lean4/pull/2629) when the user writes an invalid one.
+* The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types.
+* [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616).
+* [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).
+* **Lake:** Add `postUpdate?` package configuration option. Used by a package to specify some code which should be run after a successful `lake update` of the package or one of its downstream dependencies. ([lake#185](https://github.com/leanprover/lake/issues/185))
+
+v4.2.0
+---------
+
 * Improvements to Lake startup time ([#2572](https://github.com/leanprover/lean4/pull/2572), [#2573](https://github.com/leanprover/lean4/pull/2573))
 * `refine e` now replaces the main goal with metavariables which were created during elaboration of `e` and no longer captures pre-existing metavariables that occur in `e` ([#2502](https://github.com/leanprover/lean4/pull/2502)).
   * This is accomplished via changes to `withCollectingNewGoalsFrom`, which also affects `elabTermWithHoles`, `refine'`, `calc` (tactic), and `specialize`. Likewise, all of these now only include newly-created metavariables in their output.
@@ -48,7 +65,7 @@ v4.0.0
 
 * [`dsimp` / `simp` / `simp_all` now fail by default if they make no progress](https://github.com/leanprover/lean4/pull/2336).
 
-  This can be overriden with the `(config := { failIfUnchanged := false })` option.
+  This can be overridden with the `(config := { failIfUnchanged := false })` option.
   This change was made to ease manual use of `simp` (with complicated goals it can be hard to tell if it was effective)
   and to allow easier flow control in tactics internally using `simp`.
   See the [summary discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20fails.20if.20no.20progress/near/380153295)
@@ -147,7 +164,7 @@ v4.0.0
 
 * New [code generator](https://github.com/leanprover/lean4/tree/master/src/Lean/Compiler/LCNF) project has started.
 
-* Remove description argument frome `register_simp_attr`. [PR #1566](https://github.com/leanprover/lean4/pull/1566).
+* Remove description argument from `register_simp_attr`. [PR #1566](https://github.com/leanprover/lean4/pull/1566).
 
 * [Additional concurrency primitives](https://github.com/leanprover/lean4/pull/1555).
 
@@ -667,7 +684,7 @@ v4.0.0-m5 (07 August 2022)
   `Foo : {Foo : Type u} → List Foo → Type`.
 
 
-* Fix syntax hightlighting for recursive declarations. Example
+* Fix syntax highlighting for recursive declarations. Example
   ```lean
   inductive List (α : Type u) where
     | nil : List α  -- `List` is not highlighted as a variable anymore
@@ -976,7 +993,7 @@ For example, given `f : Nat → Nat` and `g : Nat → Nat`, `f.comp g` is now no
 
 * Various improvements to go-to-definition & find-all-references accuracy.
 
-* Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)).
+* Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [wishlist](https://github.com/leanprover/lean4/issues/988)).
 
 * Rename option `autoBoundImplicitLocal` => `autoImplicit`.
 

doc/dev/bootstrap.md

@@ -69,6 +69,13 @@ Finally, when we want to use new language features in the library, we need to
 update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
 `make update-stage0` without `-C` defaults to stage1.
 
+Updates to `stage0` should be their own commits in the Git history. In
+other words, before running `make update-stage0`, please commit your
+work. Then, commit the updated `stage0` compiler code with the commit message:
+```
+chore: update stage0
+```
+
 ## Further Bootstrapping Complications
 
 As written above, changes in meta code in the current stage usually will only

doc/dev/index.md

@@ -64,3 +64,10 @@ simply by pushing a tag to your fork of the Lean 4 github repository
 If you push `my-tag` to a fork in your github account `my_name`,
 you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
 (You must use a tag name that does not start with a numeral, or contain `_`).
+
+### `ccache`
+
+Lean's build process uses [`ccache`](https://ccache.dev/) if it is
+installed to speed up recompilation of the generated C code. Without
+`ccache`, you'll likely spend more time than necessary waiting on
+rebuilds - it's a good idea to make sure it's installed.

doc/dev/testing.md

@@ -111,7 +111,7 @@ First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by
 sudo apt-get install meld
 ```
 
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `test/lean` directory and
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `tests/lean` directory and
 executing
 
 ```

doc/examples/bintree.lean

@@ -5,7 +5,7 @@ If the type of keys can be totally ordered -- that is, it supports a well-behave
 then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
 proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
 
-This example is based on a similar example found in the ["Sofware Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
+This example is based on a similar example found in the ["Software Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
 book (volume 3).
 -/
 
@@ -81,9 +81,9 @@ def Tree.toList (t : Tree β) : List (Nat × β) :=
       |>.toList
 
 /-!
-The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator.
+The implementation of `Tree.toList` is inefficient because of how it uses the `++` operator.
 On a balanced tree its running time is linearithmic, because it does a linear number of
-concatentations at each level of the tree. On an unbalanced tree it's quadratic time.
+concatenations at each level of the tree. On an unbalanced tree it's quadratic time.
 Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
 -/
 def Tree.toListTR (t : Tree β) : List (Nat × β) :=
@@ -114,9 +114,9 @@ concatenating all goals produced by `tac'`. In this theorem, we use it to apply
 
 The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce
 and/or apply auto generated equation theorems for these two functions.
-The parameter `*` intructs the simplifier to use any equation in a goal as rewriting rules.
+The parameter `*` instructs the simplifier to use any equation in a goal as rewriting rules.
 In this particular case, `simp` uses the induction hypotheses as rewriting rules.
-Finally, the parameter `List.append_assoc` intructs the simplifier to use the
+Finally, the parameter `List.append_assoc` instructs the simplifier to use the
 `List.append_assoc` theorem as a rewriting rule.
 -/
 theorem Tree.toList_eq_toListTR (t : Tree β)
@@ -186,7 +186,7 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
 The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
 hypotheses in the current goal as rewriting rules.
 Recall that the `by_cases` tactic creates two goals. One where we have `h : e` and
-another one containing `h : ¬ e`. The simplier uses the `h` to rewrite `e` to `True`
+another one containing `h : ¬ e`. The simplifier uses the `h` to rewrite `e` to `True`
 in the first subgoal, and `e` to `False` in the second. This is particularly
 useful if `e` is the condition of an `if`-statement.
 -/

doc/examples/deBruijn.lean

@@ -152,7 +152,7 @@ We prove all cases but the one for `plus` using `simp [*]`. This tactic instruct
 use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
-The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in
+The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in
 the "reverse direction". That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
 -/
 theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := by

doc/examples/interp.lean

@@ -83,7 +83,7 @@ In practice, this means we use `stop` to refer to the most recently defined vari
 
 A value `Expr.val` carries a concrete representation of an integer.
 
-A lambda `Expr.lam` creates a function. In the scope of a function ot type `Ty.fn a ty`, there is a
+A lambda `Expr.lam` creates a function. In the scope of a function of type `Ty.fn a ty`, there is a
 new local variable of type `a`.
 
 A function application `Expr.app` produces a value of type `ty` given a function from `a` to `ty` and a value of type `a`.
@@ -139,7 +139,7 @@ def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
 More interestingly, a factorial function fact (e.g. `fun x => if (x == 0) then 1 else (fact (x-1) * x)`), can be written as.
 Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the
 definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor
-`Expr.delay` to delay its unfolding. Second, we add the annotation `decreasing_by sorry` which can be viwed as
+`Expr.delay` to delay its unfolding. Second, we add the annotation `decreasing_by sorry` which can be viewed as
 "trust me, this recursive definition makes sense". Recall that `sorry` is an unsound axiom in Lean.
 -/
 

doc/examples/phoas.lean

@@ -228,7 +228,7 @@ We prove all cases but the one for `plus` using `simp [*]`. This tactic instruct
 use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
-The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in
+The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in
 the "reverse direction. That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
 -/
 theorem constFold_sound (e : Term' Ty.denote ty) : denote (constFold e) = denote e := by

doc/examples/tc.lean

@@ -38,7 +38,7 @@ theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t
   cases h₁ <;> cases h₂ <;> rfl
 
 /-!
-The inductive type `Maybe p` has two contructors: `found a h` and `unknown`.
+The inductive type `Maybe p` has two constructors: `found a h` and `unknown`.
 The former contains an element `a : α` and a proof that `a` satisfies the predicate `p`.
 The constructor `unknown` is used to encode "failure".
 -/

doc/faq.md

@@ -47,7 +47,7 @@ We expect similar independent checkers will be built for Lean 4.
 
 We use [GitHub](https://github.com/leanprover/lean4/issues) to track bugs and new features.
 Bug reports are always welcome, but nitpicking issues are not (e.g., the error message is confusing).
-See also our [contribution guidelines](../CONTRIBUTING.md).
+See also our [contribution guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
 
 ### Is it Lean, LEAN, or L∃∀N?
 

doc/latex/lstlean.tex

@@ -4,7 +4,7 @@
 
 \lstdefinelanguage{lean} {
 
-% Anything betweeen $ becomes LaTeX math mode
+% Anything between $ becomes LaTeX math mode
 mathescape=false,
 % Comments may or not include Latex commands
 texcl=false,
@@ -265,7 +265,7 @@
 % Style for (listings') identifiers
 identifierstyle={\ttfamily\color{black}},
 % Note : highlighting of Coq identifiers is done through a new
-% delimiter definition through an lstset at the begining of the
+% delimiter definition through an lstset at the beginning of the
 % document. Don't know how to do better.
 
 % Style for declaration keywords

doc/monads/readers.lean

@@ -113,7 +113,7 @@ the monadic container type.
 to write `(readerFunc3 args).run env` and this is a bit ugly, so Lean provides an infix operator
 `|>` that eliminates those parentheses so you can write `readerFunc3 args |>.run env` and then you can
 chain multiple monadic actions like this `m1 args1 |>.run args2 |>.run args3` and this is the
-recommended style.  You will see this patten used heavily in Lean code.
+recommended style.  You will see this pattern used heavily in Lean code.
 
 The `let env ← read` expression in `readerFunc1` unwraps the environment from the `ReaderM` so we
 can use it. Each type of monad might provide one or more extra functions like this, functions that