From 7580126a2adc134a9704edb724cf2c49d58f952b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 26 Apr 2024 14:09:01 +0200 Subject: [PATCH] Simplify API, enable interactive diagnostics Also try to support incremental messages --- lean-toolchain | 2 +- src/verso/Verso/Doc/Concrete.lean | 2 +- src/verso/Verso/Doc/Elab/Incremental.lean | 26 +++++++++++------------ 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/lean-toolchain b/lean-toolchain index 2d7b40a..3755ac0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-04-17 +leanprover/lean4:nightly-2024-04-25 diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index c53e7de..ce4e062 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -222,7 +222,7 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eo let titleString := inlinesToString (← getEnv) titleParts let initState : PartElabM.State := .init titleName let (indicateFinished, ⟨st, st', _⟩) ← - incrementallyElabCommand text blocks + incrementallyElabCommand blocks (initAct := do setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)) (endAct := closePartsUntil 0 endPos) (handleStep := partCommand) diff --git a/src/verso/Verso/Doc/Elab/Incremental.lean b/src/verso/Verso/Doc/Elab/Incremental.lean index 17404de..06d5013 100644 --- a/src/verso/Verso/Doc/Elab/Incremental.lean +++ b/src/verso/Verso/Doc/Elab/Incremental.lean @@ -148,10 +148,6 @@ The parameters are: will frequently be a transformed `TermElabM`. If so, its `MonadStateOf σ` instance must capture `TermElabM`'s state, e.g. via `saveState` and `TermState.restoreFull`. - * `cmd` is the complete syntax of the command being elaborated. This is used only for displaying - interactive feedback to the user, and it should be a piece of syntax whose range encompasses all - the individual steps to be elaborated. - * `steps` is the individual steps to incrementally elaborate. These should all be contained within `cmd`. They are saved in incremental snapshots and compared (with `Syntax.structRangeEq`) to determine whether the snapshot should be re-used or invalidated. @@ -175,25 +171,27 @@ def incrementallyElabCommand [IncrementalSnapshot snapshot σ] [TypeName snapshot] [Nonempty snapshot] [Nonempty σ] - [Monad m] [MonadLiftT BaseIO m] [MonadExcept Exception m] [MonadLog m] [AddMessageContext m] [MonadFinally m] [MonadOptions m] + [Monad m] [MonadLiftT BaseIO m] [MonadLiftT CoreM m] [MonadExcept Exception m] [MonadLog m] [AddMessageContext m] [MonadFinally m] [MonadOptions m] [MonadStateOf σ m] - (cmd : Syntax) (steps : Array Syntax) (initAct : m Unit) (endAct : m Unit) (handleStep : Syntax → m Unit) (lift : {α : _} → m α → CommandElabM α) : CommandElabM (CommandElabM Unit × σ) := do + let cmd := mkNullNode steps if let some snap := (← read).snap? then withReader (fun ρ => {ρ with snap? := none}) do lift <| do let mut oldSnap? := snap.old?.bind (·.val.get.toTyped? (α := Internal.IncrementalSnapshot)) let mut nextPromise ← IO.Promise.new - let initData : Language.Snapshot := {diagnostics := .empty} + + let freshSnapshot : m Language.Snapshot := do + pure {diagnostics := ← Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog)} + let initData : Language.Snapshot ← freshSnapshot snap.new.resolve <| DynamicSnapshot.ofTyped <| Internal.IncrementalSnapshot.mk initData (.mk <| mkSnap (.pure (← get))) (some {range? := cmd.getRange?, task := nextPromise.result}) cmd initAct - let mut errors : MessageLog := .empty for b in steps do let mut reuseState := false if let some oldSnap := oldSnap? then @@ -206,20 +204,20 @@ def incrementallyElabCommand -- If they match, do nothing and advance the snapshot let σ := data |> getIncrState |>.get set σ - errors := next.get.toLeanSnapshot |>.diagnostics.msgLog oldSnap? := next.get reuseState := true let nextNextPromise ← IO.Promise.new let updatedState ← IO.Promise.new + nextPromise.resolve <| - .mk {diagnostics := ⟨errors, none⟩} (.mk <| mkSnap updatedState.result) + .mk (← freshSnapshot) (.mk <| mkSnap updatedState.result) (some {range? := b.getRange?, task := nextNextPromise.result}) b try if not reuseState then oldSnap? := none try handleStep b - catch e => errors := errors.add <| ← exnMessage e + catch e => logMessage <| ← exnMessage e updatedState.resolve <| ← get nextPromise := nextNextPromise @@ -227,12 +225,14 @@ def incrementallyElabCommand -- In case of a fatal exception in partCommand, we need to make sure that the promise actually -- gets resolved to avoid hanging forever. And the first resolve wins, so the second one is a -- no-op the rest of the time. - nextPromise.resolve <| .mk {diagnostics := ⟨errors, none⟩} (.mk <| mkSnap (.pure (← get))) none b + nextPromise.resolve <| .mk (← freshSnapshot) (.mk <| mkSnap (.pure (← get))) none b updatedState.resolve <| ← get -- some old state goes here endAct let finalState ← get + let allDone : CommandElabM Unit := do - nextPromise.resolve <| .mk {diagnostics := ⟨errors, none⟩} (.mk <| mkSnap (.pure finalState)) none cmd + let diags ← Snapshot.Diagnostics.ofMessageLog <| ← liftCoreM Core.getAndEmptyMessageLog + nextPromise.resolve <| .mk {diagnostics := diags} (.mk <| mkSnap (.pure finalState)) none cmd pure (allDone, finalState) else -- incrementality not available - just do the action the easy way lift <| do