inductive Lapis.Server.Progress.ProgressToken : Type

A progress token can be a string or number

• string (s : String) : ProgressToken
• number (n : Int) : ProgressToken

instance Lapis.Server.Progress.instInhabitedProgressToken : Inhabited ProgressToken

Equations

• Lapis.Server.Progress.instInhabitedProgressToken = { default := Lapis.Server.Progress.instInhabitedProgressToken.default }

def Lapis.Server.Progress.instInhabitedProgressToken.default : ProgressToken

Equations

• Lapis.Server.Progress.instInhabitedProgressToken.default = Lapis.Server.Progress.ProgressToken.string default

def Lapis.Server.Progress.instBEqProgressToken.beq : ProgressToken → ProgressToken → Bool

Equations

• Lapis.Server.Progress.instBEqProgressToken.beq (Lapis.Server.Progress.ProgressToken.string a) (Lapis.Server.Progress.ProgressToken.string b) = (a == b)
• Lapis.Server.Progress.instBEqProgressToken.beq (Lapis.Server.Progress.ProgressToken.number a) (Lapis.Server.Progress.ProgressToken.number b) = (a == b)
• Lapis.Server.Progress.instBEqProgressToken.beq x✝¹ x✝ = false

instance Lapis.Server.Progress.instBEqProgressToken : BEq ProgressToken

Equations

• Lapis.Server.Progress.instBEqProgressToken = { beq := Lapis.Server.Progress.instBEqProgressToken.beq }

instance Lapis.Server.Progress.instHashableProgressToken : Hashable ProgressToken

Equations

• Lapis.Server.Progress.instHashableProgressToken = { hash := Lapis.Server.Progress.instHashableProgressToken.hash }

def Lapis.Server.Progress.instHashableProgressToken.hash : ProgressToken → UInt64

Equations

• Lapis.Server.Progress.instHashableProgressToken.hash (Lapis.Server.Progress.ProgressToken.string a) = mixHash 0 (hash a)
• Lapis.Server.Progress.instHashableProgressToken.hash (Lapis.Server.Progress.ProgressToken.number a) = mixHash 1 (hash a)

instance Lapis.Server.Progress.instToStringProgressToken : ToString ProgressToken

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Server.Progress.instToJsonProgressToken : Lean.ToJson ProgressToken

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.Server.Progress.instFromJsonProgressToken : Lean.FromJson ProgressToken

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Progress.WorkDoneProgressBegin : Type

• title : String
• cancellable : Option Bool
• message : Option String
• percentage : Option Nat

def Lapis.Server.Progress.instInhabitedWorkDoneProgressBegin.default : WorkDoneProgressBegin

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressBegin.default = { title := default, cancellable := default, message := default, percentage := default }

instance Lapis.Server.Progress.instInhabitedWorkDoneProgressBegin : Inhabited WorkDoneProgressBegin

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressBegin = { default := Lapis.Server.Progress.instInhabitedWorkDoneProgressBegin.default }

instance Lapis.Server.Progress.instToJsonWorkDoneProgressBegin : Lean.ToJson WorkDoneProgressBegin

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Progress.WorkDoneProgressReport : Type

• cancellable : Option Bool
• message : Option String
• percentage : Option Nat

instance Lapis.Server.Progress.instInhabitedWorkDoneProgressReport : Inhabited WorkDoneProgressReport

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressReport = { default := Lapis.Server.Progress.instInhabitedWorkDoneProgressReport.default }

def Lapis.Server.Progress.instInhabitedWorkDoneProgressReport.default : WorkDoneProgressReport

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressReport.default = { cancellable := default, message := default, percentage := default }

instance Lapis.Server.Progress.instToJsonWorkDoneProgressReport : Lean.ToJson WorkDoneProgressReport

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Progress.WorkDoneProgressEnd : Type

• message : Option String

def Lapis.Server.Progress.instInhabitedWorkDoneProgressEnd.default : WorkDoneProgressEnd

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressEnd.default = { message := default }

instance Lapis.Server.Progress.instInhabitedWorkDoneProgressEnd : Inhabited WorkDoneProgressEnd

Equations

