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.
cpufreq_dt: communicate full voltage range to regulators
In the last commit, fdtbus_regulator_set_voltage got changed to accept the voltage as a target, min, max triple from a min, max pair. This commit switched the cpufreq code over to sending the full voltage triple to regulators if it is available in the device tree.
This fixes PR 60671
fdtbus_regulator_set_voltage_triple: support target/min/max
Some dt-bindings specify voltages as target/min/max, while the NetBSD fdt subsystem only supported min/max.
This PR introduces fdtbus_regulator_set_voltage_triple that tries to set the voltage to an optimal value before falling back to the full range.
See PR 60671
Import math/HiGHS from wip, update to version 1.15.1.
HiGHS is a high performance serial and parallel solver for large
scale sparse linear programming (LP) problems of the form:
Minimize c^Tx subject to L <= Ax <= U; l <= x <= u
rumdl: update to 0.3.0.
Changed
2.4–4.7× faster rumdl fmt than 0.2.79 on frozen documentation
snapshots: Cargo (99 files) 4.7×, MkDocs Material (85 files) 2.6×, and
Ruff (16 files) 2.4×. Reusing parsed Markdown and shared source analysis
reduces repeated work. Speedups compare median elapsed times from 31 paired
runs after five warmups on Apple M6: ordinary Rust 1.96.0 release builds,
default threads, warm filesystem cache, and --no-config --no-cache --silent
(--flavor=standard for Cargo/Ruff, --flavor=mkdocs for MkDocs Material).
Output includes the correctness fixes listed below and can differ from 0.2.79.
Code block tools are supported and remain opt-in. Missing tags, missing
active-mode tools and invocations with no tools checked are ignored by default.
An omitted unknown-tag policy inherits on-missing-language-definition,
preserving existing strict configurations. Valid internal cached checks count
as checked; applicable external tools rerun to reflect changes in their own
configuration and environment.
on-missing-language-definition = "warn" now reports uncovered languages;
[134 lines not shown]
Initial import of devel/cbmc version 6.10.0.
CBMC is a Bounded Model Checker for C and C++ programs. It supports
C89, C99, most of C11, C17, C23 and most compiler extensions provided
by gcc and Visual Studio. It also supports SystemC using Scoot. It
allows verifying array bounds (buffer overflows), pointer safety,
exceptions and user-specified assertions. Furthermore, it can check
C and C++ for consistency with other languages, such as Verilog.
The verification is performed by unwinding the loops in the program
and passing the resulting equation to a decision procedure.
ast-grep: update to 0.51.0.
0.51.0
fix(cli): use ast-grep name in project setup hint #3001
fix: replace deprecated serde_yaml with serde-saphyr #2999
fix(deps): update rust crate tree-sitter-haskell to 0.24.0 #2988
fix(cli): preserve files when update-all writes fail #2995
Revise security policy for clarity and updates a7d3f69
fix: update wasm linting ea55463
ggml: update to 0.27.0.
ggml v0.27.0 extends the backend scheduler API with user callbacks
for split weight copying and compute-buffer reallocation, and bumps
the RPC protocol to v8 to support tensor-parallel RPC servers.
Backends gained substantial new fast paths: chunked gated-delta-net
kernels on CUDA/HIP, KleidiAI SME2 k-quant matmuls and AVX2 Q2_0
dot products on CPU, L2-aware coopmat2 matmul scheduling and bf16
activations on Vulkan, reordered-layout MoE kernels (MXFP4, IQ3,
Q5_K, grouped XMX GEMM) on SYCL, dp4a MoE GEMMs on OpenCL, tensor-API
and wider-head-dim flash attention on Metal, and a DMA/HVX copy
overhaul with new pooling and 3D im2col ops on Hexagon. Correctness
work concentrated on non-contiguous and strided views, grid/workgroup
size limits, out-of-bounds accesses, and well-defined mul_mat_id
behavior for duplicate expert ids.
