From a50a2d00748f6a2607552a887445e7c188c0dc61 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 19 Apr 2024 14:51:15 +0200 Subject: [PATCH] rebased merge --- src/Lean/CoreM.lean | 2 +- src/Lean/Elab/MutualDef.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Language/Basic.lean | 14 ----------- src/Lean/Language/Lean.lean | 39 +++++++++++++++++++---------- src/Lean/Meta/Basic.lean | 2 +- 7 files changed, 31 insertions(+), 32 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 97aa61929d03..ba8b73258558 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -179,7 +179,7 @@ def restore (b : State) : CoreM Unit := /-- Restores full state including sources for unique identifiers. Only intended for incremental reuse -betweeen elaboration runs, not for backtracking within a single run. +between elaboration runs, not for backtracking within a single run. -/ def restoreFull (b : State) : CoreM Unit := set b diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 29aea800508f..85e00c5c4009 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -941,7 +941,7 @@ where for header in headers, view in views do if let some classNamesStx := view.deriving? then for classNameStx in classNamesStx do - let className ← resolveGlobalConstNoOverload classNameStx + let className ← realizeGlobalConstNoOverload classNameStx withRef classNameStx do unless (← processDefDeriving className header.declName) do throwError "failed to synthesize instance '{className}' for '{header.declName}'" diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 47e549ae53cb..1b1c9eebf420 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -59,7 +59,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic withCaseRef (getAltDArrow alt) rhs do if isHoleRHS rhs then addInfo - mvarId.withContext <| withRef rhs do + mvarId.withContext <| withTacticInfoContext rhs do let mvarDecl ← mvarId.getDecl let val ← elabTermEnsuringType rhs mvarDecl.type mvarId.assign val diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 7636092c85cf..3d41a282e0d2 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -307,7 +307,7 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab /-- Restores full state including sources for unique identifiers. Only intended for incremental reuse -betweeen elaboration runs, not for backtracking within a single run. +between elaboration runs, not for backtracking within a single run. -/ def SavedState.restoreFull (s : SavedState) : TermElabM Unit := do s.meta.restoreFull diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index ec9be01cdfce..2bafab978cdd 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -17,11 +17,6 @@ set_option linter.missingDocs true namespace Lean.Language -/-- Unique diagnostics ID type of `Snapshot.Diagnostics.id?`. -/ -structure Snapshot.Diagnostics.ID where - private id : Nat -deriving Nonempty, BEq, Ord - /-- `MessageLog` with interactive diagnostics. -/ structure Snapshot.Diagnostics where /-- Non-interactive message log. -/ @@ -36,15 +31,6 @@ structure Snapshot.Diagnostics where interactiveDiagsRef? : Option (IO.Ref (Option Dynamic)) deriving Inhabited -/-- Next ID to be used for `Snapshot.Diagnostics.id?`. -/ --- As the `Nat` value is not observable outside of this module, using a global ref should be --- justified and simplifies reporting diagnostics from inside the elaborator -private builtin_initialize nextDiagsIdRef : IO.Ref Nat ← IO.mkRef 0 - -/-- Returns a new, unique diagnostics ID. -/ -def Snapshot.Diagnostics.ID.new : BaseIO ID := - nextDiagsIdRef.modifyGet fun id => (⟨id⟩, id + 1) - /-- The empty set of diagnostics. -/ def Snapshot.Diagnostics.empty : Snapshot.Diagnostics where msgLog := .empty diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 2263eb57d726..b938534e5fc5 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -169,9 +169,9 @@ register_builtin_option showPartialSyntaxErrors : Bool := { /-- Snapshot after elaboration of the entire command. -/ structure CommandFinishedSnapshot extends Language.Snapshot where /-- Resulting elaboration state. -/ - cmdState : State + cmdState : Command.State deriving Nonempty -instance : Language.ToSnapshotTree CommandFinishedSnapshot where +instance : ToSnapshotTree CommandFinishedSnapshot where toSnapshotTree s := ⟨s.toSnapshot, #[]⟩ /-- State after a command has been parsed. -/ @@ -187,6 +187,8 @@ structure CommandParsedSnapshotData extends Snapshot where elabSnap : SnapshotTask DynamicSnapshot /-- State after processing is finished. -/ finishedSnap : SnapshotTask CommandFinishedSnapshot + /-- Cache for `save`; to be replaced with incrementality. -/ + tacticCache : IO.Ref Tactic.Cache deriving Nonempty /-- State after a command has been parsed. -/ @@ -213,9 +215,9 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where /-- Cancels all significant computations from this snapshot onwards. -/ partial def CommandParsedSnapshot.cancel (snap : CommandParsedSnapshot) : BaseIO Unit := do - -- This is the only relevant computation right now - -- TODO: cancel additional elaboration tasks if we add them without switching to implicit - -- cancellation + -- This is the only relevant computation right now, everything else is promises + -- TODO: cancel additional elaboration tasks (which will be tricky with `DynamicSnapshot`) if we + -- add them without switching to implicit cancellation snap.data.finishedSnap.cancel if let some next := snap.next? then -- recurse on next command (which may have been spawned just before we cancelled above) @@ -449,6 +451,7 @@ where diagnostics := .empty, stx := .missing, parserState elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf } finishedSnap := .pure { diagnostics := .empty, cmdState } + tacticCache := (← IO.mkRef {}) } let unchanged old : BaseIO CommandParsedSnapshot := @@ -485,11 +488,14 @@ where -- on first change, make sure to cancel all further old tasks old.cancel - -- definitely assigned in `doElab` task - let headers ← IO.Promise.new + -- definitely resolved in `doElab` task + let elabPromise ← IO.Promise.new + let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {}) let finishedSnap ← doElab stx cmdState msgLog.hasErrors beginPos - { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := headers } ctx + { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise } + tacticCache + ctx let next? ← if Parser.isTerminalCommand stx then pure none -- for now, wait on "command finished" snapshot before parsing next command @@ -499,20 +505,28 @@ where diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) stx parserState - elabSnap := { range? := none, task := headers.result } + elabSnap := { range? := finishedSnap.range?, task := elabPromise.result } finishedSnap + tacticCache } doElab (stx : Syntax) (cmdState : Command.State) (hasParseError : Bool) (beginPos : String.Pos) - (snap : SnapshotBundle DynamicSnapshot) : + (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) : LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do let ctx ← read SnapshotTask.ofIO (stx.getRange?.getD ⟨beginPos, beginPos⟩) do let scope := cmdState.scopes.head! let cmdStateRef ← IO.mkRef { cmdState with messages := .empty } + /- + The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` + has exclusive access to the cache, we create a fresh reference here. Before this change, the + following `tacticCache.modify` would reset the tactic post cache while another snapshot was + still using it. + -/ + let tacticCacheNew ← IO.mkRef (← tacticCache.get) let cmdCtx : Elab.Command.Context := { ctx with cmdPos := beginPos - tacticCache? := none + tacticCache? := some tacticCacheNew snap? := some snap } let (output, _) ← @@ -543,8 +557,7 @@ where data := output } let cmdState := { cmdState with messages } - -- only has an effect if actual `resolve` was skipped from fatal exception (caught by - -- `catchExceptions` above) or it not being a mutual def + -- definitely resolve eventually snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf } return { diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index ac46534b22c3..0882164276b5 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -373,7 +373,7 @@ def SavedState.restore (b : SavedState) : MetaM Unit := do /-- Restores full state including sources for unique identifiers. Only intended for incremental reuse -betweeen elaboration runs, not for backtracking within a single run. +between elaboration runs, not for backtracking within a single run. -/ def SavedState.restoreFull (b : SavedState) : MetaM Unit := do Core.restoreFull b.core