• Lapis.Server.Progress.instInhabitedWorkDoneProgressEnd = { default := Lapis.Server.Progress.instInhabitedWorkDoneProgressEnd.default }

instance Lapis.Server.Progress.instToJsonWorkDoneProgressEnd : Lean.ToJson WorkDoneProgressEnd

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Progress.ProgressState : Type

State of an active progress operation

• token : ProgressToken
• title : String
• cancellable : Bool
• cancelled : IO.Ref Bool
• started : Bool

structure Lapis.Server.Progress.ProgressManager : Type

Manages active progress tokens and their lifecycle

• activeProgress : IO.Ref (Std.HashMap String ProgressState)

  Active progress operations

• tokenCounter : Concurrent.AtomicCounter

  Counter for generating unique tokens

• outputChannel : Transport.OutputChannel

  Output channel for sending notifications

• pendingResponses : Receiver.PendingResponses

  Pending responses for create requests

def Lapis.Server.Progress.ProgressManager.new (outputChannel : Transport.OutputChannel) (pendingResponses : Receiver.PendingResponses) : IO ProgressManager

Create a new progress manager

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Progress.ProgressManager.generateToken (pm : ProgressManager) : IO ProgressToken

Generate a unique progress token

Equations

• pm.generateToken = do let n ← pm.tokenCounter.incrementAndGet pure (Lapis.Server.Progress.ProgressToken.number (Int.ofNat n))

def Lapis.Server.Progress.ProgressManager.createToken (pm : ProgressManager) (token : ProgressToken) : IO Bool

Request the client to create a progress token (for server-initiated progress)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Progress.ProgressManager.begin (pm : ProgressManager) (token : ProgressToken) (title : String) (cancellable : Bool := false) (message : Option String := none) (percentage : Option Nat := none) : IO Unit

Begin a progress operation

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Progress.ProgressManager.report (pm : ProgressManager) (token : ProgressToken) (message : Option String := none) (percentage : Option Nat := none) (cancellable : Option Bool := none) : IO Unit

Report progress update

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Progress.ProgressManager.end (pm : ProgressManager) (token : ProgressToken) (message : Option String := none) : IO Unit

End a progress operation

Equations

• One or more equations did not get rendered due to their size.

def Lapis.Server.Progress.ProgressManager.isCancelled (pm : ProgressManager) (token : ProgressToken) : IO Bool

Check if a progress operation was cancelled

Equations

• pm.isCancelled token = do let active ← ST.Ref.get pm.activeProgress match active.get? (toString token) with | some state => ST.Ref.get state.cancelled | none => pure true

def Lapis.Server.Progress.ProgressManager.markCancelled (pm : ProgressManager) (token : ProgressToken) : IO Unit

Mark a progress operation as cancelled (called when client sends cancel)

Equations

• pm.markCancelled token = do let active ← ST.Ref.get pm.activeProgress match active.get? (toString token) with | some state => ST.Ref.set state.cancelled true | x => pure PUnit.unit

def Lapis.Server.Progress.ProgressManager.withProgress {α : Type} (pm : ProgressManager) (title : String) (cancellable : Bool := false) (action : ProgressToken → IO α) : IO α

Run an action with progress reporting

Equations

• One or more equations did not get rendered due to their size.

structure Lapis.Server.Progress.ProgressHandle : Type

A handle for reporting progress within an operation

• manager : ProgressManager
• token : ProgressToken

def Lapis.Server.Progress.ProgressHandle.report (h : ProgressHandle) (message : Option String := none) (percentage : Option Nat := none) : IO Unit

Report progress

Equations

• h.report message percentage = h.manager.report h.token message percentage

def Lapis.Server.Progress.ProgressHandle.isCancelled (h : ProgressHandle) : IO Bool

Check if cancelled

Equations

• h.isCancelled = h.manager.isCancelled h.token

def Lapis.Server.Progress.ProgressHandle.checkCancelled (h : ProgressHandle) : IO Unit

Throw if cancelled

Equations

• h.checkCancelled = do let __do_lift ← h.isCancelled if __do_lift = true then throw (IO.userError "Operation cancelled") else pure PUnit.unit