From aa45e994592294da2ae811b6e02bb87416f97ea4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 8 Aug 2024 12:14:45 +0200 Subject: [PATCH] fix: export more symbols needed by Verso This enables the Verso LSP server extensions to work. --- src/Lean/Compiler/IR/EmitC.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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