fix: explicitly initialize Std in lean_initialize (#4668)

Fixes the stage 2 build, which runs with `prefer_native=true`
leanprover · Jul 6, 2024 · 4ed7947 · 4ed7947
1 parent 55d09a3
commit 4ed7947
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 4 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -300,11 +300,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
     string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
 else()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -313,7 +313,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB} -lStd")
+string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,

diff --git a/src/Std/Data/DHashMap.lean b/src/Std/Data/DHashMap.lean
@@ -5,5 +5,6 @@ Authors: Markus Himmel
 -/
 prelude
 import Std.Data.DHashMap.Basic
+import Std.Data.DHashMap.RawLemmas
 import Std.Data.DHashMap.Lemmas
 import Std.Data.DHashMap.AdditionalOperations
diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 extern "C" object* initialize_Init(uint8_t, object* w);
+extern "C" object* initialize_Std(uint8_t, object* w);
 extern "C" object* initialize_Lean(uint8_t, object* w);
 
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
@@ -27,7 +28,13 @@ extern "C" LEAN_EXPORT void lean_initialize() {
     save_stack_info();
     initialize_util_module();
     uint8_t builtin = 1;
+    // Initializing the core libs explicitly is necessary because of references to them other than
+    // via `import`, such as:
+    // * calling exported Lean functions from C++
+    // * calling into native code of the current module from a previous stage when `prefer_native`
+    //   is set
     consume_io_result(initialize_Init(builtin, io_mk_world()));
+    consume_io_result(initialize_Std(builtin, io_mk_world()));
     consume_io_result(initialize_Lean(builtin, io_mk_world()));
     initialize_kernel_module();
     init_default_print_fn();