merge master

Author: Kha

.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@v8 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts

doc/declarations.md

@@ -764,11 +764,12 @@ Structures and Records
 The ``structure`` command in Lean is used to define an inductive data type with a single constructor and to define its projections at the same time. The syntax is as follows:
 
 ```
-structure Foo (a : α) extends Bar, Baz : Sort u :=
+structure Foo (a : α) : Sort u extends Bar, Baz :=
 constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)
 ```
 
-Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
+Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible (unless all the fields are ``Prop``, in which case it infers ``Prop``).
+Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
 
 The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
 

script/prepare-llvm-mingw.sh

@@ -25,7 +25,10 @@ cp llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
 echo '
 // https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode
 #define SEM_FAILCRITICALERRORS 0x0001
-__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);' > stage1/include/clang/windows.h
+__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);
+// https://docs.microsoft.com/en-us/windows/console/setconsoleoutputcp
+#define CP_UTF8 65001
+__declspec(dllimport) __stdcall int SetConsoleOutputCP(unsigned int wCodePageID);' > stage1/include/clang/windows.h
 # COFF dependencies
 cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime

script/release_notes.py

@@ -65,20 +65,21 @@ def format_markdown_description(pr_number, description):
     link = f"[#{pr_number}](https://github.com/leanprover/lean4/pull/{pr_number})"
     return f"{link} {description}"
 
+def commit_types():
+    # see doc/dev/commit_convention.md
+    return ['feat', 'fix', 'doc', 'style', 'refactor', 'test', 'chore', 'perf']
+
 def count_commit_types(commits):
     counts = {
         'total': len(commits),
-        'feat': 0,
-        'fix': 0,
-        'refactor': 0,
-        'doc': 0,
-        'chore': 0
     }
+    for commit_type in commit_types():
+        counts[commit_type] = 0
 
     for _, first_line, _ in commits:
-        for commit_type in ['feat:', 'fix:', 'refactor:', 'doc:', 'chore:']:
-            if first_line.startswith(commit_type):
-                counts[commit_type.rstrip(':')] += 1
+        for commit_type in commit_types():
+            if first_line.startswith(f'{commit_type}:'):
+                counts[commit_type] += 1
                 break
 
     return counts
@@ -158,8 +159,9 @@ def main():
     counts = count_commit_types(commits)
     print(f"For this release, {counts['total']} changes landed. "
           f"In addition to the {counts['feat']} feature additions and {counts['fix']} fixes listed below "
-          f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements "
-          f"and {counts['chore']} chores.\n")
+          f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements, "
+          f"{counts['perf']} performance improvements, {counts['test']} improvements to the test suite "
+          f"and {counts['style'] + counts['chore']} other changes.\n")
 
     section_order = sort_sections_order()
     sorted_changelog = sorted(changelog.items(), key=lambda item: section_order.index(format_section_title(item[0])) if format_section_title(item[0]) in section_order else len(section_order))

src/CMakeLists.txt

@@ -805,8 +805,6 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC
 string(APPEND LEANC_OPTS " ${LEANC_EXTRA_CC_FLAGS} ${LEANC_INTERNAL_FLAGS}")
 set(LINK_OPTS "${LEANC_INTERNAL_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -L${CMAKE_BINARY_DIR}/lib/lean")
 
-set(LAKE_PREV_PLUGIN "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}")
-
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
 string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")

src/Init/Control/Basic.lean

@@ -78,7 +78,7 @@ Error recovery and state can interact subtly. For example, the implementation of
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add
 -- * `List`, where `failure` is the empty list and `<|>` concatenates.
-class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
+class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicative f where
   /--
   Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
   from failures. See `Alternative` for more details.

src/Init/Control/Lawful/Basic.lean

@@ -47,7 +47,7 @@ pure f <*> pure x = pure (f x)
 u <*> pure y = pure (· y) <*> u
 ```
 -/
-class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where
+class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f where
   seqLeft_eq  (x : f α) (y : f β)     : x <* y = const β <$> x <*> y
   seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
   pure_seq    (g : α → β) (x : f α)   : pure g <*> x = g <$> x
@@ -77,7 +77,7 @@ x >>= f >>= g = x >>= (fun x => f x >>= g)
 
 `LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
 -/
