From 811bad16e1815b663bdb4ecdc535a0f65d410ce0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 23 May 2024 19:57:42 +0200 Subject: [PATCH] fix: ensure incremental commands and tactics are reached only on supported paths (#4259) Without this, it would not easy but perhaps be feasible to break incrementality when editing command prefixes such as `set_option ... in theorem` or also `theorem namesp.name ...` (which is a macro), especially if at some later point we support incrementality in input shifted by an edit. Explicit, sound support for these common cases will be brought back soon. --- src/Lean/Elab/Command.lean | 25 +++++++++- src/Lean/Elab/Declaration.lean | 48 ++++++++++--------- src/Lean/Elab/Tactic/Basic.lean | 7 ++- src/Lean/Elab/Term.lean | 4 +- .../lean/interactive/incrementalCommand.lean | 40 ++++++++++++++++ .../incrementalCommand.lean.expected.out | 4 ++ tests/lean/interactive/run.lean | 27 +++++++---- 7 files changed, 118 insertions(+), 37 deletions(-) create mode 100644 tests/lean/interactive/incrementalCommand.lean create mode 100644 tests/lean/interactive/incrementalCommand.lean.expected.out diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 7051ae046f..9057c98207 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -296,11 +296,29 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArr } return InfoTree.context ctx tree +/-- +Disables incremental command reuse *and* reporting for `act` if `cond` is true by setting +`Context.snap?` to `none`. +-/ +def withoutCommandIncrementality (cond : Bool) (act : CommandElabM α) : CommandElabM α := do + let opts ← getOptions + withReader (fun ctx => { ctx with snap? := ctx.snap?.filter fun snap => Id.run do + if let some old := snap.old? then + if cond && opts.getBool `trace.Elab.reuse then + dbg_trace "reuse stopped: guard failed at {old.stx}" + return !cond + }) act + private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit | [] => withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <| throwError "unexpected syntax{indentD stx}" | (elabFn::elabFns) => catchInternalId unsupportedSyntaxExceptionId - (withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) <| elabFn.value stx) + (do + -- prevent unsupported commands from accidentally accessing `Context.snap?` (e.g. by nested + -- supported commands) + withoutCommandIncrementality (!(← isIncrementalElab elabFn.declName)) do + withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) do + elabFn.value stx) (fun _ => do set s; elabCommandUsing s stx elabFns) /-- Elaborate `x` with `stx` on the macro stack -/ @@ -327,7 +345,10 @@ 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 - args.forM elabCommand + -- TODO: support incrementality at least for some cases such as expansions of + -- `set_option in` or `def a.b` + withoutCommandIncrementality true do + args.forM elabCommand else withTraceNode `Elab.command (fun _ => return stx) (tag := -- special case: show actual declaration kind for `declaration` commands (if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 54d88ef17c..c42939c99f 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -188,7 +188,7 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni let v ← classInductiveSyntaxToView modifiers stx elabInductiveViews #[v] -@[builtin_command_elab declaration] +@[builtin_command_elab declaration, builtin_incremental] def elabDeclaration : CommandElab := fun stx => do match (← liftMacroM <| expandDeclNamespace? stx) with | some (ns, newStx) => do @@ -198,22 +198,24 @@ def elabDeclaration : CommandElab := fun stx => do | none => do let decl := stx[1] let declKind := decl.getKind - 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 if isDefLike decl then + if isDefLike decl then + -- only case implementing incrementality currently elabMutualDef #[stx] - else - throwError "unexpected declaration" + 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 := @@ -322,14 +324,16 @@ def expandMutualPreamble : Macro := fun stx => let endCmd ← `(end) return mkNullNode (#[secCmd] ++ preamble ++ #[newMutual] ++ #[endCmd]) -@[builtin_command_elab «mutual»] +@[builtin_command_elab «mutual», builtin_incremental] def elabMutual : CommandElab := fun stx => do - if isMutualInductive stx then - elabMutualInductive stx[1].getArgs - else if isMutualDef stx then + if isMutualDef stx then + -- only case implementing incrementality currently elabMutualDef stx[1].getArgs - else - throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs" + else withoutCommandIncrementality true do + if isMutualInductive stx then + elabMutualInductive stx[1].getArgs + else + throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs" /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/ @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index bc35cf279e..499f5b9af2 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -152,7 +152,10 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do | .node _ k _ => if k == nullKind then -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` - stx.getArgs.forM evalTactic + -- We could support incrementality here by allocating `n` new snapshot bundles but the + -- practical value is not clear + Term.withoutTacticIncrementality true do + stx.getArgs.forM evalTactic else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind let macros := macroAttribute.getEntries (← getEnv) stx.getKind @@ -207,7 +210,7 @@ where | evalFn::evalFns => do try -- prevent unsupported tactics from accidentally accessing `Term.Context.tacSnap?` - Term.withoutTacticReuse (!(← isIncrementalElab evalFn.declName)) do + Term.withoutTacticIncrementality (!(← isIncrementalElab evalFn.declName)) do withReader ({ · with elaborator := evalFn.declName }) do withTacticInfoContext stx do evalFn.value stx diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 8a9a1acde9..235485b99c 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1905,8 +1905,8 @@ builtin_initialize } /-- Checks whether a declaration is annotated with `[builtin_incremental]` or `[incremental]`. -/ -def isIncrementalElab (decl : Name) : CoreM Bool := - (return (← builtinIncrementalElabs.get).contains decl) <||> +def isIncrementalElab [Monad m] [MonadEnv m] [MonadLiftT IO m] (decl : Name) : m Bool := + (return (← builtinIncrementalElabs.get (m := IO)).contains decl) <||> (return incrementalAttr.hasTag (← getEnv) decl) export Term (TermElabM) diff --git a/tests/lean/interactive/incrementalCommand.lean b/tests/lean/interactive/incrementalCommand.lean new file mode 100644 index 0000000000..6a2dfcc311 --- /dev/null +++ b/tests/lean/interactive/incrementalCommand.lean @@ -0,0 +1,40 @@ +/-! +Comments after a command may become part of the next command on edits. +(Note that this module doc is a command on its own) +-/ + +--v sync +--v insert: "-" +/- +info: "3.14" +-/ +#guard_msgs in +#eval "3.14" +--^ collectDiagnostics +-- (should be empty if edit was handled correctly) + +/-! Same, after header -/ +-- RESET +import Init + +--v sync +--v insert: "-" +/- +info: "3.14" +-/ +#guard_msgs in +#eval "3.14" +--^ collectDiagnostics +-- (should be empty if edit was handled correctly) + +/-! Commands not marked as `[incremental]` should not allow accidental reuse in unknown contexts. -/ +-- RESET +import Lean + +open Lean Elab Command in +elab "wrap" num c:command : command => do + elabCommand c + + --v change: "1" "2" +wrap 1 def wrapped := by + dbg_trace "w" diff --git a/tests/lean/interactive/incrementalCommand.lean.expected.out b/tests/lean/interactive/incrementalCommand.lean.expected.out new file mode 100644 index 0000000000..1f6ed9d799 --- /dev/null +++ b/tests/lean/interactive/incrementalCommand.lean.expected.out @@ -0,0 +1,4 @@ +{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []} +{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []} +w +w diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean index 0d4db7a8a6..873da639c7 100644 --- a/tests/lean/interactive/run.lean +++ b/tests/lean/interactive/run.lean @@ -116,9 +116,22 @@ partial def main (args : List String) : IO Unit := do -- We do NOT check currently that the text at this position is indeed that string. | "delete" -- `insert: "foo"` inserts the given string at the given position. - | "insert" => - let some text := Syntax.decodeStrLit params - | throw <| IO.userError s!"failed to parse {params}" + | "insert" + -- `change: "foo" "bar"` is like `delete: "foo"` followed by `insert: "bar"` in one atomic step. + | "change" => + let (delete, insert) ← match method with + | "delete" => pure (params, "\"\"") + | "insert" => pure ("\"\"", params) + | "change" => + -- TODO: allow spaces in strings + let [delete, insert] := params.splitOn " " + | throw <| IO.userError s!"expected two arguments in {params}" + pure (delete, insert) + | _ => unreachable! + let some delete := Syntax.decodeStrLit delete + | throw <| IO.userError s!"failed to parse {delete}" + let some insert := Syntax.decodeStrLit insert + | throw <| IO.userError s!"failed to parse {insert}" let params : DidChangeTextDocumentParams := { textDocument := { uri := uri @@ -126,12 +139,8 @@ partial def main (args : List String) : IO Unit := do } contentChanges := #[TextDocumentContentChangeEvent.rangeChange { start := pos - «end» := match method with - | "delete" => { pos with character := pos.character + text.length } - | _ => pos - } (match method with - | "delete" => "" - | _ => text)] + «end» := { pos with character := pos.character + delete.length } + } insert] } let params := toJson params Ipc.writeNotification ⟨"textDocument/didChange", params⟩