head	1.6;
access;
symbols;
locks; strict;
comment	@# @;


1.6
date	2026.07.25.09.57.45;	author wiz;	state Exp;
branches;
next	1.5;
commitid	zjQSatz1m40Kf1PG;

1.5
date	2026.07.25.09.40.53;	author wiz;	state Exp;
branches;
next	1.4;
commitid	QkGYt3UO5W3C91PG;

1.4
date	2026.07.24.21.27.47;	author wiz;	state Exp;
branches;
next	1.3;
commitid	21QqwH7D7DNp6XOG;

1.3
date	2026.07.24.18.42.07;	author wiz;	state Exp;
branches;
next	1.2;
commitid	ByaaI2Zu0pFCbWOG;

1.2
date	2026.07.24.18.41.55;	author wiz;	state Exp;
branches;
next	1.1;
commitid	vklJHwtKWWLwbWOG;

1.1
date	2026.07.24.18.39.19;	author wiz;	state Exp;
branches;
next	;
commitid	nN62qu9ZRD0EaWOG;


desc
@@


1.6
log
@lean4: fix typo
@
text
@# $NetBSD: Makefile,v 1.5 2026/07/25 09:40:53 wiz Exp $

DISTNAME=	lean4-4.32.1
PKGREVISION=	1
CATEGORIES=	math
MASTER_SITES=	${MASTER_SITE_GITHUB:=leanprover/}
GITHUB_TAG=	v${PKGVERSION_NOREV}

MAINTAINER=	pkgsrc-users@@NetBSD.org
HOMEPAGE=	https://lean-lang.org/
#HOMEPAGE=	https://github.com/leanprover/lean4/
COMMENT=	Programming language for theorem proving
LICENSE=	apache-2.0

DEPENDS+=	leantar-[0-9]*:../../math/leantar
DEPENDS+=	cadical>=3:../../math/cadical3

USE_LANGUAGES=	c c++
USE_TOOLS+=	bash:run gmake pkg-config

USE_CXX_FEATURES=	c++20

# needed for stage0 tools that are called during build and installation
MAKE_ENV+=	LD_LIBRARY_PATH=${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib/lean:${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib
INSTALL_ENV+=	LD_LIBRARY_PATH=${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib/lean:${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib

INSTALLATION_DIRS+=	share/lean4

CMAKE_CONFIGURE_ARGS+=	-DUSE_MIMALLOC=no
# stage0/stage1 options need to be passed explicitly
CMAKE_CONFIGURE_ARGS+=	-DSTAGE0_CMAKE_PREFIX_PATH=${BUILDLINK_DIR}
CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_CMAKE_INSTALL_PREFIX=${PREFIX}
# don't install these binaries, they are dependencies
CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_INSTALL_CADICAL=OFF
CMAKE_CONFIGURE_ARGS+=	-DSTAGE1_INSTALL_LEANTAR=OFF

# LDFLAGS from environment are ignored
CMAKE_CONFIGURE_ARGS+=	-DTOOLCHAIN_SHARED_LINKER_FLAGS=${LDFLAGS:Q}

LDFLAGS+=	${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean

REPLACE_BASH+=	src/bin/leanmake
REPLACE_BASH+=	stage0/src/bin/leanmake

# avoid pkgsrc cwrapper cc in installed file
SUBST_CLASSES+=		cc
SUBST_FILES.cc+=	src/Leanc.lean
SUBST_FILES.cc+=	src/lake/Lake/Build/Common.lean
SUBST_SED.cc+=		-e "s,@@LEANC_CC@@,${CC},"
SUBST_SED.cc+=		-e "s!@@LINKER_FLAGS@@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\"!"
SUBST_STAGE.cc=		pre-configure
SUBST_MESSAGE.cc=	Setting compiler path.

# CMakeLists.txt: "Only makefile generators are supported"
CMAKE_GENERATORS_INCOMPATIBLE=	ninja

post-install:
	${MV} ${DESTDIR}${PREFIX}/LICENSE* ${DESTDIR}${PREFIX}/share/lean4
	${CHMOD} a+x ${DESTDIR}${PREFIX}/lib/lean/*.so

.include "../../devel/cmake/build.mk"
.include "../../devel/libuv/buildlink3.mk"
BUILDLINK_API_DEPENDS.gmp+=	gmp>=5.0.5
.include "../../devel/gmp/buildlink3.mk"
.include "../../security/openssl/buildlink3.mk"
.include "../../mk/bsd.pkg.mk"
@


1.5
log
@lean4: fix alloca warning (during package build, and 'lake build')

The -std=gnu99 didn't help because alloca() was used in a C++ file.
Replace calls to alloca with __builtin_alloca instead, and get rid of
the forced gnu99.

Bump PKGREVISION.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.4 2026/07/24 21:27:47 wiz Exp $
d33 1
a33 1
# not install these binaries, they are dependencies
@


1.4
log
@lean4: needs gnu99 for alloca()
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.3 2026/07/24 18:42:07 wiz Exp $
d4 1
a20 1
USE_CC_FEATURES=	c99
a21 2
# for alloca()
FORCE_C_STD=		gnu99
@


1.3
log
@lean4: fix typo
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.2 2026/07/24 18:41:55 wiz Exp $
d20 1
d22 2
@


1.2
log
@lean4: make leantar a full dependency

ride import
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.1 2026/07/24 18:39:19 wiz Exp $
d14 1
a14 1
_DEPENDS+=	leantar-[0-9]*:../../math/leantar
@


1.1
log
@math/lean4: import lean4-4.32.1

Lean is a proof assistant and a functional programming language.
It is based on the calculus of constructions with inductive types.
@
text
@d1 1
a1 1
# $NetBSD$
d14 1
a14 1
TOOL_DEPENDS+=	leantar-[0-9]*:../../math/leantar
@