head	1.12;
access;
symbols
	pkgsrc-2026Q3:1.10.0.2
	pkgsrc-2026Q3-base:1.10;
locks; strict;
comment	@# @;


1.12
date	2026.10.17.21.06.42;	author wiz;	state Exp;
branches;
next	1.11;
commitid	lDi21R3Z7zzsfSZG;

1.11
date	2026.09.26.11.04.54;	author wiz;	state Exp;
branches;
next	1.10;
commitid	yySJ45zkk1XaB7XG;

1.10
date	2026.08.28.18.35.12;	author wiz;	state Exp;
branches;
next	1.9;
commitid	kap2La26DzH21rTG;

1.9
date	2026.08.21.18.43.46;	author wiz;	state Exp;
branches;
next	1.8;
commitid	BYLyLPwl1tKnixSG;

1.8
date	2026.08.11.12.55.48;	author wiz;	state Exp;
branches;
next	1.7;
commitid	0E2cLSa8fQuPGdRG;

1.7
date	2026.08.03.15.03.26;	author wiz;	state Exp;
branches;
next	1.6;
commitid	fTr4kvZKuddFEcQG;

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.12
log
@lean4: update to 4.35.0.

The main new feature of Lean 4.35.0 is vcgen, a faster and more
general successor of mvcgen. It also adds lake check and lake
comparator, which check a project with Lean's kernel and, if
requested, with several independent kernels that now come with the
toolchain. On the tactic side, rwa has been redesigned, constructor
now warns when it has to choose between constructors, and grind
proves more goals about BitVec and fixed-width integers by translating
them into Nat and Int arithmetic. Decidable has a new definition
based on Bool, which makes many more equations hold by rfl.
@
text
@# $NetBSD: Makefile,v 1.11 2026/09/26 11:04:54 wiz Exp $

DISTNAME=	lean4-4.35.0
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.11
log
@lean4: update to 4.34.1.

4.34.1

This patch release contains multiple runtime fixes

4.34.0

Lean 4.34.0 focuses on the kernel: three soundness issues, found
with AI adversarial testing, have been analyzed and fixed, and a
series of additional defensive checks have been implemented for
further reinforcement. In the automation side, bv_decide gets
integrated with sym and grind interactive modes, while being ported
to the SymM preprocessor that makes it up to six times faster. Work
has continued on the floating-point API after Float and Float32
models being introduced in 4.33.0; linters can now carry state
across commands and attach code actions to their warnings, and Lake
improves its linting, caching, and error reporting.

vcgen has also undergone significant development as part of a major
release scheduled for v4.35.0.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.10 2026/08/28 18:35:12 wiz Exp $
d3 1
a3 1
DISTNAME=	lean4-4.34.1
@


1.10
log
@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.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.9 2026/08/21 18:43:46 wiz Exp $
d3 1
a3 2
DISTNAME=	lean4-4.33.1
PKGREVISION=	1
@


1.9
log
@lean4: update to 4.33.1.

This patch release contains runtime and kernel fixes.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.8 2026/08/11 12:55:48 wiz Exp $
d4 1
@


1.8
log
@lean4: update to 4.33.0.

Lean 4.33.0 concentrates on responsiveness and consolidation: the
editor keeps more of your work while you type, try? can propose
proofs on its own, lia and grind tactics are improved, and Float
stops being an opaque type. Continuing the transparency work of
v4.31.0, it also enables backward.isDefEq.respectTransparency.types
by default — the change most likely to need attention when porting.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.7 2026/08/03 15:03:26 wiz Exp $
d3 1
a3 1
DISTNAME=	lean4-4.33.0
@


1.7
log
@lean4: update to 4.32.2.

Lean 4.32.2 (2026-07-28)

This point release fixes a soundness bug in the kernel.

The issue was discovered by Ramana Kumar and reported by Kiran
Gopinathan.

A malicious meta program can trick the kernel into accepting a
proof of False, or any other theorem. The kernel’s handling of
nested inductive types with phantom type parameters was incomplete
and bypassed the type checker.

The bug can be exploited even when using comparator.

The external checker nanoda does not suffer from the same bug.
However, by the nature of this bug, it is possible to write proof
terms that exploit it and at the same time exploit unrelated bugs
in the external checker, as demonstrated by Kumar with a bug in
nanoda that was (independently) reported and fixed very recently.
We highly recommend users who have to account for malicious proofs
and follow the recommended way to validate proofs to upgrade to
the latest nanoda version as well.

The FRO takes these issues seriously and will invest in the checker
ecosystem, towards more hardening, more testing and more independent
implementations of kernels and checkers.

See issue #14576 for more details on the bug and PR #14577 for the
fix.
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.6 2026/07/25 09:57:45 wiz Exp $
d3 1
a3 1
DISTNAME=	lean4-4.32.2
@


1.6
log
@lean4: fix typo
@
text
@d1 1
a1 1
# $NetBSD: Makefile,v 1.5 2026/07/25 09:40:53 wiz Exp $
d3 1
a3 2
DISTNAME=	lean4-4.32.1
PKGREVISION=	1
@


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
@