pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
lean4: add incomplete package
Module Name: pkgsrc-wip
Committed By: Thomas Klausner <wiz%NetBSD.org@localhost>
Pushed By: wiz
Date: Thu Jul 31 19:10:29 2025 +0200
Changeset: b4cb8e1344dfab73f4b6aeabd3d91343666db342
Modified Files:
Makefile
Added Files:
lean4/DESCR
lean4/Makefile
lean4/PLIST
lean4/TODO
lean4/distinfo
lean4/patches/patch-stage0_src_runtime_process.cpp
Log Message:
lean4: add incomplete package
Link failure, reported upstream.
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=b4cb8e1344dfab73f4b6aeabd3d91343666db342
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
Makefile | 1 +
lean4/DESCR | 2 ++
lean4/Makefile | 23 +++++++++++++++
lean4/PLIST | 4 +++
lean4/TODO | 20 +++++++++++++
lean4/distinfo | 6 ++++
lean4/patches/patch-stage0_src_runtime_process.cpp | 33 ++++++++++++++++++++++
7 files changed, 89 insertions(+)
diffs:
diff --git a/Makefile b/Makefile
index 68bb1e5833..dedd8ad914 100644
--- a/Makefile
+++ b/Makefile
@@ -1973,6 +1973,7 @@ SUBDIR+= ldc017
SUBDIR+= ldc120
SUBDIR+= lde
SUBDIR+= ldtp
+SUBDIR+= lean4
SUBDIR+= lebiniou
SUBDIR+= lebiniou-data
SUBDIR+= leo
diff --git a/lean4/DESCR b/lean4/DESCR
new file mode 100644
index 0000000000..2e8148c71e
--- /dev/null
+++ b/lean4/DESCR
@@ -0,0 +1,2 @@
+Lean is a proof assistant and a functional programming language.
+It is based on the calculus of constructions with inductive types.
diff --git a/lean4/Makefile b/lean4/Makefile
new file mode 100644
index 0000000000..cdcf150a5c
--- /dev/null
+++ b/lean4/Makefile
@@ -0,0 +1,23 @@
+# $NetBSD$
+
+DISTNAME= lean4-4.21.0
+CATEGORIES= math
+MASTER_SITES= ${MASTER_SITE_GITHUB:=leanprover/}
+GITHUB_TAG= v${PKGVERSION_NOREV}
+
+MAINTAINER= pkgsrc-users%NetBSD.org@localhost
+HOMEPAGE= https://github.com/leanprover/lean4/
+COMMENT= Programming language for theorem proving
+LICENSE= apache-2.0
+
+DEPENDS+= cadical-[0-9]*:../../wip/cadical
+
+USE_LANGUAGES= c c++
+USE_TOOLS+= gmake pkg-config
+
+CMAKE_CONFIGURE_ARGS+= -DUSE_MIMALLOC=no
+
+.include "../../devel/cmake/build.mk"
+.include "../../devel/libuv/buildlink3.mk"
+.include "../../devel/gmp/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/lean4/PLIST b/lean4/PLIST
new file mode 100644
index 0000000000..92ba51a2d7
--- /dev/null
+++ b/lean4/PLIST
@@ -0,0 +1,4 @@
+@comment $NetBSD$
+@comment TODO: to fill this file with the file listing:
+@comment TODO: 1. run "/usr/bin/make package"
+@comment TODO: 2. run "/usr/bin/make print-PLIST"
diff --git a/lean4/TODO b/lean4/TODO
new file mode 100644
index 0000000000..cda50231c6
--- /dev/null
+++ b/lean4/TODO
@@ -0,0 +1,20 @@
+Linking fails with
+
+
+[100%] Built target lake_lib
+[ ] Building /usr/pkgsrc/wip/lean4/work/lean4-4.21.0/cmake-pkgsrc-build/stage0/lib/lean/libLake_shared.so
+ld: /usr/pkgsrc/wip/lean4/work/lean4-4.21.0/cmake-pkgsrc-build/stage0/lib/lean/libleanshared.so: warning: Warning: reference to the libc supplied alloca(3); this most likely will not work. Please use the compiler provide
+d version of alloca(3), by supplying the appropriate compiler flags (e.g. -std=gnu99).
+ld: /usr/pkgsrc/wip/lean4/work/lean4-4.21.0/cmake-pkgsrc-build/stage0/lib/lean/libleanshared.so: note: the message above does not take linker garbage collection into account
+[100%] Built target lake_shared
+[ ] Building /usr/pkgsrc/wip/lean4/work/lean4-4.21.0/cmake-pkgsrc-build/stage0/bin/lake
+ld: /usr/pkgsrc/wip/lean4/work/lean4-4.21.0/cmake-pkgsrc-build/stage0/lib/lean/libleanshared.so: warning: Warning: reference to the libc supplied alloca(3); this most likely will not work. Please use the compiler provide
+d version of alloca(3), by supplying the appropriate compiler flags (e.g. -std=gnu99).
+ld: ../../cmake-pkgsrc-build/stage0/lib/temp/LakeMain.o.export: in function `_lean_main':
+LakeMain.c:(.text+0x1e): undefined reference to `l_Lake_cli'
+ld: ../../cmake-pkgsrc-build/stage0/lib/temp/LakeMain.o.export: in function `initialize_LakeMain':
+LakeMain.c:(.text+0x162): undefined reference to `initialize_Lake'
+ld: LakeMain.c:(.text+0x181): undefined reference to `initialize_Lake_CLI'
+
+
+https://github.com/leanprover/lean4/issues/9650
diff --git a/lean4/distinfo b/lean4/distinfo
new file mode 100644
index 0000000000..420f702c54
--- /dev/null
+++ b/lean4/distinfo
@@ -0,0 +1,6 @@
+$NetBSD$
+
+BLAKE2s (lean4-4.21.0.tar.gz) = 157b378c1d1046f582dd80a44a3b0224cb5794f43e06a7776e6c00095dd54fe5
+SHA512 (lean4-4.21.0.tar.gz) = a44e0bc10ff60c68ef5079a86f4a34a4847236ec7bd4a2a3e964bc0e9bc9f3b047563e75617066e51499b1e482266297b0ad37882d09aff1b7425a7d13b40845
+Size (lean4-4.21.0.tar.gz) = 41491073 bytes
+SHA1 (patch-stage0_src_runtime_process.cpp) = d9d813a762c060e08ac3b5c4f400a8d561b0d447
diff --git a/lean4/patches/patch-stage0_src_runtime_process.cpp b/lean4/patches/patch-stage0_src_runtime_process.cpp
new file mode 100644
index 0000000000..dad250057b
--- /dev/null
+++ b/lean4/patches/patch-stage0_src_runtime_process.cpp
@@ -0,0 +1,33 @@
+$NetBSD$
+
+clearenv() does not exist on NetBSD.
+
+--- stage0/src/runtime/process.cpp.orig 2025-07-31 11:25:32.645020915 +0000
++++ stage0/src/runtime/process.cpp
+@@ -340,6 +340,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_g
+ uint64_t tid;
+ #ifdef __APPLE__
+ lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
++#elif defined(__NetBSD__)
++ tid = (uint64_t)pthread_self();
+ #elif defined(LEAN_EMSCRIPTEN)
+ tid = 0;
+ #else
+@@ -430,7 +432,7 @@ static optional<pipe> setup_stdio(stdio
+ lean_unreachable();
+ }
+
+-#ifdef __APPLE__
++#if defined(__APPLE__) || defined(__NetBSD__)
+ extern "C" char **environ;
+ #endif
+
+@@ -446,7 +448,7 @@ static obj_res spawn(string_ref const &
+
+ if (pid == 0) {
+ if (!inherit_env) {
+-#ifdef __APPLE__
++#if defined(__APPLE__) || defined(__NetBSD__)
+ environ = NULL;
+ #else
+ clearenv();
Home |
Main Index |
Thread Index |
Old Index