Skip to content

Commit da2132e

Browse files
nomeatanomeata
committed
Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/private-eqns
2 parents a13df08 + 0f4459b commit da2132e

921 files changed

Lines changed: 315615 additions & 214291 deletions

File tree

Some content is hidden

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

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -105,11 +105,11 @@ jobs:
105105
path: |
106106
.ccache
107107
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
108-
build/stage1/**/*.olean
108+
build/stage1/**/*.olean*
109109
build/stage1/**/*.ilean
110110
build/stage1/**/*.c
111111
build/stage1/**/*.c.o*' || '' }}
112-
key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
112+
key: ${{ matrix.name }}-build-v3-${{ github.sha }}
113113
# fall back to (latest) previous cache
114114
restore-keys: |
115115
${{ matrix.name }}-build-v3
@@ -243,7 +243,7 @@ jobs:
243243
path: |
244244
.ccache
245245
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
246-
build/stage1/**/*.olean
246+
build/stage1/**/*.olean*
247247
build/stage1/**/*.ilean
248248
build/stage1/**/*.c
249249
build/stage1/**/*.c.o*' || '' }}

‎.github/workflows/ci.yml‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,13 @@ jobs:
103103
echo "Tag ${TAG_NAME} did not match SemVer regex."
104104
fi
105105
106+
- name: Check for custom releases (e.g., not in the main lean repository)
107+
if: startsWith(github.ref, 'refs/tags/') && github.repository != 'leanprover/lean4'
108+
id: set-release-custom
109+
run: |
110+
TAG_NAME="${GITHUB_REF##*/}"
111+
echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
112+
106113
- name: Set check level
107114
id: set-level
108115
# We do not use github.event.pull_request.labels.*.name here because
@@ -111,7 +118,7 @@ jobs:
111118
run: |
112119
check_level=0
113120
114-
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then
121+
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
115122
check_level=2
116123
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
117124
check_level=1

‎.github/workflows/pr-release.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ jobs:
3434
- name: Download artifact from the previous workflow.
3535
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
3636
id: download-artifact
37-
uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
37+
uses: dawidd6/action-download-artifact@v10 # https://github.com/marketplace/actions/download-workflow-artifact
3838
with:
3939
run_id: ${{ github.event.workflow_run.id }}
4040
path: artifacts

‎src/Init/Control/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ abbrev forIn_eq_forin' := @forIn_eq_forIn'
4949
/--
5050
Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
5151
-/
52-
def ForInStep.value (x : ForInStep α) : α :=
52+
@[expose] def ForInStep.value (x : ForInStep α) : α :=
5353
match x with
5454
| ForInStep.done b => b
5555
| ForInStep.yield b => b

‎src/Init/Control/Except.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -136,15 +136,15 @@ may throw the corresponding exception.
136136
137137
This is the inverse of `ExceptT.run`.
138138
-/
139-
@[always_inline, inline]
139+
@[always_inline, inline, expose]
140140
def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
141141

142142
/--
143143
Use a monadic action that may throw an exception as an action that may return an exception's value.
144144
145145
This is the inverse of `ExceptT.mk`.
146146
-/
147-
@[always_inline, inline]
147+
@[always_inline, inline, expose]
148148
def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
149149

150150
namespace ExceptT
@@ -154,14 +154,14 @@ variable {ε : Type u} {m : Type u → Type v} [Monad m]
154154
/--
155155
Returns the value `a` without throwing exceptions or having any other effect.
156156
-/
157-
@[always_inline, inline]
157+
@[always_inline, inline, expose]
158158
protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
159159
ExceptT.mk <| pure (Except.ok a)
160160

161161
/--
162162
Handles exceptions thrown by an action that can have no effects _other_ than throwing exceptions.
163163
-/
164-
@[always_inline, inline]
164+
@[always_inline, inline, expose]
165165
protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
166166
| Except.ok a => f a
167167
| Except.error e => pure (Except.error e)
@@ -170,14 +170,14 @@ protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε
170170
Sequences two actions that may throw exceptions. Typically used via `do`-notation or the `>>=`
171171
operator.
172172
-/
173-
@[always_inline, inline]
173+
@[always_inline, inline, expose]
174174
protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
175175
ExceptT.mk <| ma >>= ExceptT.bindCont f
176176

