chore: clarify safety of compile-time code execution

src/Lean/Environment.lean

@@ -666,6 +666,7 @@ where
         moduleNames := s.moduleNames.push i.module
       }
       importMods is
+
 /--
   Create environment object from imports and free compacted regions after calling `act`. No live references to the
   environment object or imported objects may exist after `act` finishes. -/
@@ -724,6 +725,10 @@ def displayStats (env : Environment) : IO Unit := do
     unless fmt.isNil do IO.println ("  " ++ toString (Format.nest 2 (extDescr.statsFn s.state)))
     IO.println ("  number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0))
 
+/--
+  Evaluate the given declaration under the given environment to a value of the given type.
+  This function is only safe to use if the type matches the declaration's type in the environment
+  and if `enableInitializersExecution` has been used before importing any modules. -/
 @[extern "lean_eval_const"]
 unsafe constant evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
 
@@ -731,7 +736,7 @@ private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : Exce
   throw ("unexpected type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
 
 /-- Like `evalConst`, but first check that `constName` indeed is a declaration of type `typeName`.
-    This function is still unsafe because it cannot guarantee that `typeName` is in fact the name of the type `α`. -/
+    Note that this function cannot guarantee that `typeName` is in fact the name of the type `α`. -/
 unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName : Name) (constName : Name) : ExceptT String Id α :=
   match env.find? constName with
   | none      => throw ("unknown constant '" ++ toString constName ++ "'")

src/Lean/ImportingFlag.lean

@@ -8,16 +8,20 @@ namespace Lean
 private builtin_initialize importingRef : IO.Ref Bool ← IO.mkRef false
 
 private builtin_initialize runInitializersRef : IO.Ref Bool ← IO.mkRef false
+
 /--
   By default the `initialize` code is not executed when importing .olean files.
   When this flag is set to `true`, the initializers are executed.
   This method is meant to be used by the Lean frontend only.
 
   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: The Lean frontend executes this method at startup time.
 -/
 @[export lean_enable_initializer_execution]
-def enableInitializersExecution : IO Unit :=
+unsafe def enableInitializersExecution : IO Unit :=
   runInitializersRef.set true
 
 def isInitializerExecutionEnabled : IO Bool :=

src/Leanpkg.lean

@@ -216,7 +216,7 @@ def splitCmdlineArgs : List String → IO (String × List String × List String)
 
 end Leanpkg
 
-def main (args : List String) : IO UInt32 := do
+unsafe def main (args : List String) : IO UInt32 := do
   try
     Lean.enableInitializersExecution
     Lean.initSearchPath (← Lean.getBuildDir)