From: Kirill A. Korinsky <kirill@korins.ky>
Subject: Re: Bring math/mathlib and math/lean to 4.35.0-rc3
To: Yozo TODA <yozo@v007.vaio.ne.jp>
Cc: ports@openbsd.org
Date: Mon, 12 Oct 2026 02:22:28 +0200

On Sat, 10 Oct 2026 08:33:30 +0200,
Yozo TODA <yozo@v007.vaio.ne.jp> wrote:
> 
> > I'd like to switch math/lean to 4 and bring math/mathlib as well.
> > I've attached gziped diff and a few required dependencies.
> 
> packaging on my amd64 machine, I noticed the following:
> (sorry just comments only, you may already updating...)
> 
> (1)
> /usr/local/LICENSE
> /usr/local/LICENSES
> 
> should be installed to /usr/local/share/lean/ ?
> (yes, of course ${LOCALBASE}/share/lean/ )
>

Thanks, good catch I had missed this one.

> (2)
> /usr/local/src/lean/ should be moved to
> /usr/local/share/lean/ ?
> (${LOCALBASE}/share/lean/)
>

I thought about that, but it makes things more complicated plus
lang/hare/hare already installs into /usr/local/src/hare

> (3)
> core dump on my environment, but I found that it needs more memory
> than my standard environment for "staff".
> should be commented on DESCR or README ?
> 
>   $ ls -l *core
>   ls: *core: No such file or directory
>   $ ulimit -d
>   1572864
>   $ lean --print-prefix
>   libc++abi: terminating due to uncaught exception of type lean::exception: failed to create thread: Cannot allocate memory
>   Abort trap (core dumped) 
>   $ (ulimit -d 3500000 && lean --print-prefix )
>   /usr/local
>

Yeah, Lean needs memory and by default it allocates 1Gb per thread. You can
control it via LEAN_STACK_SIZE_KB.

I thought to add something into README but I haven't figured out that.

> (4)
> can we avoid "/usr/local/bin/../lib/*" and straight to "/usr/local/lib/*" ?
> 
> $ ldd /usr/local/bin/lean
> /usr/local/bin/lean:
> 	Start            End              Type  Open Ref GrpRef Name
> 	00000739ad111000 00000739ad115000 exe   2    0   0      /usr/local/bin/lean
> 	0000073c54e1a000 0000073c54f4d000 rlib  0    5   0      /usr/lib/libc++.so.13.0
> 	0000073c88634000 0000073c88683000 rlib  0    6   0      /usr/lib/libc++abi.so.10.0
> 	0000073c27626000 0000073c27633000 rlib  0    6   0      /usr/lib/libpthread.so.28.1
> 	0000073c8090f000 0000073c80913000 rlib  0    1   0      /usr/local/bin/../lib/lean/libInit_shared.so
> 	0000073c290f1000 0000073c290f5000 rlib  0    1   0      /usr/local/bin/../lib/lean/libleanshared_2.so
> 	0000073c8ce71000 0000073c8ce75000 rlib  0    1   0      /usr/local/bin/../lib/lean/libleanshared_1.so
> 	0000073c1720d000 0000073c221d0000 rlib  0    1   0      /usr/local/bin/../lib/lean/libleanshared.so
> 	0000073c84280000 0000073c84306000 rlib  0    5   0      /usr/local/bin/../lib/libgmp.so.11.1
> 	0000073c957b0000 0000073c957e5000 rlib  0    5   0      /usr/local/bin/../lib/libuv.so.5.3
> 	0000073bce8d9000 0000073bce949000 rlib  0    5   0      /usr/lib/libssl.so.60.2
> 	0000073bcb76d000 0000073bcb9b7000 rlib  0    6   0      /usr/lib/libcrypto.so.57.2
> 	0000073bbaa17000 0000073bbaa48000 rlib  0    5   0      /usr/lib/libm.so.10.1
> 	0000073c4faa1000 0000073c4fbaa000 rlib  0    1   0      /usr/lib/libc.so.104.0
> 	0000073c2f0a1000 0000073c2f0a1000 ld.so 0    1   0      /usr/libexec/ld.so
>

Thanks, missed and fixed.

> 
> (5)
> the binary links to the system LibreSSL libraries
> (/usr/lib/libssl.so*  and /usr/lib/crypto.so.*).
> I believe it should be adjusted to link to openssl port.
> the output log of my compilation shows the configuration finding the openssl successfully,
> but the linking phase used LibreSSL system libraries.
>

Any reason why? System's LibreSSL is standard and using OpenSSL should have
a reason which I probably missed.

Thus, here an updated diff and tgz, this time it is 4.35.0-rc4.

I'm waiting till the final release for 4.35.0.

-- 
wbr, Kirill