diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index bd866ca93a5d..729ebb8112d4 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -96,8 +96,13 @@ def shouldExport (n : Name) : Bool := -- libleanshared to avoid Windows symbol limit !(`Lean.Compiler.LCNF).isPrefixOf n && !(`Lean.IR).isPrefixOf n && - -- Lean.Server.findModuleRefs is used in Verso - (!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs) + -- Lean.Server.findModuleRefs is used in SubVerso, and the contents of RequestM are used by the + -- full Verso as well as anything else that extends the LSP server. + (!(`Lean.Server.Watchdog).isPrefixOf n) && + (!(`Lean.Server.ImportCompletion).isPrefixOf n) && + (!(`Lean.Server.Completion).isPrefixOf n) + + def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do let ps := decl.params