From 4972f214be58fb932205b6c563aa4fbfb94673c2 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 22 May 2022 14:43:32 -0400 Subject: [PATCH] fix: sorried errors in rpcServerMethod --- src/Lean/Server/Rpc/RequestHandling.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 538384c7cd..8e2ee4c0fc 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -108,9 +108,10 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do throwError s!"{errMsg}: already registered" let wrappedName := method ++ `_rpc_wrapped let procT := mkConst ``RpcProcedure - let proc ← MetaM.run' <| TermElabM.run' <| do - let c ← Lean.Elab.Term.elabTerm (← `(wrapRpcProcedure $(quote method) _ _ $(mkIdent method))) procT - return ← instantiateMVars c + let proc ← MetaM.run' <| TermElabM.run' <| withoutErrToSorry do + let stx ← ``(wrapRpcProcedure $(quote method) _ _ $(mkIdent method)) + let c ← Lean.Elab.Term.elabTerm stx procT + instantiateMVars c addAndCompile <| Declaration.defnDecl { name := wrappedName type := procT