From 37442b66f8c923b060a9d4d63a0cda373f529ba9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 00:31:16 +0000 Subject: [PATCH 1/2] fix: build UnicodeCLib with Lean's bundled C compiler Use buildLeanO instead of buildO so the C tables are compiled by the toolchain's clang with Lean's C flags (honoring LEAN_CC) instead of the system cc. Building no longer requires a system C compiler. Replace ntohl/htonl in basic.c with byte shifts, since the Lean sysroot has no arpa/inet.h; this also drops the winsock2.h dependency. Co-Authored-By: Claude Opus 5.5 --- UnicodeCLib/basic.c | 20 +++++++++----------- lakefile.lean | 4 ++-- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/UnicodeCLib/basic.c b/UnicodeCLib/basic.c index be91265f0..d5189fffb 100644 --- a/UnicodeCLib/basic.c +++ b/UnicodeCLib/basic.c @@ -1,9 +1,4 @@ #include -#ifdef _WIN32 -#include -#else -#include -#endif #include "basic.h" static inline int unicode_script_is_valid(uint32_t c) { @@ -19,16 +14,19 @@ static inline int unicode_script_is_valid(uint32_t c) { } uint32_t unicode_script_of_abbrev(b_lean_obj_arg abbr) { - lean_string_object * str = lean_to_string(abbr); - assert(str->m_size > 4); - uint32_t val = *((uint32_t*)(str->m_data)); - return ntohl(val); + assert(lean_string_size(abbr) > 4); + const unsigned char * s = (const unsigned char *)lean_string_cstr(abbr); + return (uint32_t)s[0] << 24 | (uint32_t)s[1] << 16 | (uint32_t)s[2] << 8 | (uint32_t)s[3]; } lean_obj_res unicode_script_to_abbrev(uint32_t scr) { assert(unicode_script_is_valid(scr)); lean_object * abbr = lean_alloc_string(5, 5, 4); - lean_to_string(abbr)->m_data[4] = 0; - *((uint32_t*)lean_to_string(abbr)->m_data) = htonl(scr); + char * s = lean_to_string(abbr)->m_data; + s[0] = (char)(scr >> 24 & 0xff); + s[1] = (char)(scr >> 16 & 0xff); + s[2] = (char)(scr >> 8 & 0xff); + s[3] = (char)(scr & 0xff); + s[4] = 0; return abbr; } diff --git a/lakefile.lean b/lakefile.lean index f902b6b2e..0f5066aaf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -18,8 +18,8 @@ target UnicodeCLib pkg : FilePath := do if file.path.extension == some "c" then let obj := pkg.buildDir / "UnicodeCLib" / ((file.fileName.dropSuffix ".c" |>.copy) ++ ".o") let src ← inputTextFile file.path - let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I", (pkg.dir / "UnicodeCLib").toString, "-O", "-fPIC"] - oFiles := oFiles.push <| ← buildO obj src weakArgs + let weakArgs := #["-I", (pkg.dir / "UnicodeCLib").toString, "-O3", "-DNDEBUG"] + oFiles := oFiles.push <| ← buildLeanO obj src weakArgs let name := nameToStaticLib "unicodeclib" buildStaticLib (pkg.sharedLibDir / name) oFiles From 835348a7d5b67a22a9562c84b71ec71fbb9cfe07 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 01:54:15 +0000 Subject: [PATCH 2/2] chore: go back to buildO with the system cc, tracking the Lean toolchain Keep compiling UnicodeCLib with the system C compiler as before, but add the Lean toolchain to its trace so the objects are rebuilt when lean.h changes. The portable basic.c rewrite stays. Co-Authored-By: Claude Opus 5.5 --- lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 0f5066aaf..deb938343 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -18,8 +18,8 @@ target UnicodeCLib pkg : FilePath := do if file.path.extension == some "c" then let obj := pkg.buildDir / "UnicodeCLib" / ((file.fileName.dropSuffix ".c" |>.copy) ++ ".o") let src ← inputTextFile file.path - let weakArgs := #["-I", (pkg.dir / "UnicodeCLib").toString, "-O3", "-DNDEBUG"] - oFiles := oFiles.push <| ← buildLeanO obj src weakArgs + let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I", (pkg.dir / "UnicodeCLib").toString, "-O", "-fPIC"] + oFiles := oFiles.push <| ← buildO obj src weakArgs (extraDepTrace := getLeanTrace) let name := nameToStaticLib "unicodeclib" buildStaticLib (pkg.sharedLibDir / name) oFiles