Skip to content

Commit

Permalink
fix: export symbols needed by Verso (#4884)
Browse files Browse the repository at this point in the history
Verso needed a symbol that was unexported - this exposes it again.
  • Loading branch information
david-christiansen authored Aug 1, 2024
1 parent a856016 commit 32b9de8
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/Lean/Compiler/IR/EmitC.lean
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,10 @@ def emitCInitName (n : Name) : M Unit :=
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).isPrefixOf n
!(`Lean.Compiler.LCNF).isPrefixOf n &&
!(`Lean.IR).isPrefixOf n &&
-- Lean.Server.findModuleRefs is used in Verso
(!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)

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

0 comments on commit 32b9de8

Please sign in to comment.