max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: upstream Std.CodeAction.*

Browse source 
Remove tactic_code_action

rearrange

oops

.

add tests

import file

Update src/Lean/Elab/Tactic/GuardMsgs.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Update src/Lean/Elab/Tactic/GuardMsgs.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

fix namespace

move GuardMsgs

cleanup
This commit is contained in:
Scott Morrison 2024-02-09 23:43:11 +11:00 • committed by Leonardo de Moura
parent 72d233d181
commit 3dd10654e1
10 changed files with 743 additions and 167 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
src/Init/Notation.lean
View file

@ -532,3 +532,65 @@ except that it doesn't print an empty diagnostic.
(This is effectively a synonym for `run_elab`.)
-/
syntax (name := runMeta) "run_meta " doSeq : command
/-- Element that can be part of a `#guard_msgs` specification. -/
syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
/-- Specification for `#guard_msgs` command. -/
syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
/--
`#guard_msgs` captures the messages generated by another command and checks that they
match the contents of the docstring attached to the `#guard_msgs` command.
Basic example:
```lean
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message entirely.
By default, the command intercepts all messages, but there is a way to specify which types
of messages to consider. For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In this last example, since the message is not intercepted there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
Syntax description:
```
#guard_msgs (drop? info|warning|error|all,*)? in cmd
```
If there is no specification, `#guard_msgs` intercepts all messages.
Otherwise, if there is one, the specification is considered in left-to-right order, and the first
that applies chooses the outcome of the message:
- `info`, `warning`, `error`: intercept a message with the given severity level.
- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
are equivalent).
- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
level and then drop it. These messages are not checked.
- `drop all`: intercept a message and drop it.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
everything else.
-/
syntax (name := guardMsgsCmd)
(docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command

4
src/Lean/Data/Lsp/Utf16.lean
View file

@ -86,6 +86,10 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
text.leanPosToLspPos (text.toPosition pos)
/-- Gets the LSP range from a `String.Range`. -/
def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
end FileMap
end Lean

1
src/Lean/Elab.lean
View file

@ -47,3 +47,4 @@ import Lean.Elab.Eval
import Lean.Elab.Calc
import Lean.Elab.InheritDoc
import Lean.Elab.ParseImportsFast
import Lean.Elab.GuardMsgs

135
src/Lean/Elab/GuardMsgs.lean Normal file
View file

@ -0,0 +1,135 @@
/-
Copyright (c) 2023 Kyle Miller. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
import Lean.Server.CodeActions.Attr
/-! `#guard_msgs` command for testing commands
This module defines a command to test that another command produces the expected messages.
See the docstring on the `#guard_msgs` command.
-/
open Lean Parser.Tactic Elab Command
namespace Lean.Elab.Tactic.GuardMsgs
/-- Gives a string representation of a message without source position information.
Ensures the message ends with a '\n'. -/
private def messageToStringWithoutPos (msg : Message) : IO String := do
let mut str ← msg.data.toString
unless msg.caption == "" do
str := msg.caption ++ ":\n" ++ str
if !("\n".isPrefixOf str) then str := " " ++ str
match msg.severity with
| MessageSeverity.information => str := "info:" ++ str
| MessageSeverity.warning => str := "warning:" ++ str
| MessageSeverity.error => str := "error:" ++ str
if str.isEmpty || str.back != '\n' then
str := str ++ "\n"
return str
/-- The decision made by a specification for a message. -/
inductive SpecResult
/-- Capture the message and check it matches the docstring. -/
| check
/-- Drop the message and delete it. -/
| drop
/-- Do not capture the message. -/
| passthrough
/-- Parses a `guardMsgsSpec`.
- No specification: check everything.
- With a specification: interpret the spec, and if nothing applies pass it through. -/
def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
CommandElabM (Message → SpecResult) := do
if let some spec := spec? then
match spec with
| `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
let mut p : Message → SpecResult := fun _ => .passthrough
let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
(msg : Message) : SpecResult :=
if msg.severity == s then if drop then .drop else .check
else p msg
for elt in elts.reverse do
match elt with
| `(guardMsgsSpecElt| $[drop%$drop?]? info) => p := pushP .information drop?.isSome p
| `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
| `(guardMsgsSpecElt| $[drop%$drop?]? error) => p := pushP .error drop?.isSome p
| `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
p := fun _ => if drop?.isSome then .drop else .check
| _ => throwErrorAt elt "Invalid #guard_msgs specification element"
return p
| _ => throwErrorAt spec "Invalid #guard_msgs specification"
else
return fun _ => .check
/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
used for code action support. -/
structure GuardMsgFailure where
/-- The result of the nested command -/
res : String
deriving TypeName
@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
| `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
let specFn ← parseGuardMsgsSpec spec?
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
elabCommandTopLevel cmd
let msgs := (← get).messages
let mut toCheck : MessageLog := .empty
let mut toPassthrough : MessageLog := .empty
for msg in msgs.toList do
match specFn msg with
| .check => toCheck := toCheck.add msg
| .drop => pure ()
| .passthrough => toPassthrough := toPassthrough.add msg
let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-- We do some whitespace normalization here to allow users to break long lines.
if expected.replace "\n" " " == res.replace "\n" " " then
-- Passed. Only put toPassthrough messages back on the message log
modify fun st => { st with messages := initMsgs ++ toPassthrough }
else
-- Failed. Put all the messages back on the message log and add an error
modify fun st => { st with messages := initMsgs ++ msgs }
logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
| _ => throwUnsupportedSyntax
open CodeAction Server RequestM in
/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
@[command_code_action guardMsgsCmd]
def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
let .node _ ts := node | return #[]
let res := ts.findSome? fun
| .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
| _ => none
let some (stx, res) := res | return #[]
let doc ← readDoc
let eager := {
title := "Update #guard_msgs with tactic output"
kind? := "quickfix"
isPreferred? := true
}
pure #[{
eager
lazy? := some do
let some start := stx.getPos? true | return eager
let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
let newText := if res.isEmpty then
""
else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
s!"/-- {res} -/\n"
else
s!"/--\n{res}\n-/\n"
pure { eager with
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
newText
}
}
}]
end Lean.Elab.Tactic.GuardMsgs

