From 9d47377bdadef1fad53279358078683c8403adde Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 5 Jun 2024 16:10:38 +0200 Subject: [PATCH] feat: incrementality for careful command macros such as `set_option in theorem`, `theorem foo.bar`, `lemma` (#4364) See Note [Incremental Macros] for the caveat on correct `withRef` use --- src/Lean/Elab/BuiltinCommand.lean | 4 +- src/Lean/Elab/Command.lean | 70 ++++++++++++++++++- src/Lean/Elab/Declaration.lean | 64 ++++++++++------- src/Lean/Elab/Tactic/Basic.lean | 22 ++---- src/Lean/Language/Basic.lean | 4 +- src/Lean/Language/Lean.lean | 20 ++++++ tests/lean/interactive/incrementalMutual.lean | 26 +++++++ .../incrementalMutual.lean.expected.out | 10 +++ tests/lean/shadow.lean.expected.out | 2 +- 9 files changed, 173 insertions(+), 49 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 404ecab9bf..fcf486aefa 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -461,7 +461,9 @@ def elabRunMeta : CommandElab := fun stx => modifyScope fun scope => { scope with opts := options } @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro - | `($cmd₁ in $cmd₂) => `(section $cmd₁:command $cmd₂ end) + | `($cmd₁ in%$tk $cmd₂) => + -- Limit ref variability for incrementality; see Note [Incremental Macros] + withRef tk `(section $cmd₁:command $cmd₂ end) | _ => Macro.throwUnsupported @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 9057c98207..fb0f5b8151 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -338,6 +338,26 @@ instance : MonadRecDepth CommandElabM where builtin_initialize registerTraceClass `Elab.command +open Language in +/-- Snapshot after macro expansion of a command. -/ +structure MacroExpandedSnapshot extends Snapshot where + /-- The declaration name of the macro. -/ + macroDecl : Name + /-- The expanded syntax tree. -/ + newStx : Syntax + /-- `State.nextMacroScope` after expansion. -/ + newNextMacroScope : Nat + /-- Whether any traces were present after expansion. -/ + hasTraces : Bool + /-- + Follow-up elaboration snapshots, one per command if `newStx` is a sequence of commands. + -/ + next : Array (SnapshotTask DynamicSnapshot) +deriving TypeName +open Language in +instance : ToSnapshotTree MacroExpandedSnapshot where + toSnapshotTree s := ⟨s.toSnapshot, s.next.map (·.map (sync := true) toSnapshotTree)⟩ + partial def elabCommand (stx : Syntax) : CommandElabM Unit := do withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do match stx with @@ -345,8 +365,8 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do if k == nullKind then -- list of commands => elaborate in order -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones - -- TODO: support incrementality at least for some cases such as expansions of - -- `set_option in` or `def a.b` + -- Incrementality is currently limited to the common case where the sequence is the direct + -- output of a macro, see below. withoutCommandIncrementality true do args.forM elabCommand else withTraceNode `Elab.command (fun _ => return stx) (tag := @@ -358,7 +378,51 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do withInfoTreeContext (mkInfoTree := mkInfoTree decl stx) do let stxNew ← liftMacroM <| liftExcept stxNew? withMacroExpansion stx stxNew do - elabCommand stxNew + -- Support incrementality; see also Note [Incremental Macros] + if let some snap := (←read).snap? then + -- Unpack nested commands; see `MacroExpandedSnapshot.next` + let cmds := if stxNew.isOfKind nullKind then stxNew.getArgs else #[stxNew] + let nextMacroScope := (← get).nextMacroScope + let hasTraces := (← getTraceState).traces.size > 0 + let oldSnap? := do + let oldSnap ← snap.old? + let oldSnap ← oldSnap.val.get.toTyped? MacroExpandedSnapshot + guard <| oldSnap.macroDecl == decl && oldSnap.newNextMacroScope == nextMacroScope + -- check absence of traces; see Note [Incremental Macros] + guard <| !oldSnap.hasTraces && !hasTraces + return oldSnap + let oldCmds? := oldSnap?.map fun old => + if old.newStx.isOfKind nullKind then old.newStx.getArgs else #[old.newStx] + Language.withAlwaysResolvedPromises cmds.size fun promises => do + snap.new.resolve <| .ofTyped { + diagnostics := .empty + macroDecl := decl + newStx := stxNew + newNextMacroScope := nextMacroScope + hasTraces + next := promises.zipWith cmds fun promise arg => + { range? := arg.getRange?, task := promise.result } + : MacroExpandedSnapshot + } + -- After the first command whose syntax tree changed, we must disable + -- incremental reuse + let mut reusedCmds := true + let opts ← getOptions + -- For each command, associate it with new promise and old snapshot, if any, and + -- elaborate recursively + for cmd in cmds, promise in promises, i in [0:cmds.size] do + let oldCmd? := oldCmds?.bind (·[i]?) + withReader ({ · with snap? := some { + new := promise + old? := do + guard reusedCmds + let old ← oldSnap? + return { stx := (← oldCmd?), val := (← old.next[i]?) } + } }) do + elabCommand cmd + reusedCmds := reusedCmds && oldCmd?.any (·.structRangeEqWithTraceReuse opts cmd) + else + elabCommand stxNew | _ => match commandElabAttribute.getEntries s.env k with | [] => diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index c42939c99f..4282d62e56 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -188,34 +188,42 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni let v ← classInductiveSyntaxToView modifiers stx elabInductiveViews #[v] +/-- +Macro that expands a declaration with a complex name into an explicit `namespace` block. +Implementing this step as a macro means that reuse checking is handled by `elabCommand`. + -/ +@[builtin_macro Lean.Parser.Command.declaration] +def expandNamespacedDeclaration : Macro := fun stx => do + match (← expandDeclNamespace? stx) with + | some (ns, newStx) => do + -- Limit ref variability for incrementality; see Note [Incremental Macros] + let declTk := stx[1][0] + let ns := mkIdentFrom declTk ns + withRef declTk `(namespace $ns $(⟨newStx⟩) end $ns) + | none => Macro.throwUnsupported + @[builtin_command_elab declaration, builtin_incremental] def elabDeclaration : CommandElab := fun stx => do - match (← liftMacroM <| expandDeclNamespace? stx) with - | some (ns, newStx) => do - let ns := mkIdentFrom stx ns - let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns) - withMacroExpansion stx newStx <| elabCommand newStx - | none => do - let decl := stx[1] - let declKind := decl.getKind - if isDefLike decl then - -- only case implementing incrementality currently - elabMutualDef #[stx] - else withoutCommandIncrementality true do - if declKind == ``Lean.Parser.Command.«axiom» then - let modifiers ← elabModifiers stx[0] - elabAxiom modifiers decl - else if declKind == ``Lean.Parser.Command.«inductive» then - let modifiers ← elabModifiers stx[0] - elabInductive modifiers decl - else if declKind == ``Lean.Parser.Command.classInductive then - let modifiers ← elabModifiers stx[0] - elabClassInductive modifiers decl - else if declKind == ``Lean.Parser.Command.«structure» then - let modifiers ← elabModifiers stx[0] - elabStructure modifiers decl - else - throwError "unexpected declaration" + let decl := stx[1] + let declKind := decl.getKind + if isDefLike decl then + -- only case implementing incrementality currently + elabMutualDef #[stx] + else withoutCommandIncrementality true do + if declKind == ``Lean.Parser.Command.«axiom» then + let modifiers ← elabModifiers stx[0] + elabAxiom modifiers decl + else if declKind == ``Lean.Parser.Command.«inductive» then + let modifiers ← elabModifiers stx[0] + elabInductive modifiers decl + else if declKind == ``Lean.Parser.Command.classInductive then + let modifiers ← elabModifiers stx[0] + elabClassInductive modifiers decl + else if declKind == ``Lean.Parser.Command.«structure» then + let modifiers ← elabModifiers stx[0] + elabStructure modifiers decl + else + throwError "unexpected declaration" /-- Return true if all elements of the mutual-block are inductive declarations. -/ private def isMutualInductive (stx : Syntax) : Bool := @@ -306,6 +314,10 @@ def expandMutualElement : Macro := fun stx => do let mut elemsNew := #[] let mut modified := false for elem in stx[1].getArgs do + -- Don't trigger the `expandNamespacedDecl` macro, the namespace is handled by the mutual def + -- elaborator directly instead + if elem.isOfKind ``Parser.Command.declaration then + continue match (← expandMacro? elem) with | some elemNew => elemsNew := elemsNew.push elemNew; modified := true | none => elemsNew := elemsNew.push elem diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 1df7d4c4c7..ea59229e36 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -201,32 +201,20 @@ where withReader ({ · with elaborator := m.declName }) do withTacticInfoContext stx do let stx' ← adaptMacro m.value stx - /- - If we have a macro, we can always support incrementality: we can assume that in the - old and new version, behavior is determined solely by the unfolding and can rely on - its incrementality guarantees. We only have to update `tacSnap?` to point to the old - unfolding. - - Caveat 1: Apart from the unfolding itself, macro execution does have two additional - outputs: modifications to the next macro scope and to the traces. We check that the - next macro scope is unchanged below but choose to ignore the traces as they should not - have an effect on functional correctness of reuse and usually should not depend on the - nested tactics that we are trying to make incremental. - - Caveat 2: As the default `ref` of a macro spans its entire syntax tree and is applied - to any token created from a quotation, the ref usually has to be changed to a less - variable source to achieve incrementality. See the implementation of tactic `have` for - an example. - -/ + -- Support incrementality; see also Note [Incremental Macros] if evalFns.isEmpty && ms.isEmpty then -- Only try incrementality in one branch if let some snap := (← readThe Term.Context).tacSnap? then let nextMacroScope := (← getThe Core.State).nextMacroScope + let traceState ← getTraceState let old? := do let old ← snap.old? -- If the kind is equal, we can assume the old version was a macro as well guard <| old.stx.isOfKind stx.getKind let state ← old.val.get.data.finished.get.state? guard <| state.term.meta.core.nextMacroScope == nextMacroScope + -- check absence of traces; see Note [Incremental Macros] + guard <| state.term.meta.core.traceState.traces.size == 0 + guard <| traceState.traces.size == 0 return old.val.get Language.withAlwaysResolvedPromise fun promise => do -- Store new unfolding in the snapshot tree diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 514b103de2..fd4d898280 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -228,7 +228,6 @@ structure DynamicSnapshot where val : Dynamic /-- Snapshot tree retrieved from `val` before erasure. -/ tree : SnapshotTree -deriving Nonempty instance : ToSnapshotTree DynamicSnapshot where toSnapshotTree s := s.tree @@ -243,6 +242,9 @@ def DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : DynamicSnapshot) Option α := snap.val.get? α +instance : Inhabited DynamicSnapshot where + default := .ofTyped { diagnostics := .empty : SnapshotLeaf } + /-- Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree preorder. -/ diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 6de1a3c01a..355d45545b 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -140,6 +140,26 @@ times, here is a summary of what it has to do to implement incrementality: a wildcard pattern -/ +/- +# Note [Incremental Macros] + +If we have a macro, we can cheaply support incrementality: as a macro is a pure function, if all +outputs apart from the expanded syntax tree itself are identical in two document versions, we can +simply delegate reuse detection to the subsequently called elaborator. All we have to do is to +forward the old unfolding, if any, to it in the appropriate context field and store the new +unfolding for that purpose in a new snapshot node whose child will be filled by the called +elaborator. This is currently implemented for command and tactic macros. + +Caveat 1: Traces are an additional output of macro expansion but because they are hard to compare +and should not be active in standard use cases, we disable incrementality if either version produced +traces. + +Caveat 2: As the default `ref` of a macro spans its entire syntax tree and is applied to any token +created from a quotation, the ref usually has to be changed to a less variable source using +`withRef` to achieve effective incrementality. See `Elab.Command.expandNamespacedDeclaration` for a +simple example and the implementation of tactic `have` for a complex example. +-/ + set_option linter.missingDocs true namespace Lean.Language.Lean diff --git a/tests/lean/interactive/incrementalMutual.lean b/tests/lean/interactive/incrementalMutual.lean index eaddd9b9b7..b2a45435ef 100644 --- a/tests/lean/interactive/incrementalMutual.lean +++ b/tests/lean/interactive/incrementalMutual.lean @@ -38,3 +38,29 @@ def map' {α β} (f : α → β) : List α → List β := --^ collectDiagnostics --^ insert: "\n" --^ collectDiagnostics + +/-! Reuse should work through the namespaced decl macro. -/ +-- RESET +def ns.n : (by dbg_trace "ns 0"; exact Nat) := by + dbg_trace "ns 1" + --^ sync + --^ insert: ".5" + exact 0 + +/-! Changing the namespace should prohibit def reuse. -/ +-- RESET +def nt.n : (by dbg_trace "nt 0"; exact Nat) := by + --^ sync + --^ change: "t" "u" + dbg_trace "nt 1" + exact 0 + +/-! Reuse should support `in`. -/ +-- RESET +set_option trace.Elab.definition.body true in +def so : Nat := by + dbg_trace "so 0" + dbg_trace "so 1" + --^ sync + --^ insert: ".5" + exact 0 diff --git a/tests/lean/interactive/incrementalMutual.lean.expected.out b/tests/lean/interactive/incrementalMutual.lean.expected.out index c3f9a4297c..195381e151 100644 --- a/tests/lean/interactive/incrementalMutual.lean.expected.out +++ b/tests/lean/interactive/incrementalMutual.lean.expected.out @@ -19,3 +19,13 @@ h 0 1 h 1 1 {"version": 1, "uri": "file:///incrementalMutual.lean", "diagnostics": []} {"version": 2, "uri": "file:///incrementalMutual.lean", "diagnostics": []} +ns 0 +ns 1 +ns 1.5 +nt 0 +nt 1 +nt 0 +nt 1 +so 0 +so 1 +so 1.5 diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index b75cd4a6e3..8d1685226a 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -19,7 +19,7 @@ inst✝ inst : α shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder context: α : Type u_1 -inst.71 : Inhabited α +inst.75 : Inhabited α inst inst : α ⊢ {β δ : Type} → α → β → δ → α × β × δ shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder