feat: add flag for controlling the execution of initialize commands when importing modules programmatically

Fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Environment.20extensions.20in.20importModules

src/Lean/Compiler/InitAttr.lean

@@ -45,7 +45,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO
         else throwError "initialization function must have type `IO Unit`"
     afterImport := fun entries => do
       let ctx ← read
-      if runAfterImport then
+      if runAfterImport && (← isInitializerExecutionEnabled) then
         for modEntries in entries do
           for (decl, initDecl) in modEntries do
             if initDecl.isAnonymous then

src/Lean/ImportingFlag.lean

@@ -7,6 +7,22 @@ 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: The Lean frontend executes this method at startup time.
+-/
+@[export lean_enable_initializer_execution]
+def enableInitializersExecution : IO Unit :=
+  runInitializersRef.set true
+
+def isInitializerExecutionEnabled : IO Bool :=
+  runInitializersRef.get
+
 /- We say Lean is "initializing" when it is executing `builtin_initialize` declarations and importing modules.
    Recall that Lean excutes `initialize` declarations while importing modules. -/
 def initializing : IO Bool :=
@@ -29,5 +45,6 @@ def withImporting (x : IO α) : IO α :=
     x
   finally
     importingRef.set false
+    runInitializersRef.set false
 
 end Lean

src/shell/CMakeLists.txt

@@ -211,3 +211,11 @@ add_test(NAME leanpkgtest_prv
            export PATH=${LEAN_BIN}:$PATH
            find . -name '*.olean' -delete
            leanmake 2>&1 | grep 'error: field.*private'")
+
+add_test(NAME leanpkgtest_user_attr_app
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app"
+         COMMAND bash -c "
+           set -eu
+           export PATH=${LEAN_BIN}:$PATH
+           find . -name '*.olean' -delete
+           leanmake bin LINK_OPTS=-rdynamic && build/bin/UserAttr")

src/shell/lean.cpp

@@ -379,6 +379,8 @@ void check_optarg(char const * option_name) {
     }
 }
 
+extern "C" object * lean_enable_initializer_execution(object * w);
+
 int main(int argc, char ** argv) {
 #ifdef LEAN_EMSCRIPTEN
     // When running in command-line mode under Node.js, we make system directories available in the virtual filesystem.
@@ -412,7 +414,7 @@ int main(int argc, char ** argv) {
     bool only_deps = false;
     bool stats = false;
     // 0 = don't run server, 1 = watchdog, 2 = worker
-    int run_server = 0; 
+    int run_server = 0;
     unsigned num_threads    = 0;
 #if defined(LEAN_MULTI_THREAD)
     num_threads = hardware_concurrency();
@@ -429,6 +431,7 @@ int main(int argc, char ** argv) {
         std::cerr << "error: " << ex.what() << std::endl;
         return 1;
     }
+    consume_io_result(lean_enable_initializer_execution(io_mk_world()));
 
     options opts = get_default_options();
     optional<std::string> server_in;
@@ -578,7 +581,7 @@ int main(int argc, char ** argv) {
             return run_server_watchdog(forwarded_args);
         else if (run_server == 2)
             return run_server_worker();
-            
+
         if (use_stdin) {
             if (argc - optind != 0) {
                 mod_fn = argv[optind++];

tests/leanpkg/user_attr_app/.gitignore

@@ -0,0 +1 @@
+/build

tests/leanpkg/user_attr_app/UserAttr.lean

@@ -0,0 +1,30 @@
+import UserAttr.Tst
+
+open Lean
+
+def tst : MetaM Unit := do
+  let env ← getEnv
+  assert! (blaAttr.hasTag env `f)
+  assert! (blaAttr.hasTag env `g)
+  assert! !(blaAttr.hasTag env `id)
+  pure ()
+
+#eval tst
+
+def declareLeanPath : MetaM Unit := do
+  addAndCompile <| Declaration.defnDecl {
+    name  := `leanPath
+    type  := mkConst ``String
+    value := toExpr <| System.SearchPath.separator.toString.intercalate ((← Lean.getBuiltinSearchPath).map toString)
+    levelParams := []
+    hints := ReducibilityHints.abbrev
+    safety := DefinitionSafety.safe
+  }
+
+#eval declareLeanPath
+
+#eval leanPath
+
+unsafe def main : IO Unit := do
+  initSearchPath s!"{leanPath}{System.SearchPath.separator}build"
+  withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => ()

tests/leanpkg/user_attr_app/UserAttr/BlaAttr.lean

@@ -0,0 +1,5 @@
+import Lean
+
+open Lean
+
+initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"

tests/leanpkg/user_attr_app/UserAttr/Tst.lean

@@ -0,0 +1,4 @@
+import UserAttr.BlaAttr
+
+@[bla] def f (x : Nat) := x + 2
+@[bla] def g (x : Nat) := x + 1

tests/leanpkg/user_attr_app/leanpkg.toml

@@ -0,0 +1,3 @@
+[package]
+name = "UserAttr"
+version = "0.1"