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

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

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

Log message:
lean4: update to 4.33.1.

This patch release contains runtime and kernel fixes.

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

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.

Log message:
lean4: another patch filed upstream

Log message:
lean4: fix typo