math/lean4 4.33.1nb1 NetBSD

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.

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 …

This was done between fork + exec. This reduces lake hangs due to malloc state inherited by the child. Bump PKGREVISION.

This patch release contains runtime and kernel fixes.

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.