Download raw body.
Bring math/mathlib and math/lean to 4.35.0-rc3
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
Bring math/mathlib and math/lean to 4.35.0-rc3