diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 729ebb8112..0300971705 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -91,19 +91,6 @@ def toCInitName (n : Name) : M String := do def emitCInitName (n : Name) : M Unit := toCInitName n >>= emit -def shouldExport (n : Name) : Bool := - -- HACK: exclude symbols very unlikely to be used by the interpreter or other consumers of - -- libleanshared to avoid Windows symbol limit - !(`Lean.Compiler.LCNF).isPrefixOf n && - !(`Lean.IR).isPrefixOf n && - -- 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 let env ← getEnv @@ -112,7 +99,7 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U else if isExternal then emit "extern " else emit "LEAN_EXPORT " else - if !isExternal && shouldExport decl.name then emit "LEAN_EXPORT " + if !isExternal then emit "LEAN_EXPORT " emit (toCType decl.resultType ++ " " ++ cppBaseName) unless ps.isEmpty do emit "(" @@ -658,7 +645,7 @@ def emitDeclAux (d : Decl) : M Unit := do let baseName ← toCName f; if xs.size == 0 then emit "static " - else if shouldExport f then + else emit "LEAN_EXPORT " -- make symbol visible to the interpreter emit (toCType t); emit " "; if xs.size > 0 then