6
src/Lean/Meta/Tactic/TryThis.lean
View file

@ -7,11 +7,7 @@ prelude
import Lean.Server.CodeActions
import Lean.Widget.UserWidget
import Lean.Data.Json.Elab
/-- Gets the LSP range from a `String.Range`. -/
def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
import Lean.Data.Lsp.Utf16
/-!
# "Try this" support

165
src/Lean/Server/CodeActions.lean
View file

@ -4,165 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers
-/
prelude
import Lean.Server.FileWorker.RequestHandling
import Lean.Server.InfoUtils
namespace Lean.Server
open Lsp
open RequestM
open Snapshots
/-- A code action optionally supporting a lazy code action computation that is only run when the user clicks on
the code action in the editor.
If you want to use the lazy feature, make sure that the `edit?` field on the `eager` code action result is `none`.
-/
structure LazyCodeAction where
/-- This is the initial code action that is sent to the server, to implement -/
eager : CodeAction
lazy? : Option (IO CodeAction) := none
/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
structure CodeActionResolveData where
params : CodeActionParams
/-- Name of CodeActionProvider that produced this request. -/
providerName : Name
/-- Index in the list of code action that the given provider generated. -/
providerResultIndex : Nat
deriving ToJson, FromJson
def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
let r : Except String DocumentUri := do
let some data := ca.data?
| throw s!"no data param on code action {ca.title}"
let data : CodeActionResolveData ← fromJson? data
return data.params.textDocument.uri
match r with
| Except.ok uri => uri
| Except.error e => panic! e
instance : FileSource CodeAction where
fileSource x := CodeAction.getFileSource! x
instance : Coe CodeAction LazyCodeAction where
coe c := { eager := c }
/-- A code action provider is a function for providing LSP code actions for an editor.
You can register them with the `@[code_action_provider]` attribute.
This is a low-level interface for making LSP code actions.
This interface can be used to implement the following applications:
- refactoring code: adding underscores to unused variables,
- suggesting imports
- document-level refactoring: removing unused imports, sorting imports, formatting.
- Helper suggestions for working with type holes (`_`)
- Helper suggestions for tactics.
When implementing your own `CodeActionProvider`, we assume that no long-running computations are allowed.
If you need to create a code-action with a long-running computation, you can use the `lazy?` field on `LazyCodeAction`
to perform the computation after the user has clicked on the code action in their editor.
-/
def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
deriving instance Inhabited for CodeActionProvider
private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
IO.mkRef ∅
def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
builtinCodeActionProviders.modify (·.insert decl provider)
builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
addEntryFn := fun s n => s.insert n
toArrayFn := fun es => es.toArray.qsort Name.quickLt
}
builtin_initialize
let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
name
descr := (if builtin then "(builtin) " else "") ++
"Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
applicationTime := .afterCompilation
add := fun decl stx kind => do
Attribute.Builtin.ensureNoArgs stx
unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
let env ← getEnv
if builtin then
let h := mkConst decl
declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
else
setEnv <| codeActionProviderExt.addEntry env decl
}
mkAttr true `builtin_code_action_provider
mkAttr false `code_action_provider
private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
evalConstCheck CodeActionProvider ``CodeActionProvider declName
/-- Get a `CodeActionProvider` from a declaration name. -/
@[implemented_by evalCodeActionProviderUnsafe]
private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
/-- Handles a `textDocument/codeAction` request.
This is implemented by calling all of the registered `CodeActionProvider` functions.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
let doc ← readDoc
let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := return #[])
fun snap => do
let caps ← RequestM.runCoreM snap do
let env ← getEnv
let names := codeActionProviderExt.getState env |>.toArray
let caps ← names.mapM evalCodeActionProvider
return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
caps.concatMapM fun (providerName, cap) => do
let cas ← cap params snap
cas.mapIdxM fun i lca => do
if lca.lazy?.isNone then return lca.eager
let data : CodeActionResolveData := {
params, providerName, providerResultIndex := i
}
let j : Json := toJson data
let ca := { lca.eager with data? := some j }
return ca
builtin_initialize
registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
/-- Handler for `"codeAction/resolve"`.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
-/
def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
let doc ← readDoc
let some data := param.data?
| throw (RequestError.invalidParams "Expected a data field on CodeAction.")
let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := throw <| RequestError.internalError "snapshot not found")
fun snap => do
let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
| some cap => pure cap
| none => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
let cas ← cap data.params snap
let some ca := cas[data.providerResultIndex]?
| throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
let some lazy := ca.lazy?
| throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
let r ← liftM lazy
return r
builtin_initialize
registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
end Lean.Server
import Lean.Server.CodeActions.Attr
import Lean.Server.CodeActions.Basic
import Lean.Server.CodeActions.Provider

