chore: remove LEAN_EXPORT denylist workaround
This commit is contained in:
parent
8d12dd87a4
commit
9d0302e749
1 changed files with 2 additions and 15 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue