Skip to content

Commit dfcd414

Browse files
KhaKha
committed
merge nightly-with-mathlib
2 parents e8a8ab2 + c75d37f commit dfcd414

File tree

1,288 files changed

+659467
-574501
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,288 files changed

+659467
-574501
lines changed

‎.github/workflows/build-template.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -229,7 +229,7 @@ jobs:
229229
id: test
230230
run: |
231231
ulimit -c unlimited # coredumps
232-
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml
232+
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
233233
if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
234234
- name: Test Summary
235235
uses: test-summary/action@v2

‎.github/workflows/ci.yml‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -200,8 +200,6 @@ jobs:
200200
"os": "ubuntu-latest",
201201
"check-level": 2,
202202
"CMAKE_PRESET": "reldebug",
203-
// exclude seriously slow/stackoverflowing tests
204-
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress|3807'"
205203
},
206204
// TODO: suddenly started failing in CI
207205
/*{
@@ -247,8 +245,6 @@ jobs:
247245
"check-level": 2,
248246
"shell": "msys2 {0}",
249247
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
250-
// for reasons unknown, interactivetests are flaky on Windows
251-
"CTEST_OPTIONS": "--repeat until-pass:2",
252248
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
253249
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
254250
"binary-check": "ldd",

‎doc/dev/index.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ You should not edit the `stage0` directory except using the commands described i
88

99
## Development Setup
1010

11-
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
11+
You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code.
1212
Please see below for specific instructions for VS Code.
1313

1414
### Dev setup using elan

‎doc/make/index.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
22

3-
We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
3+
We strongly suggest that new users instead follow the [Installation Instructions](https://lean-lang.org/install/) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
44

55
Requirements
66
------------

‎src/Init/Control/EState.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ variable {ε σ α : Type u}
1919

2020
instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
2121
toString
22-
| Result.ok a _ => "ok: " ++ toString a
23-
| Result.error e _ => "error: " ++ toString e
22+
| Result.ok a _ => String.Internal.append "ok: " (toString a)
23+
| Result.error e _ => String.Internal.append "error: " (toString e)
2424

2525
instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
2626
reprPrec

‎src/Init/Control/Lawful/Instances.lean‎

Lines changed: 31 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -22,34 +22,35 @@ open Function
2222

2323
namespace ExceptT
2424

25-
@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
25+
@[ext, grind ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
2626
simp [run] at h
2727
assumption
2828

29-
@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
29+
@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
3030

31-
@[simp] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
31+
@[simp, grind =] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
3232

33-
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
33+
@[simp, grind =] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
3434

35-
@[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
35+
@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
3636
simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
3737

38-
@[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
38+
@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
3939
simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
4040

41-
theorem run_bind [Monad m] (x : ExceptT ε m α)
41+
@[grind =]
42+
theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
4243
: run (x >>= f : ExceptT ε m β)
4344
=
4445
run x >>= fun
4546
| Except.ok x => run (f x)
4647
| Except.error e => pure (Except.error e) :=
4748
rfl
4849

49-
@[simp] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
50+
@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
5051
simp [ExceptT.lift, pure, ExceptT.pure]
5152

52-
@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
53+
@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
5354
: (f <$> x).run = Except.map f <$> x.run := by
5455
simp [Functor.map, ExceptT.map, ←bind_pure_comp]
5556
apply bind_congr
@@ -113,28 +114,28 @@ instance : LawfulFunctor (Except ε) := inferInstance
113114

114115
namespace ReaderT
115116

116-
@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
117+
@[ext, grind ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
117118
simp [run] at h
118119
exact funext h
119120

120-
@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
121+
@[simp, grind =] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
121122

122-
@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
123+
@[simp, grind =] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
123124
: (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
124125

125-
@[simp] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
126+
@[simp, grind =] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
126127
: (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
127128

128-
@[simp] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
129+
@[simp, grind =] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
129130
: (f <$> x).run ctx = f <$> x.run ctx := rfl
130131

131-
@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
132+
@[simp, grind =] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
132133
: (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
133134

134-
@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
135+
@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
135136
: (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
136137

137-
@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
138+
@[simp, grind =] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
138139

139140
@[simp] theorem run_seq {α β : Type u} [Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ)
140141
: (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := rfl
@@ -175,38 +176,39 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
175176

176177
namespace StateT
177178

178-
@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
179+
@[ext, grind ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
179180
funext h
180181

181-
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
182+
@[simp, grind =] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
182183
rfl
183184

184-
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
185+
@[simp, grind =] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
185186

186-
@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
187+
@[simp, grind =] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
187188
: (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2 := by
188189
simp [bind, StateT.bind, run]
189190

190-
@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
191+
@[simp, grind =] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
191192
simp [Functor.map, StateT.map, run, ←bind_pure_comp]
192193

193-
@[simp] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
194+
@[simp, grind =] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
194195

195-
@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
196+
@[simp, grind =] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
196197

197-
@[simp] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
198+
@[simp, grind =] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
198199

199-
@[simp] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
200+
@[simp, grind =] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
200201
simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]
201202

202-
@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
203+
@[simp, grind =] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
203204

205+
@[grind =]
204206
theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
205207
simp [StateT.lift, StateT.run, bind, StateT.bind]
206208

207-
@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
209+
@[simp, grind =] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
208210

209-
@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
211+
@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
210212
(monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
211213

212214
@[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by

‎src/Init/Core.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,6 @@ instance : DecidableEq Empty := fun a => a.elim
101101
/-- Decidable equality for PEmpty -/
102102
instance : DecidableEq PEmpty := fun a => a.elim
103103

104-
set_option genInjectivity false in
105104
/--
106105
Delays evaluation. The delayed code is evaluated at most once.
107106
@@ -617,7 +616,6 @@ class Sep (α : outParam <| Type u) (γ : Type v) where
617616
/-- Computes `{ a ∈ c | p a }`. -/
618617
sep : (α → Prop) → γ → γ
619618

620-
set_option genInjectivity false in
621619
/--
622620
`Task α` is a primitive for asynchronous computation.
623621
It represents a computation that will resolve to a value of type `α`,

‎src/Init/Data/Array/Basic.lean‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,6 @@ public import Init.WFTactics
1010
public import Init.Data.Nat.Basic
1111
public import Init.Data.Fin.Basic
1212
public import Init.Data.UInt.BasicAux
13-
public import Init.Data.Repr
14-
public import Init.Data.ToString.Basic
1513
public import Init.GetElem
1614
public import Init.Data.List.ToArrayImpl
1715
import all Init.Data.List.ToArrayImpl
@@ -164,7 +162,7 @@ This is a low-level version of `Array.size` that directly queries the runtime sy
164162
representation of arrays. While this is not provable, `Array.usize` always returns the exact size of
165163
the array since the implementation only supports arrays of size less than `USize.size`.
166164
-/
167-
@[extern "lean_array_size", simp]
165+
@[extern "lean_array_size", simp, expose]
168166
def usize (xs : @& Array α) : USize := xs.size.toUSize
169167

170168
/--
@@ -443,7 +441,7 @@ def swapAt! (xs : Array α) (i : Nat) (v : α) : α × Array α :=
443441
swapAt xs i v
444442
else
445443
have : Inhabited (α × Array α) := ⟨(v, xs)⟩
446-
panic! ("index " ++ toString i ++ " out of bounds")
444+
panic! String.Internal.append (String.Internal.append "index " (toString i)) " out of bounds"
447445
448446
/--
449447
Returns the first `n` elements of an array. The resulting array is produced by repeatedly calling
@@ -2169,7 +2167,7 @@ instance {α : Type u} [Repr α] : Repr (Array α) where
21692167
reprPrec xs _ := Array.repr xs
21702168

21712169
instance [ToString α] : ToString (Array α) where
2172-
toString xs := "#" ++ toString xs.toList
2170+
toString xs := String.Internal.append "#" (toString xs.toList)
21732171

21742172
end Array
21752173

‎src/Init/Data/Array/Find.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -728,7 +728,7 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
728728
cases xs
729729
simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
730730
rw [findFinIdx?_congr List.unattach_toArray]
731-
simp only [Option.map_map, Function.comp_def, Fin.cast_trans]
731+
simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
732732
simp [Array.size]
733733

734734
/-! ### idxOf

‎src/Init/Data/Array/Lemmas.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ public import Init.Data.List.Monadic
1515
public import Init.Data.List.OfFn
1616
public import Init.Data.Array.Mem
1717
public import Init.Data.Array.DecidableEq
18-
public import Init.Data.Array.Lex.Basic
1918
public import Init.Data.Range.Lemmas
2019
public import Init.TacticsExtra
2120
public import Init.Data.List.ToArray

0 commit comments

Comments
 (0)