Skip to content

Commit

Permalink
fix: export more symbols needed by Verso (#4956)
Browse files Browse the repository at this point in the history
This enables the Verso LSP server extensions to work.
  • Loading branch information
david-christiansen authored Aug 8, 2024
1 parent b144107 commit bcbd729
Showing 1 changed file with 7 additions and 2 deletions.
9 changes: 7 additions & 2 deletions src/Lean/Compiler/IR/EmitC.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit bcbd729

Please sign in to comment.