CVS commit: pkgsrc/math/lean4

["Thomas Klausner" <wiz%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   wiz
Date:           Mon Aug  3 15:03:26 UTC 2026

Modified Files:
        pkgsrc/math/lean4: Makefile distinfo

Log Message:
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.


To generate a diff of this commit:
cvs rdiff -u -r1.6 -r1.7 pkgsrc/math/lean4/Makefile
cvs rdiff -u -r1.4 -r1.5 pkgsrc/math/lean4/distinfo

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/math/lean4/Makefile
diff -u pkgsrc/math/lean4/Makefile:1.6 pkgsrc/math/lean4/Makefile:1.7
--- pkgsrc/math/lean4/Makefile:1.6      Sat Jul 25 09:57:45 2026
+++ pkgsrc/math/lean4/Makefile  Mon Aug  3 15:03:26 2026
@@ -1,7 +1,6 @@
-# $NetBSD: Makefile,v 1.6 2026/07/25 09:57:45 wiz Exp $
+# $NetBSD: Makefile,v 1.7 2026/08/03 15:03:26 wiz Exp $
 
-DISTNAME=      lean4-4.32.1
-PKGREVISION=   1
+DISTNAME=      lean4-4.32.2
 CATEGORIES=    math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=leanprover/}
 GITHUB_TAG=    v${PKGVERSION_NOREV}

Index: pkgsrc/math/lean4/distinfo
diff -u pkgsrc/math/lean4/distinfo:1.4 pkgsrc/math/lean4/distinfo:1.5
--- pkgsrc/math/lean4/distinfo:1.4      Sat Jul 25 11:24:52 2026
+++ pkgsrc/math/lean4/distinfo  Mon Aug  3 15:03:26 2026
@@ -1,8 +1,8 @@
-$NetBSD: distinfo,v 1.4 2026/07/25 11:24:52 wiz Exp $
+$NetBSD: distinfo,v 1.5 2026/08/03 15:03:26 wiz Exp $
 
-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
+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
 SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
 SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
 SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9