feat: rpc attribute

Functions can now be marked with the `@[rpc]` attribute, which
registers the function as an RpcProcedure that can be used to
communicate with the code editor and infoview.

src/Lean/Server/Rpc/RequestHandling.lean

@@ -121,4 +121,15 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do
       }
   setEnv <| userRpcProcedures.insert (← getEnv) method wrappedName
 
+builtin_initialize registerBuiltinAttribute {
+  name := `rpc
+  descr := "Marks a function as a Lean server RPC method.
+    Shorthand for `registerRpcProcedure`.
+    The function must have type `α → RequestM (RequestTask β)` with
+    RpcEncodings for both α and β."
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add := fun decl stx kind =>
+    registerRpcProcedure decl
+}
+
 end Lean.Server