Merge branch 'master' into concat

.github/workflows/check-prelude.yml

@@ -14,14 +14,15 @@ jobs:
           sparse-checkout: |
             src/Lean
             src/Std
+            src/lake/Lake
       - name: Check Prelude
         run: |
           failed_files=""
           while IFS= read -r -d '' file; do
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std -name '*.lean' -print0)
+          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1

.github/workflows/labels-from-comments.yml

@@ -1,7 +1,8 @@
 # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# or `release-ci` labels by commenting on the PR or issue.
+# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
 # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
 # from that set are removed automatically at the same time.
+# Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
 
 name: Label PR based on Comment
 
@@ -11,7 +12,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -20,13 +21,14 @@ jobs:
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |
-          const { owner, repo, number: issue_number  } = context.issue;
+          const { owner, repo, number: issue_number } = context.issue;
           const commentLines = context.payload.comment.body.split('\r\n');
 
           const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
           const releaseCI = commentLines.includes('release-ci');
+          const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -47,3 +49,19 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
+
+          if (changelogMatch) {
+            const changelogLabel = changelogMatch.trim();
+            const { data: existingLabels } = await github.rest.issues.listLabelsOnIssue({ owner, repo, issue_number });
+            const changelogLabels = existingLabels.filter(label => label.name.startsWith('changelog-'));
+
+            // Remove all other changelog labels
+            for (const label of changelogLabels) {
+              if (label.name !== changelogLabel) {
+                await github.rest.issues.removeLabel({ owner, repo, issue_number, name: label.name }).catch(() => {});
+              }
+            }
+
+            // Add the new changelog label
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [changelogLabel] });
+          }

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v7 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -111,7 +111,7 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v2.1.0
+        uses: dcarbone/install-jq-action@v3.0.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD

RELEASES.md

@@ -8,11 +8,16 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.15.0
+v4.16.0
 ----------
 
 Development in progress.
 
+v4.15.0
+----------
+
+Release candidate, release notes will be copied from the branch `releases/v4.15.0` once completed.
+
 v4.14.0
 ----------
 
