On Wed, Oct 14, 2026 at 04:06:51AM +0200, Kirill A. Korinsky wrote:
> ports@,
> 
> I'd like to update math/lean instead of dropping it as was suggested here:
> https://marc.info/?l=openbsd-ports&m=178990539056610&w=2
> 
> So, here an update of math/lean to 4.35.0 plus its depds

lean needs a BDEP on shells/bash.

archivers/leangz and math/cadical have pretty shitty DESCR, but that's
not really your fault: leangz's authors clearly don't like text and
comments at all, and math/cadical isn't super useful for someone who
just wants to know what it is...

Anyway, these two deps and the update are ok tb

(I dropped lean maintainership in the interim so the diff for math/lean
does not apply as it is).

> new port math/mathlib.

I would like some other porters to consider and approve this monster.
It takes forever to build (it's also irritating that the upper bound
keeps growing and growing as the hours pass).

Moreover, I find the do-install shell concoction pretty gross.

I considered a port for mathlib in the past and did not send that out
just because how large it already was back then.