133
src/Lean/Server/CodeActions/Attr.lean Normal file
View file

@ -0,0 +1,133 @@
/-
Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Server.CodeActions.Basic
/-!
# Initial setup for code action attributes
* Attribute `@[hole_code_action]` collects code actions which will be called
on each occurrence of a hole (`_`, `?_` or `sorry`).
* Attribute `@[tactic_code_action]` collects code actions which will be called
on each occurrence of a tactic.
* Attribute `@[command_code_action]` collects code actions which will be called
on each occurrence of a command.
-/
namespace Lean.CodeAction
open Lean Elab Server Lsp RequestM Snapshots
/-- A hole code action extension. -/
abbrev HoleCodeAction :=
CodeActionParams → Snapshot →
(ctx : ContextInfo) → (hole : TermInfo) → RequestM (Array LazyCodeAction)
/-- Read a hole code action from a declaration of the right type. -/
def mkHoleCodeAction (n : Name) : ImportM HoleCodeAction := do
let { env, opts, .. } ← read
IO.ofExcept <| unsafe env.evalConstCheck HoleCodeAction opts ``HoleCodeAction n
/-- An extension which collects all the hole code actions. -/
initialize holeCodeActionExt :
PersistentEnvExtension Name (Name × HoleCodeAction) (Array Name × Array HoleCodeAction) ←
registerPersistentEnvExtension {
mkInitial := pure (#[], #[])
addImportedFn := fun as => return (#[], ← as.foldlM (init := #[]) fun m as =>
as.foldlM (init := m) fun m a => return m.push (← mkHoleCodeAction a))
addEntryFn := fun (s₁, s₂) (n₁, n₂) => (s₁.push n₁, s₂.push n₂)
exportEntriesFn := (·.1)
}
initialize
registerBuiltinAttribute {
name := `hole_code_action
descr := "Declare a new hole code action, to appear in the code actions on ?_ and _"
applicationTime := .afterCompilation
add := fun decl stx kind => do
Attribute.Builtin.ensureNoArgs stx
unless kind == AttributeKind.global do
throwError "invalid attribute 'hole_code_action', must be global"
if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
modifyEnv (holeCodeActionExt.addEntry · (decl, ← mkHoleCodeAction decl))
}
/-- A command code action extension. -/
abbrev CommandCodeAction :=
CodeActionParams → Snapshot → (ctx : ContextInfo) → (node : InfoTree) →
RequestM (Array LazyCodeAction)
/-- Read a command code action from a declaration of the right type. -/
def mkCommandCodeAction (n : Name) : ImportM CommandCodeAction := do
let { env, opts, .. } ← read
IO.ofExcept <| unsafe env.evalConstCheck CommandCodeAction opts ``CommandCodeAction n
/-- An entry in the command code actions extension, containing the attribute arguments. -/
structure CommandCodeActionEntry where
/-- The declaration to tag -/
declName : Name
/-- The command kinds that this extension supports.
If empty it is called on all command kinds. -/
cmdKinds : Array Name
deriving Inhabited
/-- The state of the command code actions extension. -/
structure CommandCodeActions where
/-- The list of command code actions to apply on any command. -/
onAnyCmd : Array CommandCodeAction := {}
/-- The list of command code actions to apply when a particular command kind is highlighted. -/
onCmd : NameMap (Array CommandCodeAction) := {}
deriving Inhabited
/-- Insert a command code action entry into the `CommandCodeActions` structure. -/
def CommandCodeActions.insert (self : CommandCodeActions)
(tacticKinds : Array Name) (action : CommandCodeAction) : CommandCodeActions :=
if tacticKinds.isEmpty then
{ self with onAnyCmd := self.onAnyCmd.push action }
else
{ self with onCmd := tacticKinds.foldl (init := self.onCmd) fun m a =>
m.insert a ((m.findD a #[]).push action) }
/-- An extension which collects all the command code actions. -/
initialize cmdCodeActionExt :
PersistentEnvExtension CommandCodeActionEntry (CommandCodeActionEntry × CommandCodeAction)
(Array CommandCodeActionEntry × CommandCodeActions) ←
registerPersistentEnvExtension {
mkInitial := pure (#[], {})
addImportedFn := fun as => return (#[], ← as.foldlM (init := {}) fun m as =>
as.foldlM (init := m) fun m ⟨name, kinds⟩ =>
return m.insert kinds (← mkCommandCodeAction name))
addEntryFn := fun (s₁, s₂) (e, n₂) => (s₁.push e, s₂.insert e.cmdKinds n₂)
exportEntriesFn := (·.1)
}
/--
This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
* `@[command_code_action kind]`: This is a code action which applies to applications of the command
`kind` (a command syntax kind), which can replace the command or insert things before or after it.
* `@[command_code_action kind₁ kind₂]`: shorthand for
`@[command_code_action kind₁, command_code_action kind₂]`.
* `@[command_code_action]`: This is a command code action that applies to all commands.
Use sparingly.
-/
syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
initialize
registerBuiltinAttribute {
name := `command_code_action
descr := "Declare a new command code action, to appear in the code actions on commands"
applicationTime := .afterCompilation
add := fun decl stx kind => do
unless kind == AttributeKind.global do
throwError "invalid attribute 'command_code_action', must be global"
let `(attr| command_code_action $args*) := stx | return
let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
}

168
src/Lean/Server/CodeActions/Basic.lean Normal file
View file

@ -0,0 +1,168 @@
/-
Copyright (c) 2022 E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers
-/
prelude
import Lean.Server.FileWorker.RequestHandling
import Lean.Server.InfoUtils
namespace Lean.Server
open Lsp
open RequestM
open Snapshots
/-- A code action optionally supporting a lazy code action computation that is only run when the user clicks on
the code action in the editor.
If you want to use the lazy feature, make sure that the `edit?` field on the `eager` code action result is `none`.
-/
structure LazyCodeAction where
/-- This is the initial code action that is sent to the server, to implement -/
eager : CodeAction
lazy? : Option (IO CodeAction) := none
/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
structure CodeActionResolveData where
params : CodeActionParams
/-- Name of CodeActionProvider that produced this request. -/
providerName : Name
/-- Index in the list of code action that the given provider generated. -/
providerResultIndex : Nat
deriving ToJson, FromJson
def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
let r : Except String DocumentUri := do
let some data := ca.data?
| throw s!"no data param on code action {ca.title}"
let data : CodeActionResolveData ← fromJson? data
return data.params.textDocument.uri
match r with
| Except.ok uri => uri
| Except.error e => panic! e
instance : FileSource CodeAction where
fileSource x := CodeAction.getFileSource! x
instance : Coe CodeAction LazyCodeAction where
coe c := { eager := c }
/-- A code action provider is a function for providing LSP code actions for an editor.
You can register them with the `@[code_action_provider]` attribute.
This is a low-level interface for making LSP code actions.
This interface can be used to implement the following applications:
- refactoring code: adding underscores to unused variables,
- suggesting imports
- document-level refactoring: removing unused imports, sorting imports, formatting.
- Helper suggestions for working with type holes (`_`)
- Helper suggestions for tactics.
When implementing your own `CodeActionProvider`, we assume that no long-running computations are allowed.
If you need to create a code-action with a long-running computation, you can use the `lazy?` field on `LazyCodeAction`
to perform the computation after the user has clicked on the code action in their editor.
-/
def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
deriving instance Inhabited for CodeActionProvider
private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
IO.mkRef ∅
def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
builtinCodeActionProviders.modify (·.insert decl provider)
builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
addEntryFn := fun s n => s.insert n
toArrayFn := fun es => es.toArray.qsort Name.quickLt
}
builtin_initialize
let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
name
descr := (if builtin then "(builtin) " else "") ++
"Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
applicationTime := .afterCompilation
add := fun decl stx kind => do
Attribute.Builtin.ensureNoArgs stx
unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
let env ← getEnv
if builtin then
let h := mkConst decl
declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
else
setEnv <| codeActionProviderExt.addEntry env decl
}
mkAttr true `builtin_code_action_provider
mkAttr false `code_action_provider
private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
evalConstCheck CodeActionProvider ``CodeActionProvider declName
/-- Get a `CodeActionProvider` from a declaration name. -/
@[implemented_by evalCodeActionProviderUnsafe]
private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
/-- Handles a `textDocument/codeAction` request.
This is implemented by calling all of the registered `CodeActionProvider` functions.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
let doc ← readDoc
let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := return #[])
fun snap => do
let caps ← RequestM.runCoreM snap do
let env ← getEnv
let names := codeActionProviderExt.getState env |>.toArray
let caps ← names.mapM evalCodeActionProvider
return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
caps.concatMapM fun (providerName, cap) => do
let cas ← cap params snap
cas.mapIdxM fun i lca => do
if lca.lazy?.isNone then return lca.eager
let data : CodeActionResolveData := {
params, providerName, providerResultIndex := i
}
let j : Json := toJson data
let ca := { lca.eager with data? := some j }
return ca
builtin_initialize
registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
/-- Handler for `"codeAction/resolve"`.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
-/
def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
let doc ← readDoc
let some data := param.data?
| throw (RequestError.invalidParams "Expected a data field on CodeAction.")
let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := throw <| RequestError.internalError "snapshot not found")
fun snap => do
let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
| some cap => pure cap
| none => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
let cas ← cap data.params snap
let some ca := cas[data.providerResultIndex]?
| throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
let some lazy := ca.lazy?
| throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
let r ← liftM lazy
return r
builtin_initialize
registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
end Lean.Server

185
src/Lean/Server/CodeActions/Provider.lean Normal file
View file

@ -0,0 +1,185 @@
/-
Copyright (c) 2023 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Elab.BuiltinTerm
import Lean.Elab.BuiltinNotation
import Lean.Server.InfoUtils
import Lean.Server.CodeActions.Attr
/-!
# Initial setup for code actions
This declares a code action provider that calls all `@[hole_code_action]` definitions
on each occurrence of a hole (`_`, `?_` or `sorry`).
(This is in a separate file from `Std.CodeAction.Hole.Attr` so that the server does not attempt
to use this code action provider when browsing the `Std.CodeAction.Hole.Attr` file itself.)
-/
namespace Lean.CodeAction
open Lean Elab Term Server RequestM
/--
A code action which calls all `@[hole_code_action]` code actions on each hole
(`?_`, `_`, or `sorry`).
-/
@[code_action_provider] def holeCodeActionProvider : CodeActionProvider := fun params snap => do
let doc ← readDoc
let startPos := doc.meta.text.lspPosToUtf8Pos params.range.start
let endPos := doc.meta.text.lspPosToUtf8Pos params.range.end
have holes := snap.infoTree.foldInfo (init := #[]) fun ctx info result => Id.run do
let .ofTermInfo info := info | result
unless [``elabHole, ``elabSyntheticHole, ``elabSorry].contains info.elaborator do
return result
let (some head, some tail) := (info.stx.getPos? true, info.stx.getTailPos? true) | result
unless head ≤ endPos && startPos ≤ tail do return result
result.push (ctx, info)
let #[(ctx, info)] := holes | return #[]
(holeCodeActionExt.getState snap.env).2.concatMapM (· params snap ctx info)
/--
The return value of `findTactic?`.
This is the syntax for which code actions will be triggered.
-/
inductive FindTacticResult
/-- The nearest enclosing tactic is a tactic, with the given syntax stack. -/
| tactic : Syntax.Stack → FindTacticResult
/-- The cursor is between tactics, and the nearest enclosing range is a tactic sequence.
Code actions will insert tactics at index `insertIdx` into the syntax
(which is a nullNode of `tactic;*` inside a `tacticSeqBracketed` or `tacticSeq1Indented`). -/
| tacticSeq : (preferred : Bool) → (insertIdx : Nat) → Syntax.Stack → FindTacticResult
/--
Find the syntax on which to trigger tactic code actions.
This is a pure syntax pass, without regard to elaboration information.
* `preferred : String.Pos → Bool`: used to select "preferred `tacticSeq`s" based on the cursor
column, when the cursor selection would otherwise be ambiguous. For example, in:
```
· foo
· bar
baz
|
```
where the cursor is at the `|`, we select the `tacticSeq` starting with `foo`, while if the
cursor was indented to align with `baz` then we would select the `bar; baz` sequence instead.
* `range`: the cursor selection. We do not do much with range selections; if a range selection
covers more than one tactic then we abort.
* `root`: the root syntax to process
The return value is either a selected tactic, or a selected point in a tactic sequence.
-/
partial def findTactic? (preferred : String.Pos → Bool) (range : String.Range)
(root : Syntax) : Option FindTacticResult := do _ ← visit root; ← go [] root
where
/-- Returns `none` if we should not visit this syntax at all, and `some false` if we only
want to visit it in "extended" mode (where we include trailing characters). -/
visit (stx : Syntax) (prev? : Option String.Pos := none) : Option Bool := do
let left ← stx.getPos? true
guard <| prev?.getD left ≤ range.start
let .original (endPos := right) (trailing := trailing) .. := stx.getTailInfo | none
guard <| right.byteIdx + trailing.bsize ≥ range.stop.byteIdx
return left ≤ range.start && right ≥ range.stop
/-- Merges the results of two `FindTacticResult`s. This just prefers the second (inner) one,
unless the inner tactic is a dispreferred tactic sequence and the outer one is preferred.
This is used to implement whitespace-sensitive selection of tactic sequences. -/
merge : (r₁ : Option FindTacticResult) → (r₂ : FindTacticResult) → FindTacticResult
| some r₁@(.tacticSeq (preferred := true) ..), .tacticSeq (preferred := false) .. => r₁
| _, r₂ => r₂
/-- Main recursion for `findTactic?`. This takes a `stack` context and a root syntax `stx`,
and returns the best `FindTacticResult` it can find. It returns `none` (abort) if two or more
results are found, and `some none` (none yet) if no results are found. -/
go (stack : Syntax.Stack) (stx : Syntax) (prev? : Option String.Pos := none) :
Option (Option FindTacticResult) := do
if stx.getKind == ``Parser.Tactic.tacticSeq then
-- TODO: this implementation is a bit too strict about the beginning of tacticSeqs.
-- We would like to be able to parse
-- · |
-- foo
-- (where `|` is the cursor position) as an insertion into the sequence containing foo
-- at index 0, but we currently use the start of the tacticSeq, which is the foo token,
-- as the earliest possible location that will be associated to the sequence.
let bracket := stx[0].getKind == ``Parser.Tactic.tacticSeqBracketed
let argIdx := if bracket then 1 else 0
let (stack, stx) := ((stx[0], argIdx) :: (stx, 0) :: stack, stx[0][argIdx])
let mainRes := stx[0].getPos?.map fun pos =>
let i := Id.run do
for i in [0:stx.getNumArgs] do
if let some pos' := stx[2*i].getPos? then
if range.stop < pos' then
return i
(stx.getNumArgs + 1) / 2
.tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack)
let mut childRes := none
for i in [0:stx.getNumArgs:2] do
if let some inner := visit stx[i] then
let stack := (stx, i) :: stack
if let some child := (← go stack stx[i]) <|>
(if inner then some (.tactic ((stx[i], 0) :: stack)) else none)
then
if childRes.isSome then failure
childRes := merge mainRes child
return childRes <|> mainRes
else
let mut childRes := none
let mut prev? := prev?
for i in [0:stx.getNumArgs] do
if let some _ := visit stx[i] prev? then
if let some child ← go ((stx, i) :: stack) stx[i] prev? then
if childRes.isSome then failure
childRes := child
prev? := stx[i].getTailPos? true <|> prev?
return childRes
/--
Returns the info tree corresponding to a syntax, using `kind` and `range` for identification.
(This is not foolproof, but it is a fairly accurate proxy for `Syntax` equality and a lot cheaper
than deep comparison.)
-/
partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
(ctx? : Option ContextInfo) (t : InfoTree)
(f : ContextInfo → Info → Bool) (canonicalOnly := false) :
Option (ContextInfo × InfoTree) :=
match t with
| .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
| node@(.node i ts) => do
if let some ctx := ctx? then
if let some range := i.stx.getRange? canonicalOnly then
-- FIXME: info tree needs to be organized better so that this works
-- guard <| range.includes tgtRange
if i.stx.getKind == kind && range == tgtRange && f ctx i then
return (ctx, node)
for t in ts do
if let some res := findInfoTree? kind tgtRange (i.updateContext? ctx?) t f canonicalOnly then
return res
none
| _ => none
/--
A code action which calls all `@[command_code_action]` code actions on each command.
-/
@[code_action_provider] def cmdCodeActionProvider : CodeActionProvider := fun params snap => do
let doc ← readDoc
let startPos := doc.meta.text.lspPosToUtf8Pos params.range.start
let endPos := doc.meta.text.lspPosToUtf8Pos params.range.end
have cmds := snap.infoTree.foldInfoTree (init := #[]) fun ctx node result => Id.run do
let .node (.ofCommandInfo info) _ := node | result
let (some head, some tail) := (info.stx.getPos? true, info.stx.getTailPos? true) | result
unless head ≤ endPos && startPos ≤ tail do return result
result.push (ctx, node)
let actions := (cmdCodeActionExt.getState snap.env).2
let mut out := #[]
for (ctx, node) in cmds do
let .node (.ofCommandInfo info) _ := node | unreachable!
if let some arr := actions.onCmd.find? info.stx.getKind then
for act in arr do
try out := out ++ (← act params snap ctx node) catch _ => pure ()
for act in actions.onAnyCmd do
try out := out ++ (← act params snap ctx node) catch _ => pure ()
pure out

51
tests/lean/run/guard_msgs.lean Normal file
View file

@ -0,0 +1,51 @@
#guard_msgs in
/-- error: unknown identifier 'x' -/
#guard_msgs in
example : α := x
/--
error: unknown identifier 'x'
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: unknown identifier 'x'
-/
#guard_msgs in
#guard_msgs in
example : α := x
#guard_msgs in
/-- warning: declaration uses 'sorry' -/
#guard_msgs in
example : α := sorry
#guard_msgs in
/-- warning: declaration uses 'sorry' -/
#guard_msgs(warning) in
example : α := sorry
/-- warning: declaration uses 'sorry' -/
#guard_msgs in
#guard_msgs(error) in
example : α := sorry
#guard_msgs in
#guard_msgs(drop warning) in
example : α := sorry
#guard_msgs in
#guard_msgs(error, drop warning) in
example : α := sorry
#guard_msgs in
/-- error: unknown identifier 'x' -/
#guard_msgs(error, drop warning) in
example : α := x
#guard_msgs in
/--
error: failed to synthesize instance
OfNat α 22
-/
#guard_msgs(error) in
example : α := 22