-class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where
+class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m where
   bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
   bind_map       {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x
   pure_bind      (x : α) (f : α → m β) : pure x >>= f = f x

src/Init/Core.lean

@@ -2020,7 +2020,7 @@ free variables. The frontend automatically declares a fresh auxiliary constant `
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers (e.g., Trepplein) that do not implement this feature.
+external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 
@@ -2055,7 +2055,7 @@ decidability instance can be evaluated to `true` using the lean compiler / inter
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers (e.g., Trepplein) that do not implement this feature.
+external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
@@ -2066,7 +2066,7 @@ The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers (e.g., Trepplein) that do not implement this feature.
+external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
@@ -2125,7 +2125,7 @@ class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 `LawfulLeftIdentify op o` indicates `o` is a verified left identity of
 `op`.
 -/
-class LawfulLeftIdentity (op : α → β → β) (o : outParam α) extends LeftIdentity op o : Prop where
+class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
   /-- Left identity `o` is an identity. -/
   left_id : ∀ a, op o a = a
 
@@ -2141,7 +2141,7 @@ class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 `LawfulRightIdentify op o` indicates `o` is a verified right identity of
 `op`.
 -/
-class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends RightIdentity op o : Prop where
+class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where
   /-- Right identity `o` is an identity. -/
   right_id : ∀ a, op a o = a
 
@@ -2151,13 +2151,13 @@ class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends Righ
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
 -/
-class Identity (op : α → α → α) (o : outParam α) extends LeftIdentity op o, RightIdentity op o : Prop
+class Identity (op : α → α → α) (o : outParam α) : Prop extends LeftIdentity op o, RightIdentity op o
 
 /--
 `LawfulIdentity op o` indicates `o` is a verified left and right
 identity of `op`.
 -/
-class LawfulIdentity (op : α → α → α) (o : outParam α) extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o : Prop
+class LawfulIdentity (op : α → α → α) (o : outParam α) : Prop extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o
 
 /--
 `LawfulCommIdentity` can simplify defining instances of `LawfulIdentity`
@@ -2168,7 +2168,7 @@ This class is intended for simplifying defining instances of
 `LawfulIdentity` and functions needed commutative operations with
 identity should just add a `LawfulIdentity` constraint.
 -/
-class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] extends LawfulIdentity op o : Prop where
+class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] : Prop extends LawfulIdentity op o where
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 

src/Init/Data/Array/Attach.lean

@@ -8,8 +8,9 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
 import Init.Data.List.Attach
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -554,6 +555,10 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array 
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Array.map_push]
 
+@[simp] theorem mem_unattach {p : α → Prop} {xs : Array { x // p x }} {a} :
+    a ∈ xs.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ xs := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem size_unattach {p : α → Prop} {xs : Array { x // p x }} :
     xs.unattach.size = xs.size := by
   unfold unattach
@@ -675,6 +680,20 @@ and simplifies these to the function directly taking the value.
   simp
   rw [List.find?_subtype hf]
 
+@[simp] theorem all_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.all f 0 stop = xs.unattach.all g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.any f 0 stop = xs.unattach.any g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {xs : Array { x // p x }}

src/Init/Data/Array/Basic.lean

@@ -14,8 +14,8 @@ import Init.GetElem
 import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 universe u v w
 
@@ -144,6 +144,8 @@ end List
 
 namespace Array
 
+theorem size_eq_length_toList (xs : Array α) : xs.size = xs.toList.length := rfl
+
 @[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @List.toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -1090,6 +1092,11 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+def replace [BEq α] (xs : Array α) (a b : α) : Array α :=
+  match xs.finIdxOf? a with
+  | none => xs
+  | some i => xs.set i b
+
 /-! ### Lexicographic ordering -/
 
 instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩
@@ -1102,6 +1109,20 @@ instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toLi
 We do not currently intend to provide verification theorems for these functions.
 -/
 
+/-! ### leftpad and rightpad -/
+
+/--
+Pads `l : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`.
+If `l` is initially larger than `n`, just return `l`.
+-/
+def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs
+
+/--
+Pads `l : Array α` on the right with repeated occurrences of `a : α` until it is of size `n`.
+If `l` is initially larger than `n`, just return `l`.
+-/
+def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a
+
 /- ### reduceOption -/
 
 /-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/

src/Init/Data/Array/BasicAux.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
   simp only [push, mk.injEq] at h

src/Init/Data/Array/BinSearch.lean

@@ -9,7 +9,7 @@ import Init.Data.Int.DivMod.Lemmas
 import Init.Omega
 universe u v
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not use `linter.indexVariables` here as it is helpful to name the index variables as `lo`, `mid`, and `hi`.
 
 namespace Array

src/Init/Data/Array/Bootstrap.lean

@@ -13,8 +13,8 @@ import Init.Data.List.TakeDrop
 This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 

src/Init/Data/Array/Count.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Nat.Count
 # Lemmas about `Array.countP` and `Array.count`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -23,6 +23,18 @@ section countP
 
 variable (p q : α → Bool)
 
+@[simp] theorem _root_.List.countP_toArray (l : List α) : countP p l.toArray = l.countP p := by
+  simp [countP]
+  induction l with
+  | nil => rfl
+  | cons hd tl ih =>
+    simp only [List.foldr_cons, ih, List.countP_cons]
+    split <;> simp_all
+
+@[simp] theorem countP_toList (xs : Array α) : xs.toList.countP p = countP p xs := by
+  cases xs
+  simp
+
 @[simp] theorem countP_empty : countP p #[] = 0 := rfl
 
 @[simp] theorem countP_push_of_pos (xs) (pa : p a) : countP p (xs.push a) = countP p xs + 1 := by
@@ -150,6 +162,13 @@ section count
 
 variable [BEq α]
 
+@[simp] theorem _root_.List.count_toArray (l : List α) (a : α) : count a l.toArray = l.count a := by
+  simp [count, List.count_eq_countP]
+
+@[simp] theorem count_toList (xs : Array α) (a : α) : xs.toList.count a = xs.count a := by
+  cases xs
+  simp
+
 @[simp] theorem count_empty (a : α) : count a #[] = 0 := rfl
 
 theorem count_push (a b : α) (xs : Array α) :

src/Init/Data/Array/DecidableEq.lean

@@ -9,8 +9,8 @@ import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array