diff --git a/src/Init/Lean/Compiler/ExportAttr.lean b/src/Init/Lean/Compiler/ExportAttr.lean index 10c303d200..c98c777471 100644 --- a/src/Init/Lean/Compiler/ExportAttr.lean +++ b/src/Init/Lean/Compiler/ExportAttr.lean @@ -33,6 +33,8 @@ def getExportNameFor (env : Environment) (n : Name) : Option Name := exportAttr.getParam env n def isExport (env : Environment) (n : Name) : Bool := -(getExportNameFor env n).isSome +-- The main function morally is an exported function as well. In particular, +-- it should not participate in borrow inference. +(getExportNameFor env n).isSome || n == `main end Lean diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 847e500054..f1590976b8 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -453,6 +453,12 @@ static obj_res mark_persistent_fn(obj_arg o) { return lean_box(0); } +#if defined(__has_feature) +#if __has_feature(address_sanitizer) +#include +#endif +#endif + extern "C" void lean_mark_persistent(object * o) { buffer todo; todo.push_back(o); @@ -467,6 +473,16 @@ extern "C" void lean_mark_persistent(object * o) { LEAN_BYTE(o->m_header, 5) = LEAN_PERSISTENT_MEM_KIND; #else o->m_mem_kind = LEAN_PERSISTENT_MEM_KIND; +#endif +#if defined(__has_feature) +#if __has_feature(address_sanitizer) + // do not report as leak + // NOTE: Most persistent objects are actually reachable from global + // variables up to the end of the process. However, this is *not* + // true for closures inside of persistent thunks, which are + // "orphaned" after being evaluated. + __lsan_ignore_object(o); +#endif #endif uint8_t tag = lean_ptr_tag(o); if (tag <= LeanMaxCtorTag) {