From e4014f2023f3bca0f6c1a3a9fd0ae33fa9f45837 Mon Sep 17 00:00:00 2001 From: Ahmed Sami Date: Wed, 26 Feb 2025 19:00:45 +0100 Subject: [PATCH] Increase severity of `uses 'sorry'`. Fixes #276 --- server/GameServer/RpcHandlers.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index ce4e61ca..e31436c6 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -231,6 +231,11 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo -- Answer: The last snap only copied the diags from the end of this snap let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray + -- Increase the severity of `uses 'sorry'` warnings + diag := diag.map (fun d => if d.toDiagnostic.message == "declaration uses 'sorry'" + then { d with severity? := some Lsp.DiagnosticSeverity.error } + else d) + -- Level is completed if there are no errors or warnings let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)