177177
/--
178178
Transforms a successful computation's value using `f`. Typically used via the `<$>` operator.
179179
-/
180-
@[always_inline, inline]
180+
@[always_inline, inline, expose]
181181
protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
182182
ExceptT.mk <| x >>= fun a => match a with
183183
| (Except.ok a) => pure <| Except.ok (f a)
@@ -186,7 +186,7 @@ protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : Excep
186186
/--
187187
Runs a computation from an underlying monad in the transformed monad with exceptions.
188188
-/
189-
@[always_inline, inline]
189+
@[always_inline, inline, expose]
190190
protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
191191
ExceptT.mk <| Except.ok <$> t
192192

@@ -197,7 +197,7 @@ instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
197197
/--
198198
Handles exceptions produced in the `ExceptT ε` transformer.
199199
-/
200-
@[always_inline, inline]
200+
@[always_inline, inline, expose]
201201
protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
202202
ExceptT.mk <| ma >>= fun res => match res with
203203
| Except.ok a => pure (Except.ok a)

‎src/Init/Control/ExceptCps.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ namespace ExceptCpsT
2525
/--
2626
Use a monadic action that may throw an exception as an action that may return an exception's value.
2727
-/
28-
@[always_inline, inline]
28+
@[always_inline, inline, expose]
2929
def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
3030
x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
3131

@@ -43,7 +43,7 @@ Returns the value of a computation, forgetting whether it was an exception or a
4343
4444
This corresponds to early return.
4545
-/
46-
@[always_inline, inline]
46+
@[always_inline, inline, expose]
4747
def runCatch [Monad m] (x : ExceptCpsT α m α) : m α :=
4848
x α pure pure
4949

@@ -63,7 +63,7 @@ instance : MonadExceptOf ε (ExceptCpsT ε m) where
6363
/--
6464
Run an action from the transformed monad in the exception monad.
6565
-/
66-
@[always_inline, inline]
66+
@[always_inline, inline, expose]
6767
def lift [Monad m] (x : m α) : ExceptCpsT ε m α :=
6868
fun _ k _ => x >>= k
6969

‎src/Init/Control/Lawful.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ prelude
99
import Init.Control.Lawful.Basic
1010
import Init.Control.Lawful.Instances
1111
import Init.Control.Lawful.Lemmas
12+
import Init.Control.Lawful.MonadLift

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
module
7+
8+
prelude
9+
import Init.Control.Lawful.MonadLift.Basic
10+
import Init.Control.Lawful.MonadLift.Lemmas
11+
import Init.Control.Lawful.MonadLift.Instances