@@ -88,7 +93,7 @@ v4.13.0
   * [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
 
 * Metaprogramming
-  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)  
+  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
   * [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
   * [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
   * [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.

doc/dev/bootstrap.md

@@ -103,10 +103,21 @@ your PR using rebase merge, bypassing the merge queue.
 As written above, changes in meta code in the current stage usually will only
 affect later stages. This is an issue in two specific cases.
 
+* For the special case of *quotations*, it is desirable to have changes in builtin parsers affect them immediately: when the changes in the parser become active in the next stage, builtin macros implemented via quotations should generate syntax trees compatible with the new parser, and quotation patterns in builtin macros and elaborators should be able to match syntax created by the new parser and macros.
+  Since quotations capture the syntax tree structure during execution of the current stage and turn it into code for the next stage, we need to run the current stage's builtin parsers in quotations via the interpreter for this to work.
+  Caveats:
+  * We activate this behavior by default when building stage 1 by setting `-Dinternal.parseQuotWithCurrentStage=true`.
+    We force-disable it inside `macro/macro_rules/elab/elab_rules` via `suppressInsideQuot` as they are guaranteed not to run in the next stage and may need to be run in the current one, so the stage 0 parser is the correct one to use for them.
+    It may be necessary to extend this disabling to functions that contain quotations and are (exclusively) used by one of the mentioned commands. A function using quotations should never be used by both builtin and non-builtin macros/elaborators. Example: https://github.com/leanprover/lean4/blob/f70b7e5722da6101572869d87832494e2f8534b7/src/Lean/Elab/Tactic/Config.lean#L118-L122
+  * The parser needs to be reachable via an `import` statement, otherwise the version of the previous stage will silently be used.
+  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading tokens is taken from the previous stage.
+
+  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422R13
+
 * For *non-builtin* meta code such as `notation`s or `macro`s in
   `Notation.lean`, we expect changes to affect the current file and all later
   files of the same stage immediately, just like outside the stdlib. To ensure
-  this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
+  this, we build stage 1 using `-Dinterpreter.prefer_native=false` -
   otherwise, when executing a macro, the interpreter would notice that there is
   already a native symbol available for this function and run it instead of the
   new IR, but the symbol is from the previous stage!
@@ -124,26 +135,11 @@ affect later stages. This is an issue in two specific cases.
   further stages (e.g. after an `update-stage0`) will then need to be compiled
   with the flag set to `false` again since they will expect the new signature.
 
-  For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
-
-* For the special case of *quotations*, it is desirable to have changes in
-  built-in parsers affect them immediately: when the changes in the parser
-  become active in the next stage, macros implemented via quotations should
-  generate syntax trees compatible with the new parser, and quotation patterns
-  in macro and elaborators should be able to match syntax created by the new
-  parser and macros. Since quotations capture the syntax tree structure during
-  execution of the current stage and turn it into code for the next stage, we
-  need to run the current stage's built-in parsers in quotation via the
-  interpreter for this to work. Caveats:
-  * Since interpreting full parsers is not nearly as cheap and we rarely change
-    built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
-  * The parser needs to be reachable via an `import` statement, otherwise the
-    version of the previous stage will silently be used.
-  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading
-    tokens is taken from the previous stage.
-
-  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
-  (from before the flag defaulted to `false`).
+  When enabling `prefer_native`, we usually want to *disable* `parseQuotWithCurrentStage` as it would otherwise make quotations use the interpreter after all.
+  However, there is a specific case where we want to set both options to `true`: when we make changes to a non-builtin parser like `simp` that has a builtin elaborator, we cannot have the new parser be active outside of quotations in stage 1 as the builtin elaborator from stage 0 would not understand them; on the other hand, we need quotations in e.g. the builtin `simp` elaborator to produce the new syntax in the next stage.
+  As this issue usually affects only tactics, enabling `debug.byAsSorry` instead of `prefer_native` can be a simpler solution.
+
+  For a `prefer_native` example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
 
 To modify either of these flags both for building and editing the stdlib, adjust
 the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset

doc/examples/interp.lean

@@ -12,17 +12,17 @@ Remark: this example is based on an example found in the Idris manual.
 Vectors
 --------
 
-A `Vector` is a list of size `n` whose elements belong to a type `α`.
+A `Vec` is a list of size `n` whose elements belong to a type `α`.
 -/
 
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
 
 /-!
-We can overload the `List.cons` notation `::` and use it to create `Vector`s.
+We can overload the `List.cons` notation `::` and use it to create `Vec`s.
 -/
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vec.cons
 
 /-!
 Now, we define the types of our simple functional language.
@@ -50,11 +50,11 @@ the builtin instance for `Add Int` as the solution.
 /-!
 Expressions are indexed by the types of the local variables, and the type of the expression itself.
 -/
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vec Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
-inductive Expr : Vector Ty n → Ty → Type where
+inductive Expr : Vec Ty n → Ty → Type where
   | var   : HasType i ctx ty → Expr ctx ty
   | val   : Int → Expr ctx Ty.int
   | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
@@ -102,8 +102,8 @@ indexed over the types in scope. Since an environment is just another form of li
 to the vector of local variable types, we overload again the notation `::` so that we can use the usual list syntax.
 Given a proof that a variable is defined in the context, we can then produce a value from the environment.
 -/
-inductive Env : Vector Ty n → Type where
-  | nil  : Env Vector.nil
+inductive Env : Vec Ty n → Type where
+  | nil  : Env Vec.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons

doc/examples/tc.lean

@@ -82,9 +82,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
 /-!
 Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
 The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
-The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to rename "inaccessible" variables.
-We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
-by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
+The proof is by induction on `e` and case analysis. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
 the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
 -/
 theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by

doc/examples/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -Dlinter.all=false "$f"
+exec_check_raw lean -Dlinter.all=false "$f"

script/mathlib-bench

@@ -0,0 +1,12 @@
+#! /bin/env bash
+# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
+
+set -euo pipefail
+
+[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
+
+LEAN_PR=$1
+PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
+PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
+echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
+gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 15)
+set(LEAN_VERSION_MINOR 16)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -51,6 +51,8 @@ option(LLVM               "LLVM"               OFF)
 option(USE_GITHASH        "GIT_HASH"           ON)
 # When ON we install LICENSE files to CMAKE_INSTALL_PREFIX
 option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
+# When ON we install a copy of cadical
+option(INSTALL_CADICAL "Install a copy of cadical" ON)
 # When ON thread storage is automatically finalized, it assumes platform support pthreads.
 # This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell).
 option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON)
@@ -120,7 +122,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     # From https://emscripten.org/docs/compiling/WebAssembly.html#backends:
     # > The simple and safe thing is to pass all -s flags at both compile and link time.
     set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto")
-    string(APPEND LEANC_EXTRA_FLAGS " -pthread")
+    string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread")
     string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
     string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}")
 endif()
@@ -155,11 +157,11 @@ if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
 endif ()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
-string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
+string(APPEND LEANC_EXTRA_CC_FLAGS " -fstack-clash-protection")
 
 # This makes signed integer overflow guaranteed to match 2's complement.
 string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
-string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
+string(APPEND LEANC_EXTRA_CC_FLAGS " -fwrapv")
 
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
@@ -449,7 +451,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
     string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
   endif()
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
-  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
   string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
@@ -462,7 +464,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC")
-  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
 endif()
@@ -477,7 +479,7 @@ if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND NOT(${CMAKE_SYSTEM_NAME} MATC
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -rdynamic")
   # hide all other symbols
   string(APPEND CMAKE_CXX_FLAGS " -fvisibility=hidden -fvisibility-inlines-hidden")
-  string(APPEND LEANC_EXTRA_FLAGS " -fvisibility=hidden")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fvisibility=hidden")
 endif()
 
 # On Windows, add bcrypt for random number generation
@@ -542,9 +544,10 @@ include_directories(${CMAKE_BINARY_DIR}/include)  # config.h etc., "public" head
 string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
 
-# Do embed flag for finding system libraries in dev builds
+# Do embed flag for finding system headers and libraries in dev builds
 if(CMAKE_OSX_SYSROOT AND NOT LEAN_STANDALONE)
-  string(APPEND LEANC_EXTRA_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
 endif()
 
 add_subdirectory(initialize)
@@ -616,7 +619,7 @@ else()
     OUTPUT_NAME leancpp)
 endif()
 
-if((${STAGE} GREATER 0) AND CADICAL)
+if((${STAGE} GREATER 0) AND CADICAL AND INSTALL_CADICAL)
   add_custom_target(copy-cadical
     COMMAND cmake -E copy_if_different "${CADICAL}" "${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX}")
   add_dependencies(leancpp copy-cadical)
@@ -738,7 +741,7 @@ file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
 
 install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
 
-if (${STAGE} GREATER 0 AND CADICAL)
+if (${STAGE} GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   install(PROGRAMS "${CADICAL}" DESTINATION bin)
 endif()