dc5eb40ca3
This PR adds server-side support for dedicated 'unsolved goals' and 'goals accomplished' diagnostics that will have special support in the Lean 4 VS Code extension. The special 'unsolved goals' diagnostic is adapted from the 'unsolved goals' error diagnostic, while the 'goals accomplished' diagnostic is issued when a `theorem` or `Prop`-typed `example` has no errors or `sorry`s. The Lean 4 VS Code extension companion PR is at leanprover/vscode-lean4#585. Specifically, this PR extends the diagnostics served by the language server with the following fields: - `leanTags`: Custom tags that denote the kind of diagnostic that is being served. As opposed to the `code`, `leanTags` should never be displayed in the UI. Examples introduced by this PR are a tag to distinguish 'unsolved goals' errors from other diagnostics, as well as a tag to distinguish the new 'goals accomplished' diagnostic from other diagnostics. - `isSilent`: Whether a diagnostic should not be displayed as a regular diagnostic in the editor. In VS Code, this means that the diagnostic is displayed in the InfoView under 'Messages', but that it will not be displayed under 'All Messages' and that it will also not be displayed with a squiggly line. The `isSilent` field is also implemented for `Message` so that silent diagnostics can be logged in the elaborator. All code paths except for the language server that display diagnostics to users are adjusted to filter `Message`s with `isSilent := true`.
94 lines
4 KiB
Text
94 lines
4 KiB
Text
/-
|
|
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import Lean.CoreM
|
|
import Lean.Namespace
|
|
|
|
namespace Lean
|
|
|
|
/-- Adds given declaration to the environment, respecting `debug.skipKernelTC`. -/
|
|
def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
|
|
(cancelTk? : Option IO.CancelToken := none) : Except Exception Environment :=
|
|
if debug.skipKernelTC.get opts then
|
|
addDeclWithoutChecking env decl
|
|
else
|
|
addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
|
|
|
|
private def Environment.addDeclAux (env : Environment) (opts : Options) (decl : Declaration)
|
|
(cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
|
|
env.addDeclCore (Core.getMaxHeartbeats opts).toUSize decl cancelTk? (!debug.skipKernelTC.get opts)
|
|
|
|
@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
|
|
def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
|
|
(cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
|
|
Environment.addDeclAux env opts decl cancelTk?
|
|
|
|
private def isNamespaceName : Name → Bool
|
|
| .str .anonymous _ => true
|
|
| .str p _ => isNamespaceName p
|
|
| _ => false
|
|
|
|
private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
|
|
match name with
|
|
| .str _ s =>
|
|
if s.get 0 == '_' then
|
|
-- Do not register namespaces that only contain internal declarations.
|
|
env
|
|
else
|
|
go env name
|
|
| _ => env
|
|
where go env
|
|
| .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
|
|
| _ => env
|
|
|
|
def addDecl (decl : Declaration) : CoreM Unit := do
|
|
-- register namespaces for newly added constants; this used to be done by the kernel itself
|
|
-- but that is incompatible with moving it to a separate task
|
|
-- NOTE: we do not use `getTopLevelNames` here so that inductive types are registered as
|
|
-- namespaces
|
|
modifyEnv (decl.getNames.foldl registerNamePrefixes)
|
|
|
|
if !Elab.async.get (← getOptions) then
|
|
return (← doAdd)
|
|
|
|
-- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
|
|
-- kernel checking has finished; not all cases are supported yet
|
|
let (name, info, kind) ← match decl with
|
|
| .thmDecl thm => pure (thm.name, .thmInfo thm, .thm)
|
|
| .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
|
|
| .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
|
|
| .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
|
|
| _ => return (← doAdd)
|
|
|
|
let env ← getEnv
|
|
-- no environment extension changes to report after kernel checking; ensures we do not
|
|
-- accidentally wait for this snapshot when querying extension states
|
|
let async ← env.addConstAsync (reportExts := false) name kind
|
|
-- report preliminary constant info immediately
|
|
async.commitConst async.asyncEnv (some info)
|
|
setEnv async.mainEnv
|
|
let cancelTk ← IO.CancelToken.new
|
|
let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => do
|
|
setEnv async.asyncEnv
|
|
doAdd
|
|
async.commitCheckEnv (← getEnv)
|
|
let t ← BaseIO.mapTask (fun _ => checkAct) env.checked
|
|
let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
|
|
Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
|
|
where doAdd := do
|
|
profileitM Exception "type checking" (← getOptions) do
|
|
withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
|
|
if !(← MonadLog.hasErrors) && decl.hasSorry then
|
|
logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
|
|
let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
|
|
|> ofExceptKernelException
|
|
setEnv env
|
|
|
|
def addAndCompile (decl : Declaration) : CoreM Unit := do
|
|
addDecl decl
|
|
compileDecl decl
|
|
|
|
end Lean
|