From 285530c24567f09b507870ea4aeafe97a80a224a Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Thu, 23 Jul 2026 13:08:44 +0000 Subject: [PATCH 1/4] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 728ce7a44..98e74c348 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-07-22 +leanprover/lean4-pr-releases:pr-release-14505-09e325e From 64e06c5849d4ab781b4a6ea8009e22dc1fcfce44 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 23 Jul 2026 13:19:56 +0000 Subject: [PATCH 2/4] reference: remove obsolete manual calls of runtime initializers --- reference-manual/Manual/Runtime.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/reference-manual/Manual/Runtime.lean b/reference-manual/Manual/Runtime.lean index 6119a189f..554bd8e97 100644 --- a/reference-manual/Manual/Runtime.lean +++ b/reference-manual/Manual/Runtime.lean @@ -472,13 +472,11 @@ For modules in the Lean core (e.g., {module}`Init.Prelude`), the initializer is Module initializers will automatically initialize any imported modules. They are also idempotent (when run with the same `builtin` flag), but not thread-safe. -*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling `lean_initialize()` or `lean_initialize_runtime_module()`. +*Important for process-related functionality*: applications that use process-related functions from `libuv`, such as {name}`Std.IO.Process.getProcessTitle` and {name}`Std.IO.Process.setProcessTitle`, must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) *before* calling any module initializer. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on. -Together with initialization of the Lean runtime, code like the following should be run exactly once before accessing any Lean declarations: +Putting everything together, code like the following should be run exactly once before accessing any Lean declarations: ```C -void lean_initialize_runtime_module(); -void lean_initialize(); char ** lean_setup_args(int argc, char ** argv); lean_object * initialize_A_B(uint8_t builtin); @@ -486,9 +484,6 @@ lean_object * initialize_C(uint8_t builtin); ... argv = lean_setup_args(argc, argv); // if using process-related functionality -lean_initialize_runtime_module(); -// necessary (and replaces `lean_initialize_runtime_module`) for code that (indirectly) accesses the `Lean` package: -//lean_initialize(); lean_object * res; // use same default as for Lean executables From 0149497b3f43cef50246198c45ae255ef0208bd9 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sun, 26 Jul 2026 14:18:47 +0000 Subject: [PATCH 3/4] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 98e74c348..fed22e359 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14505-09e325e +leanprover/lean4-pr-releases:pr-release-14505-63a979f From 4e70dd4570f46fa886c991e149b5c8ef08f050da Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Mon, 27 Jul 2026 11:40:03 +0000 Subject: [PATCH 4/4] downstream: undo overrides --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index fed22e359..728ce7a44 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14505-63a979f +leanprover/lean4:nightly-2026-07-22