From d48262b9afb40ed5884d775d92bd1124f3097e3c Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sat, 25 Nov 2023 16:51:13 -0500
Subject: [PATCH] fix: work around #2044 in derive handler

---
 src/Lean/Server/Rpc/Deriving.lean |  8 ++++++++
 src/Lean/Widget/UserWidget.lean   | 13 +++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 32e95ce67388..80fe0ba56997 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -42,10 +42,13 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
 
+  let indName := mkIdent indVal.name
   `(structure RpcEncodablePacket where
       $[($fieldIds : $fieldTys)]*
       deriving FromJson, ToJson
 
+    -- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
     variable $encInstBinders* in
     instance : RpcEncodable (@$(mkCIdent indVal.name) $paramIds*) :=
       { rpcEncode := enc, rpcDecode := dec }
@@ -55,6 +58,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
         return { $[$decInits],* }
+    end $indName
   )
 
 private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
@@ -92,10 +96,13 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
   let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
 
+  let indName := mkIdent indVal.name
   `(inductive RpcEncodablePacket where
       $[$ctors:ctor]*
       deriving FromJson, ToJson
 
+    -- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
     variable $encInstBinders* in
     partial instance : RpcEncodable $typeId :=
       { rpcEncode := enc, rpcDecode := dec }
@@ -107,6 +114,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
         have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec }
         let pkt : RpcEncodablePacket ← fromJson? j
         id <| match pkt with $[$decodes:matchAlt]*
+    end $indName
   )
 
 /-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure
diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index 0aa7adb32391..532ebb68f4db 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -7,6 +7,19 @@ Authors: E.W.Ayers, Wojciech Nawrocki
 import Lean.Elab.Eval
 import Lean.Server.Rpc.RequestHandling
 
+namespace Lean.Server
+open Elab Command in
+/-- Derive `Lean.Server.RpcEncodable` for a type.
+
+TODO: remove after update-stage0 -/
+elab "#mkrpcenc" n:ident : command => do
+  elabCommand <| ← `(
+    namespace $n
+    deriving instance Lean.Server.RpcEncodable for $n
+    end $n
+  )
+end Lean.Server
+
 namespace Lean.Widget
 open Meta Elab