head	1.9;
access;
symbols
	pkgsrc-2026Q3:1.8.0.2
	pkgsrc-2026Q3-base:1.8;
locks; strict;
comment	@# @;


1.9
date	2026.09.26.11.04.54;	author wiz;	state Exp;
branches;
next	1.8;
commitid	yySJ45zkk1XaB7XG;

1.8
date	2026.08.28.18.35.12;	author wiz;	state Exp;
branches;
next	1.7;
commitid	kap2La26DzH21rTG;

1.7
date	2026.08.21.18.43.46;	author wiz;	state Exp;
branches;
next	1.6;
commitid	BYLyLPwl1tKnixSG;

1.6
date	2026.08.11.12.55.48;	author wiz;	state Exp;
branches;
next	1.5;
commitid	0E2cLSa8fQuPGdRG;

1.5
date	2026.08.03.15.03.26;	author wiz;	state Exp;
branches;
next	1.4;
commitid	fTr4kvZKuddFEcQG;

1.4
date	2026.07.25.11.24.52;	author wiz;	state Exp;
branches;
next	1.3;
commitid	2DeuV99SDILBJ1PG;

1.3
date	2026.07.25.09.40.53;	author wiz;	state Exp;
branches;
next	1.2;
commitid	QkGYt3UO5W3C91PG;

1.2
date	2026.07.24.21.26.20;	author wiz;	state Exp;
branches;
next	1.1;
commitid	qCqdT6bIOr7V5XOG;

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


desc
@@


1.9
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
@$NetBSD: distinfo,v 1.8 2026/08/28 18:35:12 wiz Exp $

BLAKE2s (lean4-4.34.1.tar.gz) = 1590c61336410c0d4be667d4c0170a9af6f05a007df1b91aa6d7ddc721d700e8
SHA512 (lean4-4.34.1.tar.gz) = d8024237a6741fd2391e7127d2de80178b4e1dc811220c51c04890b5575e4075a10de82ca950d352aa605043596673d45ed9c851f2735ea29b5992cf4612477f
Size (lean4-4.34.1.tar.gz) = 87768894 bytes
SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
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) = 2a064f747f0448be92e6426e1ba91e34e9d5ca60
SHA1 (patch-stage0_src_CMakeLists.txt) = 9605c8287537786cec326e6d6f041faa4ce3f1ae
SHA1 (patch-stage0_src_include_lean_lean.h) = b138c9a082107a667ee3df0623c2ab0e6b2a546f
SHA1 (patch-stage0_src_runtime_process.cpp) = afc46a9ee553a370da3a29ba1e907c6351a5eb1c
@


1.8
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: distinfo,v 1.7 2026/08/21 18:43:46 wiz Exp $
d3 3
a5 3
BLAKE2s (lean4-4.33.1.tar.gz) = 8639ccf7f54d47e4e90e21cd266b71698f7f9009fb2126b48553195308a4d335
SHA512 (lean4-4.33.1.tar.gz) = 72808891827abfa02c52e15cf64fc96c48a02738f5aac0331a009772512e8cad0cae18373615a734e850328d8422d32e374289805bfcaef2852efc8234867c76
Size (lean4-4.33.1.tar.gz) = 86700313 bytes
@


1.7
log
@lean4: update to 4.33.1.

This patch release contains runtime and kernel fixes.
@
text
@d1 1
a1 1
$NetBSD: distinfo,v 1.6 2026/08/11 12:55:48 wiz Exp $
d10 1
a10 1
SHA1 (patch-src_runtime_process.cpp) = fc4aeaf89ab47b0d0f6b086219a92fdc1badc2c4
d13 1
a13 1
SHA1 (patch-stage0_src_runtime_process.cpp) = 2f4fe1485a110d545eb10bc57cd9dc9153e395c8
@


1.6
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: distinfo,v 1.5 2026/08/03 15:03:26 wiz Exp $
d3 3
a5 3
BLAKE2s (lean4-4.33.0.tar.gz) = b927ea9d3bb6b62527cecdf4c898702d0783a2a2328413b6d2f6b9b74bab5953
SHA512 (lean4-4.33.0.tar.gz) = 76cc04f43fd25c482fab228264ed69045e2fe1c0b4de265d43d74a2565f18467393e76002f2029016a86d7ec90e1a5ec585f328a60556cd0d4003c4a710a7b5e
Size (lean4-4.33.0.tar.gz) = 86677749 bytes
@


1.5
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: distinfo,v 1.4 2026/07/25 11:24:52 wiz Exp $
d3 3
a5 3
BLAKE2s (lean4-4.32.2.tar.gz) = 5b567d9f8786f74582b655087f33255414a3f681910fb7457aa71d1ef8830a27
SHA512 (lean4-4.32.2.tar.gz) = f17beb7f04cdb8f1342af888341bb3b7b21c1a990ec264f6fc453f493a37c2fd77229f70cdc011e4e1a05589098817d7f502197de3f19539b666455932d160f5
Size (lean4-4.32.2.tar.gz) = 75093554 bytes
d9 1
a9 1
SHA1 (patch-src_lake_Lake_Build_Common.lean) = 2fd83850d22ba26beb56b8bd26bb3473b897aee8
@


1.4
log
@lean4: another patch filed upstream
@
text
@d1 1
a1 1
$NetBSD: distinfo,v 1.3 2026/07/25 09:40:53 wiz Exp $
d3 3
a5 3
BLAKE2s (lean4-4.32.1.tar.gz) = 9d98b0fcb0d958bdbbe110d108c6138c5e6f9c3e335dd16095761a13eb2da43e
SHA512 (lean4-4.32.1.tar.gz) = c180c406c6d9b6c28705f93ac3fad64b1a975f76cc11ae8ba2b4447ff668e2babac2bf3dd997bae2a38b196767353b484b1674a6a21a145e9a37dc3879d3029f
Size (lean4-4.32.1.tar.gz) = 75094335 bytes
@


1.3
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: distinfo,v 1.2 2026/07/24 21:26:20 wiz Exp $
d8 1
a8 1
SHA1 (patch-src_include_lean_lean.h) = 8051d7be7f01bb5a48974bcf777ea5bed0240f25
d12 1
a12 1
SHA1 (patch-stage0_src_include_lean_lean.h) = 19e6c3e23705e03d6bb33e2e21330f007b64d761
@


1.2
log
@lean4: add links to upstream pull request
@
text
@d1 1
a1 1
$NetBSD: distinfo,v 1.1 2026/07/24 18:39:20 wiz Exp $
d8 1
d12 1
@


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$
d6 1
a6 1
SHA1 (patch-src_CMakeLists.txt) = 055656efbe3796c5948f59da8f6709ac68ba9d66
d9 3
a11 3
SHA1 (patch-src_runtime_process.cpp) = 4a4723d9f69046d51ad351dff20120db0e1b40f9
SHA1 (patch-stage0_src_CMakeLists.txt) = 5a7a307617e1ca566c0cec698c308588edd3ceda
SHA1 (patch-stage0_src_runtime_process.cpp) = 18f705c5f58a2a60d98930a0ff59baf49b522bdd
@