pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/math/lean4
Module Name: pkgsrc
Committed By: wiz
Date: Fri Aug 28 18:35:12 UTC 2026
Modified Files:
pkgsrc/math/lean4: Makefile distinfo
pkgsrc/math/lean4/patches: patch-src_runtime_process.cpp
patch-stage0_src_runtime_process.cpp
Log Message:
lean4: prepare environment before fork
This was done between fork + exec. This reduces lake hangs due to
malloc state inherited by the child.
Bump PKGREVISION.
To generate a diff of this commit:
cvs rdiff -u -r1.9 -r1.10 pkgsrc/math/lean4/Makefile
cvs rdiff -u -r1.7 -r1.8 pkgsrc/math/lean4/distinfo
cvs rdiff -u -r1.2 -r1.3 \
pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp \
pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/math/lean4/Makefile
diff -u pkgsrc/math/lean4/Makefile:1.9 pkgsrc/math/lean4/Makefile:1.10
--- pkgsrc/math/lean4/Makefile:1.9 Fri Aug 21 18:43:46 2026
+++ pkgsrc/math/lean4/Makefile Fri Aug 28 18:35:12 2026
@@ -1,6 +1,7 @@
-# $NetBSD: Makefile,v 1.9 2026/08/21 18:43:46 wiz Exp $
+# $NetBSD: Makefile,v 1.10 2026/08/28 18:35:12 wiz Exp $
DISTNAME= lean4-4.33.1
+PKGREVISION= 1
CATEGORIES= math
MASTER_SITES= ${MASTER_SITE_GITHUB:=leanprover/}
GITHUB_TAG= v${PKGVERSION_NOREV}
Index: pkgsrc/math/lean4/distinfo
diff -u pkgsrc/math/lean4/distinfo:1.7 pkgsrc/math/lean4/distinfo:1.8
--- pkgsrc/math/lean4/distinfo:1.7 Fri Aug 21 18:43:46 2026
+++ pkgsrc/math/lean4/distinfo Fri Aug 28 18:35:12 2026
@@ -1,4 +1,4 @@
-$NetBSD: distinfo,v 1.7 2026/08/21 18:43:46 wiz Exp $
+$NetBSD: distinfo,v 1.8 2026/08/28 18:35:12 wiz Exp $
BLAKE2s (lean4-4.33.1.tar.gz) = 8639ccf7f54d47e4e90e21cd266b71698f7f9009fb2126b48553195308a4d335
SHA512 (lean4-4.33.1.tar.gz) = 72808891827abfa02c52e15cf64fc96c48a02738f5aac0331a009772512e8cad0cae18373615a734e850328d8422d32e374289805bfcaef2852efc8234867c76
@@ -7,7 +7,7 @@ SHA1 (patch-src_CMakeLists.txt) = c6620d
SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
SHA1 (patch-src_lake_Lake_Build_Common.lean) = d629442adea33b122932170b0ed13397760716d4
-SHA1 (patch-src_runtime_process.cpp) = fc4aeaf89ab47b0d0f6b086219a92fdc1badc2c4
+SHA1 (patch-src_runtime_process.cpp) = 2a064f747f0448be92e6426e1ba91e34e9d5ca60
SHA1 (patch-stage0_src_CMakeLists.txt) = 9605c8287537786cec326e6d6f041faa4ce3f1ae
SHA1 (patch-stage0_src_include_lean_lean.h) = b138c9a082107a667ee3df0623c2ab0e6b2a546f
-SHA1 (patch-stage0_src_runtime_process.cpp) = 2f4fe1485a110d545eb10bc57cd9dc9153e395c8
+SHA1 (patch-stage0_src_runtime_process.cpp) = afc46a9ee553a370da3a29ba1e907c6351a5eb1c
Index: pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp
diff -u pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp:1.2 pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp:1.3
--- pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp:1.2 Fri Jul 24 21:26:20 2026
+++ pkgsrc/math/lean4/patches/patch-src_runtime_process.cpp Fri Aug 28 18:35:12 2026
@@ -1,12 +1,25 @@
-$NetBSD: patch-src_runtime_process.cpp,v 1.2 2026/07/24 21:26:20 wiz Exp $
+$NetBSD: patch-src_runtime_process.cpp,v 1.3 2026/08/28 18:35:12 wiz Exp $
Set proper thread id on NetBSD.
clearenv() does not exist on NetBSD.
https://github.com/leanprover/lean4/pull/14543
---- src/runtime/process.cpp.orig 2026-07-23 16:38:08.850506865 +0000
+Create environment before forking
+https://github.com/leanprover/lean4/issues/14587
+
+--- src/runtime/process.cpp.orig 2026-08-15 19:18:21.000000000 +0000
+++ src/runtime/process.cpp
-@@ -341,6 +341,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
+@@ -8,7 +8,9 @@ Author: Jared Roesch
+ #include <fstream>
+ #include <iostream>
+ #include <iomanip>
++#include <map>
+ #include <utility>
++#include <vector>
+ #include <system_error>
+
+ #if defined(LEAN_WINDOWS)
+@@ -341,6 +343,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -15,7 +28,7 @@ https://github.com/leanprover/lean4/pull
#elif defined(LEAN_EMSCRIPTEN)
tid = 0;
#else
-@@ -431,7 +433,7 @@ static optional<pipe> setup_stdio(stdio cfg) {
+@@ -431,10 +435,52 @@ static optional<pipe> setup_stdio(stdio cfg) {
lean_unreachable();
}
@@ -24,12 +37,96 @@ https://github.com/leanprover/lean4/pull
extern "C" char **environ;
#endif
-@@ -454,7 +456,7 @@ static obj_res spawn(string_ref const & proc_name, arr
++static std::vector<char*> build_environ(bool inherit_env, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env) {
++ std::map<std::string, std::string> current;
++ if (inherit_env) {
++ /* Build a lookup map from current environ */
++ for (char** env = environ; *env; ++env) {
++ auto sep = std::strstr(*env, "=");
++ if (sep) {
++ std::string key(*env, sep - *env);
++ current[std::move(key)] = sep + 1;
++ }
++ }
++ }
++
++ /* Apply overrides */
++ for (auto & entry : env) {
++ if (entry.snd()) {
++ current[entry.fst().data()] = entry.snd().get()->data();
++ } else {
++ current.erase(entry.fst().data());
++ }
++ }
++
++ /* Create the new environ array */
++ std::vector<char*> result;
++ result.reserve(current.size() + 1);
++
++ for (auto & [key, val] : current) {
++ size_t key_len = key.size();
++ size_t val_len = val.size();
++ size_t total = key_len + 1 + val_len + 1;
++ char* entry = new char[total];
++ std::memcpy(entry, key.data(), key_len);
++ entry[key_len] = '=';
++ std::memcpy(entry + key_len + 1, val.data(), val_len);
++ entry[key_len + 1 + val_len] = '\0';
++ result.push_back(entry);
++ }
++
++ result.push_back(nullptr);
++ return result;
++}
++
+ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const & args, stdio stdin_mode, stdio stdout_mode,
+ stdio stderr_mode, option_ref<string_ref> const & cwd, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env,
+ bool inherit_env, bool do_setsid) {
+@@ -450,24 +496,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ pargs.push_back(strdup(arg.data()));
+ pargs.push_back(NULL);
+
++ std::vector<char*> new_env = build_environ(inherit_env, env);
++
+ int pid = fork();
if (pid == 0) {
- if (!inherit_env) {
+- if (!inherit_env) {
-#ifdef __APPLE__
-+#if defined(__APPLE__) || defined(__NetBSD__)
- environ = NULL;
- #else
- clearenv();
+- environ = NULL;
+-#else
+- clearenv();
+-#endif
+- }
+- for (auto & entry : env) {
+- if (entry.snd()) {
+- setenv(entry.fst().data(), entry.snd().get()->data(), true);
+- } else {
+- unsetenv(entry.fst().data());
+- }
+- }
+-
+ if (stdin_pipe) {
+ dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
+ close(stdin_pipe->m_write_fd);
+@@ -507,7 +540,7 @@ static obj_res spawn(string_ref const & proc_name, arr
+ lean_always_assert(setsid() >= 0);
+ }
+
+- if (execvp(pargs[0], pargs.data()) < 0) {
++ if (execvpe(pargs[0], pargs.data(), new_env.data()) < 0) {
+ std::cerr << "could not execute external process '" << pargs[0] << "'" << std::endl;
+ // See the comment above about `_exit` vs `exit`.
+ _exit(-1);
+@@ -520,6 +553,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ if (parg != NULL) {
+ free(parg);
+ }
++ }
++ for (char* entry : new_env) {
++ if (entry != NULL) {
++ free(entry);
++ }
+ }
+
+ object * parent_stdin = box(0);
Index: pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp
diff -u pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp:1.2 pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp:1.3
--- pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp:1.2 Fri Jul 24 21:26:20 2026
+++ pkgsrc/math/lean4/patches/patch-stage0_src_runtime_process.cpp Fri Aug 28 18:35:12 2026
@@ -1,12 +1,25 @@
-$NetBSD: patch-stage0_src_runtime_process.cpp,v 1.2 2026/07/24 21:26:20 wiz Exp $
+$NetBSD: patch-stage0_src_runtime_process.cpp,v 1.3 2026/08/28 18:35:12 wiz Exp $
Set proper thread id on NetBSD.
clearenv() does not exist on NetBSD.
https://github.com/leanprover/lean4/pull/14543
---- stage0/src/runtime/process.cpp.orig 2025-07-31 11:25:32.645020915 +0000
+Create environment before forking
+https://github.com/leanprover/lean4/issues/14587
+
+--- stage0/src/runtime/process.cpp.orig 2026-08-15 19:18:21.000000000 +0000
+++ stage0/src/runtime/process.cpp
-@@ -340,6 +340,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_g
+@@ -8,7 +8,9 @@ Author: Jared Roesch
+ #include <fstream>
+ #include <iostream>
+ #include <iomanip>
++#include <map>
+ #include <utility>
++#include <vector>
+ #include <system_error>
+
+ #if defined(LEAN_WINDOWS)
+@@ -341,6 +343,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -15,7 +28,7 @@ https://github.com/leanprover/lean4/pull
#elif defined(LEAN_EMSCRIPTEN)
tid = 0;
#else
-@@ -430,7 +432,7 @@ static optional<pipe> setup_stdio(stdio
+@@ -431,10 +435,52 @@ static optional<pipe> setup_stdio(stdio cfg) {
lean_unreachable();
}
@@ -24,12 +37,96 @@ https://github.com/leanprover/lean4/pull
extern "C" char **environ;
#endif
-@@ -446,7 +448,7 @@ static obj_res spawn(string_ref const &
++static std::vector<char*> build_environ(bool inherit_env, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env) {
++ std::map<std::string, std::string> current;
++ if (inherit_env) {
++ /* Build a lookup map from current environ */
++ for (char** env = environ; *env; ++env) {
++ auto sep = std::strstr(*env, "=");
++ if (sep) {
++ std::string key(*env, sep - *env);
++ current[std::move(key)] = sep + 1;
++ }
++ }
++ }
++
++ /* Apply overrides */
++ for (auto & entry : env) {
++ if (entry.snd()) {
++ current[entry.fst().data()] = entry.snd().get()->data();
++ } else {
++ current.erase(entry.fst().data());
++ }
++ }
++
++ /* Create the new environ array */
++ std::vector<char*> result;
++ result.reserve(current.size() + 1);
++
++ for (auto & [key, val] : current) {
++ size_t key_len = key.size();
++ size_t val_len = val.size();
++ size_t total = key_len + 1 + val_len + 1;
++ char* entry = new char[total];
++ std::memcpy(entry, key.data(), key_len);
++ entry[key_len] = '=';
++ std::memcpy(entry + key_len + 1, val.data(), val_len);
++ entry[key_len + 1 + val_len] = '\0';
++ result.push_back(entry);
++ }
++
++ result.push_back(nullptr);
++ return result;
++}
++
+ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const & args, stdio stdin_mode, stdio stdout_mode,
+ stdio stderr_mode, option_ref<string_ref> const & cwd, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env,
+ bool inherit_env, bool do_setsid) {
+@@ -450,24 +496,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ pargs.push_back(strdup(arg.data()));
+ pargs.push_back(NULL);
+
++ std::vector<char*> new_env = build_environ(inherit_env, env);
++
+ int pid = fork();
if (pid == 0) {
- if (!inherit_env) {
+- if (!inherit_env) {
-#ifdef __APPLE__
-+#if defined(__APPLE__) || defined(__NetBSD__)
- environ = NULL;
- #else
- clearenv();
+- environ = NULL;
+-#else
+- clearenv();
+-#endif
+- }
+- for (auto & entry : env) {
+- if (entry.snd()) {
+- setenv(entry.fst().data(), entry.snd().get()->data(), true);
+- } else {
+- unsetenv(entry.fst().data());
+- }
+- }
+-
+ if (stdin_pipe) {
+ dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
+ close(stdin_pipe->m_write_fd);
+@@ -507,7 +540,7 @@ static obj_res spawn(string_ref const & proc_name, arr
+ lean_always_assert(setsid() >= 0);
+ }
+
+- if (execvp(pargs[0], pargs.data()) < 0) {
++ if (execvpe(pargs[0], pargs.data(), new_env.data()) < 0) {
+ std::cerr << "could not execute external process '" << pargs[0] << "'" << std::endl;
+ // See the comment above about `_exit` vs `exit`.
+ _exit(-1);
+@@ -520,6 +553,11 @@ static obj_res spawn(string_ref const & proc_name, arr
+ if (parg != NULL) {
+ free(parg);
+ }
++ }
++ for (char* entry : new_env) {
++ if (entry != NULL) {
++ free(entry);
++ }
+ }
+
+ object * parent_stdin = box(0);
Home |
Main Index |
Thread Index |
Old Index