c36b0fb165
This PR moves `IO.CancelToken` from `Init.System.IO` to its own file
`Init.System.CancelToken`, backed by `IO.Promise Unit` instead of
`IO.Ref Bool`. This enables non-polling cancellation propagation: the
token's underlying promise can be used directly with `IO.waitAny`, and
callbacks can be registered to fire when cancellation is requested.
The structure carries both the promise *and* a plain `IO.Ref Bool` flag,
set in lockstep by `set`. `isSet` reads the flag directly (used on hot
paths like `Core.checkInterrupted`); `task`/`onSet` go through the
promise. The avoids a ~0.4% regression that a pure-promise
representation introduced.
API additions:
- `CancelToken.task : Task (Option Unit)`. Returns the underlying
promise's `result?` task directly — the same task object on every call,
so further `Task.map`/`BaseIO.bindTask` dependencies can be safely
attached. Resolves with `some ()` when `set` is called, or `none` if the
token is dropped without ever being set.
- `CancelToken.onSet : BaseIO Unit → BaseIO Unit`. Registers a callback
that runs synchronously on the cancelling thread when `set` is called
(or immediately if the token is already set). Implemented via
`BaseIO.chainTask` on `result?`, so no fresh `Task.map` per call and no
GC hazard.
Runtime cleanup:
- Add `LEAN_TASK_STATE_{WAITING,RUNNING,FINISHED}` constants in `lean.h`
matching `IO.TaskState`.
- Factor `lean::promise_is_resolved` inline in `object.h`, replacing
three open-coded `lean_io_get_task_state_core(...) == 2` checks (in
`interrupt.cpp`, `uv/timer.cpp`, `uv/signal.cpp`).
- Drop the manual `inc_ref(g_cancel_tk)` in `check_interrupted`; the
token is owned by the enclosing `scope_cancel_tk` for the duration of
the call (documented).
- Replace the bare `lean_always_assert(g_task_manager)` in
`lean_promise_new` with an explicit `lean_internal_panic` carrying a
message that names `Promise.new`, identifies the typical trigger
(`initialize` blocks, transitively via `IO.CancelToken.new`), and
recommends lazy construction. Without this, users got an opaque "LEAN
ASSERTION VIOLATION ... Condition: g_task_manager" with no actionable
hint.
Behavioural notes documented inline:
- `new` cannot be called from `initialize` blocks (task manager not
running yet); construct lazily.
- `task` documents the dropped-promise case (`none`) and steers callers
to `onSet` for callback chaining.
A consumer of `onSet` for parent → child cancel-token propagation in
parallel tactic combinators is in #13428 (fixes #13300).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
170 lines
4.8 KiB
Text
170 lines
4.8 KiB
Text
/-!
|
||
# Test `#print` command for structures and classes
|
||
-/
|
||
|
||
/-! Structure -/
|
||
/--
|
||
info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
|
||
number of parameters: 2
|
||
fields:
|
||
Prod.fst : α
|
||
Prod.snd : β
|
||
constructor:
|
||
Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
|
||
-/
|
||
#guard_msgs in
|
||
#print Prod
|
||
|
||
/-! Class -/
|
||
/--
|
||
info: class Inhabited.{u} (α : Sort u) : Sort (max 1 u)
|
||
number of parameters: 1
|
||
fields:
|
||
Inhabited.default : α
|
||
constructor:
|
||
Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α
|
||
-/
|
||
#guard_msgs in
|
||
#print Inhabited
|
||
|
||
/-! Structure with private field, imported -/
|
||
/--
|
||
info: structure IO.Promise (α : Type) : Type
|
||
number of parameters: 1
|
||
fields:
|
||
private IO.Promise.prom✝ : IO.PromisePointed✝.type
|
||
private IO.Promise.h✝ : Nonempty α
|
||
constructor:
|
||
private IO.Promise.mk✝ {α : Type} (prom : IO.PromisePointed✝.type) (h : Nonempty α) : IO.Promise α
|
||
-/
|
||
#guard_msgs in
|
||
#print IO.Promise
|
||
|
||
/-! Structure with private field, current module -/
|
||
structure PrivField where
|
||
private x : Nat
|
||
|
||
/--
|
||
info: structure PrivField : Type
|
||
number of parameters: 0
|
||
fields:
|
||
private PrivField.x : Nat
|
||
constructor:
|
||
PrivField.mk (x : Nat) : PrivField
|
||
-/
|
||
#guard_msgs in
|
||
#print PrivField
|
||
|
||
/-! Private constructor, imported -/
|
||
/--
|
||
info: class TypeName.{u} (α : Type u) : Type
|
||
number of parameters: 1
|
||
fields:
|
||
private TypeName.data✝ : (TypeNameData α).type
|
||
constructor:
|
||
private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData α).type) : TypeName α
|
||
-/
|
||
#guard_msgs in
|
||
#print TypeName
|
||
|
||
/-! Private constructor, current module -/
|
||
structure PrivCtor where private mk ::
|
||
x : Nat
|
||
/--
|
||
info: structure PrivCtor : Type
|
||
number of parameters: 0
|
||
fields:
|
||
PrivCtor.x : Nat
|
||
constructor:
|
||
private PrivCtor.mk (x : Nat) : PrivCtor
|
||
-/
|
||
#guard_msgs in
|
||
#print PrivCtor
|
||
|
||
/-! Extended class -/
|
||
/--
|
||
info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
|
||
number of parameters: 1
|
||
parents:
|
||
Alternative.toApplicative : Applicative f
|
||
fields:
|
||
Functor.map : {α β : Type u} → (α → β) → f α → f β :=
|
||
fun {α β} x y => pure x <*> y
|
||
Functor.mapConst : {α β : Type u} → α → f β → f α :=
|
||
fun {α β} => Functor.map ∘ Function.const β
|
||
Pure.pure : {α : Type u} → α → f α
|
||
Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
|
||
SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α :=
|
||
fun {α β} a b => Function.const β <$> a <*> b ()
|
||
SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β :=
|
||
fun {α β} a b => Function.const α id <$> a <*> b ()
|
||
Alternative.failure : {α : Type u} → f α
|
||
Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α
|
||
constructor:
|
||
Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α)
|
||
(orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f
|
||
field notation resolution order:
|
||
Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
|
||
-/
|
||
#guard_msgs in
|
||
#print Alternative
|
||
|
||
/-! Multiply extended class -/
|
||
/--
|
||
info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
|
||
number of parameters: 1
|
||
parents:
|
||
Applicative.toFunctor : Functor f
|
||
Applicative.toPure : Pure f
|
||
Applicative.toSeq : Seq f
|
||
Applicative.toSeqLeft : SeqLeft f
|
||
Applicative.toSeqRight : SeqRight f
|
||
fields:
|
||
Functor.map : {α β : Type u} → (α → β) → f α → f β :=
|
||
fun {α β} x y => pure x <*> y
|
||
Functor.mapConst : {α β : Type u} → α → f β → f α :=
|
||
fun {α β} => Functor.map ∘ Function.const β
|
||
Pure.pure : {α : Type u} → α → f α
|
||
Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
|
||
SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α :=
|
||
fun {α β} a b => Function.const β <$> a <*> b ()
|
||
SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β :=
|
||
fun {α β} a b => Function.const α id <$> a <*> b ()
|
||
constructor:
|
||
Applicative.mk.{u, v} {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f]
|
||
[toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f
|
||
field notation resolution order:
|
||
Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
|
||
-/
|
||
#guard_msgs in
|
||
#print Applicative
|
||
|
||
/-! Structure with unused parameter -/
|
||
|
||
structure Weird (α β : Type _) where
|
||
a : α
|
||
|
||
/--
|
||
info: structure Weird.{u_1, u_2} (α : Type u_1) (β : Type u_2) : Type u_1
|
||
number of parameters: 2
|
||
fields:
|
||
Weird.a : α
|
||
constructor:
|
||
Weird.mk.{u_1, u_2} {α : Type u_1} {β : Type u_2} (a : α) : Weird α β
|
||
-/
|
||
#guard_msgs in
|
||
#print Weird
|
||
|
||
/-! Structure-like inductive -/
|
||
|
||
inductive Fake (α : Type _) where
|
||
| mk : (x : α) → Fake α
|
||
|
||
/--
|
||
info: inductive Fake.{u_1} : Type u_1 → Type u_1
|
||
number of parameters: 1
|
||
constructors:
|
||
Fake.mk : {α : Type u_1} → α → Fake α
|
||
-/
|
||
#guard_msgs in
|
||
#print Fake
|