Skip to content

Commit d387e97

Browse files
david-christiansenKha
authored andcommitted
fix: export more symbols needed by Verso (#4956)
This enables the Verso LSP server extensions to work. (cherry picked from commit bcbd729)
1 parent daa2218 commit d387e97

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

src/Lean/Compiler/IR/EmitC.lean

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,8 +96,13 @@ def shouldExport (n : Name) : Bool :=
9696
-- libleanshared to avoid Windows symbol limit
9797
!(`Lean.Compiler.LCNF).isPrefixOf n &&
9898
!(`Lean.IR).isPrefixOf n &&
99-
-- Lean.Server.findModuleRefs is used in Verso
100-
(!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)
99+
-- Lean.Server.findModuleRefs is used in SubVerso, and the contents of RequestM are used by the
100+
-- full Verso as well as anything else that extends the LSP server.
101+
(!(`Lean.Server.Watchdog).isPrefixOf n) &&
102+
(!(`Lean.Server.ImportCompletion).isPrefixOf n) &&
103+
(!(`Lean.Server.Completion).isPrefixOf n)
104+
105+
101106

102107
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
103108
let ps := decl.params

0 commit comments

Comments
 (0)