fix: work around leanprover#2044 in derive handler

Vtec234 · Dec 15, 2023 · 73b614d · 73b614d
1 parent 7d004a8
commit 73b614d
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git 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
@@ -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