‎src/Init/Control/Lawful/MonadLift/Basic.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/-
2+
Copyright (c) 2025 Quang Dao. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao
5+
-/
6+
module
7+
8+
prelude
9+
import Init.Control.Basic
10+
11+
/-!
12+
# LawfulMonadLift and LawfulMonadLiftT
13+
14+
This module provides classes asserting that `MonadLift` and `MonadLiftT` are lawful, which means
15+
that `monadLift` is compatible with `pure` and `bind`.
16+
-/
17+
18+
section MonadLift
19+
20+
/-- The `MonadLift` typeclass only contains the lifting operation. `LawfulMonadLift` further
21+
asserts that lifting commutes with `pure` and `bind`:
22+
```
23+
monadLift (pure a) = pure a
24+
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
25+
```
26+
-/
27+
class LawfulMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
28+
[Monad m] [Monad n] [inst : MonadLift m n] : Prop where
29+
/-- Lifting preserves `pure` -/
30+
monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
31+
/-- Lifting preserves `bind` -/
32+
monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
33+
inst.monadLift (ma >>= f) = inst.monadLift ma >>= (fun x => inst.monadLift (f x))
34+
35+
/-- The `MonadLiftT` typeclass only contains the transitive lifting operation.
36+
`LawfulMonadLiftT` further asserts that lifting commutes with `pure` and `bind`:
37+
```
38+
monadLift (pure a) = pure a
39+
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
40+
```
41+
-/
42+
class LawfulMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
43+
[inst : MonadLiftT m n] : Prop where
44+
/-- Lifting preserves `pure` -/
45+
monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
46+
/-- Lifting preserves `bind` -/
47+
monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
48+
inst.monadLift (ma >>= f) = monadLift ma >>= (fun x => monadLift (f x))
49+
50+
export LawfulMonadLiftT (monadLift_pure monadLift_bind)
51+
52+
end MonadLift

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

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
/-
2+
Copyright (c) 2025 Quang Dao. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao, Paul Reichert
5+
-/
6+
module
7+
8+
prelude
9+
import all Init.Control.Option
10+
import all Init.Control.Except
11+
import all Init.Control.ExceptCps
12+
import all Init.Control.StateRef
13+
import all Init.Control.StateCps
14+
import Init.Control.Lawful.MonadLift.Lemmas
15+
import Init.Control.Lawful.Instances
16+
17+
universe u v w x
18+
19+
variable {m : Type u → Type v} {n : Type u → Type w} {o : Type u → Type x}
20+
21+
variable (m n o) in
22+
instance [Monad m] [Monad n] [Monad o] [MonadLift n o] [MonadLiftT m n]
23+
[LawfulMonadLift n o] [LawfulMonadLiftT m n] : LawfulMonadLiftT m o where
24+
monadLift_pure := fun a => by
25+
simp only [monadLift, LawfulMonadLift.monadLift_pure, liftM_pure]
26+
monadLift_bind := fun ma f => by
27+
simp only [monadLift, LawfulMonadLift.monadLift_bind, liftM_bind]
28+
29+
variable (m) in
30+
instance [Monad m] : LawfulMonadLiftT m m where
31+
monadLift_pure _ := rfl
32+
monadLift_bind _ _ := rfl
33+
34+
namespace StateT
35+
36+
variable [Monad m] [LawfulMonad m]
37+
38+
instance {σ : Type u} : LawfulMonadLift m (StateT σ m) where
39+
monadLift_pure _ := by ext; simp [MonadLift.monadLift]
40+
monadLift_bind _ _ := by ext; simp [MonadLift.monadLift]
41+
42+
end StateT
43+
44+
namespace ReaderT
45+
46+
variable [Monad m]
47+
48+
instance {ρ : Type u} : LawfulMonadLift m (ReaderT ρ m) where
49+
monadLift_pure _ := rfl
50+
monadLift_bind _ _ := rfl
51+
52+
end ReaderT
53+
54+
namespace OptionT
55+
56+
variable [Monad m] [LawfulMonad m]
57+
58+
@[simp]
59+
theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
60+
simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
61+
62+
@[simp]
63+
theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
64+
OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
65+
simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
66+
map_bind]
67+
68+
instance : LawfulMonadLift m (OptionT m) where
69+
monadLift_pure := lift_pure
70+
monadLift_bind := lift_bind
71+
72+
end OptionT
73+
74+
namespace ExceptT
75+
76+
variable [Monad m] [LawfulMonad m]
77+
78+
@[simp]
79+
theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
80+
ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
81+
simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
82+
83+
instance : LawfulMonadLift m (ExceptT ε m) where
84+
monadLift_pure := lift_pure
85+
monadLift_bind := lift_bind
86+
87+
instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
88+
monadLift_pure _ := by
89+
simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
90+
monadLift_bind ma _ := by
91+
simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
92+
Except.instMonad, Except.bind]
93+
rcases ma with _ | _ <;> simp
94+
95+
end ExceptT
96+
97+
namespace StateRefT'
98+
99+
instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
100+
monadLift_pure _ := by
101+
simp only [MonadLift.monadLift, pure]
102+
unfold StateRefT'.lift ReaderT.pure
103+
simp only
104+
monadLift_bind _ _ := by
105+
simp only [MonadLift.monadLift, bind]
106+
unfold StateRefT'.lift ReaderT.bind
107+
simp only
108+
109+
end StateRefT'
110+
111+
namespace StateCpsT
112+
113+
instance {σ : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (StateCpsT σ m) where
114+
monadLift_pure _ := by
115+
simp only [MonadLift.monadLift, pure]
116+
unfold StateCpsT.lift
117+
simp only [pure_bind]
118+
monadLift_bind _ _ := by
119+
simp only [MonadLift.monadLift, bind]
120+
unfold StateCpsT.lift
121+
simp only [bind_assoc]
122+
123+
end StateCpsT
124+
125+
namespace ExceptCpsT
126+
127+
instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT ε m) where
128+
monadLift_pure _ := by
129+
simp only [MonadLift.monadLift, pure]
130+
unfold ExceptCpsT.lift
131+
simp only [pure_bind]
132+
monadLift_bind _ _ := by
133+
simp only [MonadLift.monadLift, bind]
134+
unfold ExceptCpsT.lift
135+
simp only [bind_assoc]
136+
137+
end ExceptCpsT

0 commit comments

Comments
 (0)