On Thu, 15 Oct 2026 10:55:55 +0200,
Theo Buehler <tb@theobuehler.org> wrote:
> 
> 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).
>

Thanks, applied locally and resolved conflict.

> > 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.
> 

Yeah, do-install is ugly and I not sure how to make it cleaner.

Anyway, regarding the size: it is large but without it modern lean is
somehow useless. Almost everything inside mathlib.

-- 
wbr, Kirill