From ff45efe3fa99cb5ea677b0740beb65a994e2258a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 9 Aug 2023 12:39:04 +0200 Subject: [PATCH] doc: one more `enableInitializersExecution` remark --- src/Lean/ImportingFlag.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean index 9ac26b66e4..2a43538dd9 100644 --- a/src/Lean/ImportingFlag.lean +++ b/src/Lean/ImportingFlag.lean @@ -17,6 +17,8 @@ Remark: it is not safe to run `initialize` code when using multiple threads. Remark: Any loaded native Lean code must match its imported version. In particular, no two versions of the same module may be loaded when this flag is set. No native code may be loaded after its module has been imported. +Remark: Compacted module regions must not be freed when using this flag as the + cached initializer results may reference objects in them. Remark: The Lean frontend executes this method at startup time. -/ @[export lean_enable_initializer_execution]