From 32b9de8c7736f5dc08c113a81adff662bb39ae01 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 1 Aug 2024 06:56:27 +0200 Subject: [PATCH] fix: export symbols needed by Verso (#4884) Verso needed a symbol that was unexported - this exposes it again. --- src/Lean/Compiler/IR/EmitC.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 0bbfadcaca53..074b44a0767a 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -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