chore: merge

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,6 +5,7 @@
 * Include the link to your `RFC` or `bug` issue in the description.
 * If the issue does not already have approval from a developer, submit the PR as draft.
 * The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
+* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
 * If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
 * You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
 * Remove this section, up to and including the `---` before submitting.

.github/workflows/ci.yml

@@ -114,7 +114,7 @@ jobs:
           elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
             check_level=1
           else
-            labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}) --jq '.labels'"
+            labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
             if echo "$labels" | grep -q "release-ci"; then
               check_level=2
             elif echo "$labels" | grep -q "merge-ci"; then

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

@@ -1,6 +1,7 @@
-# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
-# by commenting on the PR or issue.
-# Other labels from this set are removed automatically at the same time.
+# 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.
+# 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.
 
 name: Label PR based on Comment
 
@@ -10,7 +11,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'))
+    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'))
     runs-on: ubuntu-latest
 
     steps:
@@ -25,6 +26,7 @@ jobs:
           const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
+          const releaseCI = commentLines.includes('release-ci');
 
           if (awaitingReview || awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -41,3 +43,7 @@ jobs:
           if (wip) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
           }
+
+          if (releaseCI) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
+          }

doc/dev/release_checklist.md

@@ -71,6 +71,12 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
+    - [Verso](https://github.com/leanprover/verso)
+      - Dependencies: exist, but they're not part of the release workflow
+      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
+      - Toolchain bump PR including updated Lake manifest
+      - Create and push the tag
+      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

nix/bootstrap.nix

@@ -95,12 +95,13 @@ lib.warn "The Nix-based build is deprecated" rec {
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
       Lake = build {
         name = "Lake";
+        sharedLibName = "Lake_shared";
         src = src + "/src/lake";
         deps = [ Init Lean ];
       };
       Lake-Main = build {
-        name = "Lake.Main";
-        roots = [ "Lake.Main" ];
+        name = "LakeMain";
+        roots = [{ glob = "one"; mod = "LakeMain"; }];
         executableName = "lake";
         deps = [ Lake ];
         linkFlags = lib.optional stdenv.isLinux "-rdynamic";
@@ -133,7 +134,7 @@ lib.warn "The Nix-based build is deprecated" rec {
       mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
       print-paths = Lean.makePrintPathsFor [] mods;
       leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} "$@"
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
       '';
       lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
         mkdir -p $out/bin
@@ -144,7 +145,7 @@ lib.warn "The Nix-based build is deprecated" rec {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* $out/lib/lean/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
           cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`
@@ -177,7 +178,7 @@ lib.warn "The Nix-based build is deprecated" rec {
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';

nix/buildLeanPackage.nix

@@ -30,7 +30,7 @@ lib.makeOverridable (
   pluginDeps ? [],
   # `overrideAttrs` for `buildMod`
   overrideBuildModAttrs ? null,
-  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name,
+  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
   srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
 with builtins; let
   # "Init.Core" ~> "Init/Core"
@@ -233,7 +233,7 @@ in rec {
   cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
   oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
   iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
-  sharedLib = mkSharedLib "lib${libName}" ''
+  sharedLib = mkSharedLib "lib${sharedLibName}" ''
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let

script/lib/update-stage0

@@ -18,7 +18,7 @@ done
 
 # special handling for Lake files due to its nested directory
 # copy the README to ensure the `stage0/src/lake` directory is comitted
-for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/README.md ':!:src/lakefile.toml'); do
+for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
     if [[ $f == *.lean ]]; then
         f=${f#src/lake}
         f=${f%.lean}.c

src/CMakeLists.txt

@@ -333,7 +333,12 @@ if(NOT LEAN_STANDALONE)
 endif()
 
 # flags for user binaries = flags for toolchain binaries + Lake
-string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
+set(LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+  set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -Wl,--as-needed -lLake_shared -Wl,--no-as-needed")
+else()
+  set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -lLake_shared")
+endif()
 
 if (LLVM)
   string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
@@ -378,16 +383,20 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
   string(APPEND LEANC_EXTRA_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")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
   string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
   string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
+  string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -install_name @rpath/libLake_shared.dylib")
   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")
+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()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -587,8 +596,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   )
   add_custom_target(leanshared ALL
     DEPENDS Init_shared leancpp
+    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
     COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
   )
+  add_custom_target(lake_shared ALL
+    DEPENDS leanshared
+    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
+  )
 else()
   add_custom_target(Init_shared ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
@@ -606,11 +620,21 @@ else()
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_custom_target(lake ALL
+  add_custom_target(lake_lib ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
     VERBATIM)
+  add_custom_target(lake_shared ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_lib
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
+    VERBATIM)
+  add_custom_target(lake ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_shared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
+    VERBATIM)
 endif()
 
 if(PREV_STAGE)

src/Init/ByCases.lean

@@ -40,21 +40,23 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
 
--- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
+@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
 theorem ite_some_none_eq_none [Decidable P] :
     (if P then some x else none) = none ↔ ¬ P := by
   simp only [ite_eq_right_iff, reduceCtorEq]
   rfl
 
-@[simp] theorem ite_some_none_eq_some [Decidable P] :
+@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
+theorem ite_some_none_eq_some [Decidable P] :
     (if P then some x else none) = some y ↔ P ∧ x = y := by
   split <;> simp_all
 
--- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
+@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
 theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
     (if h : P then some (x h) else none) = none ↔ ¬P := by
   simp
 
-@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
+theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
     (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
   by_cases h : P <;> simp [h]

src/Init/Classical.lean

@@ -134,6 +134,30 @@ The left-to-right direction, double negation elimination (DNE),
 is classically true but not constructively. -/
 @[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
 
+/-- Transfer decidability of `¬ p` to decidability of `p`. -/
+-- This can not be an instance as it would be tried everywhere.
+def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
+  match h with
+  | isFalse h => isTrue (Classical.not_not.mp h)
+  | isTrue h => isFalse h
+
+attribute [local instance] decidable_of_decidable_not in
+/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
+@[simp low] protected theorem dite_not [hn : Decidable (¬p)] (x : ¬p → α) (y : ¬¬p → α) :
+    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
+  cases hn <;> rename_i g
+  · simp [not_not.mp g]
+  · simp [g]
+
+attribute [local instance] decidable_of_decidable_not in
+/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
+@[simp low] protected theorem ite_not (p : Prop) [Decidable (¬ p)] (x y : α) : ite (¬p) x y = ite p y x :=
+  dite_not (fun _ => x) (fun _ => y)
+
+attribute [local instance] decidable_of_decidable_not in
+@[simp low] protected theorem decide_not (p : Prop) [Decidable (¬ p)] : decide (¬p) = !decide p :=
+  byCases (fun h : p => by simp_all) (fun h => by simp_all)
+
 @[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
 
 theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not

src/Init/Control/Basic.lean

@@ -28,7 +28,7 @@ Important instances include
 * `Option`, where `failure := none` and `<|>` returns the left-most `some`.
 * Parser combinators typically provide an `Applicative` instance for error-handling and
   backtracking.
-  
+
 Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add

src/Init/Core.lean

@@ -817,7 +817,7 @@ variable {a b c d : Prop}
 theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
   Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
 
-theorem Iff.refl (a : Prop) : a ↔ a :=
+@[refl] theorem Iff.refl (a : Prop) : a ↔ a :=
   Iff.intro (fun h => h) (fun h => h)
 
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
@@ -1193,6 +1193,21 @@ end
 
 /-! # Product -/
 
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨(x, y)⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (default, default)
 
@@ -1367,6 +1382,11 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
+/-- Replacement for `Array.mk.injEq`; we avoid mentioning the constructor and prefer `List.toArray`. -/
+abbrev List.toArray_inj := @Array.mk.injEq
+
+attribute [deprecated List.toArray_inj (since := "2024-09-09")] Array.mk.injEq
+
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
 

src/Init/Data.lean

@@ -39,3 +39,5 @@ import Init.Data.BEq
 import Init.Data.Subtype
 import Init.Data.ULift
 import Init.Data.PLift
+import Init.Data.Zero
+import Init.Data.NeZero

src/Init/Data/Array.lean

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit

src/Init/Data/Array/Attach.lean

@@ -20,7 +20,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   with the same elements but in the type `{x // P x}`. -/
 @[implemented_by attachWithImpl] def attachWith
     (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
-  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+  ⟨xs.toList.attachWith P fun x h => H x (Array.Mem.mk h)⟩
 
 /-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
   with the same elements but in the type `{x // x ∈ xs}`. -/