With lean4 built from source on Linux /usr/lib/libuv.so and /usr/lib/libgmp.so are being passing directly to be linked by gcc (rather than -luv and -lgmp etc).
This causes many warnings from gcc: see below.
I am not good with cmake and so far failed to come up with a viable patch for this:
the current cmake (as of 4.13/4.14) in src/cmake/Modules/ leads to GMP_LIBRARIES=/usr/lib/libgmp.so
and LIBUV_LIBRARIES=/usr/lib/libuv.so on Linux which is not desired (at least for gcc).
I suppose I could also try clang - is that recommended for Linux builds?
I tried to use the cmake PkgConfig module macros but failed to get the right kind of output (boggle).
Note pkgconf is a compatible replacement of pkg-config: they are mostly equivalent.
It doesn't matter whether pkgconf or pkg-config is used.
For reference on Fedora Linux:
$ pkgconf --libs libuv
-luv -lpthread -ldl -lrt
Whether all those are strictly needed I dunno, but they are listed.
But this is what LIBUV_LIBRARIES should equal or at the very least -luv.
Context
[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]
Steps to Reproduce
Expected behavior:
No unused linker warnings
Actual behavior:
$ lake build
:
ℹ [9/27] Replayed Curl.Errors:c.o
info: stderr:
gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done
ℹ [10/27] Replayed Curl.CurlM:c.o
info: stderr:
gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done
ℹ [11/27] Replayed Curl.HeaderData:c.o
info: stderr:
gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done
ℹ [17/27] Replayed Main:c.o
info: stderr:
gcc: warning: /usr/lib64/libuv.so: linker input file unused because linking not done
:
(This is with patched in -lgmp, so normally there would be double the number of warnings.)
Versions
$ lean --version
Lean (version 4.13.0, Release)
on Fedora Linux
Additional Information
I am currently working around it by directly patching pkgconf --libs output into src/cmake/Modules/Find*.cmake (and for stage0 of course).
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
With lean4 built from source on Linux
/usr/lib/libuv.soand/usr/lib/libgmp.soare being passing directly to be linked by gcc (rather than-luvand-lgmpetc).This causes many warnings from gcc: see below.
I am not good with cmake and so far failed to come up with a viable patch for this: the current cmake (as of 4.13/4.14) in
src/cmake/Modules/leads toGMP_LIBRARIES=/usr/lib/libgmp.soandLIBUV_LIBRARIES=/usr/lib/libuv.soon Linux which is not desired (at least for gcc). I suppose I could also try clang - is that recommended for Linux builds? I tried to use the cmakePkgConfigmodule macros but failed to get the right kind of output (boggle).Note pkgconf is a compatible replacement of pkg-config: they are mostly equivalent. It doesn't matter whether pkgconf or pkg-config is used.
For reference on Fedora Linux:
Whether all those are strictly needed I dunno, but they are listed. But this is what
LIBUV_LIBRARIESshould equal or at the very least-luv.Context
[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]
Steps to Reproduce
Expected behavior:
No unused linker warnings
Actual behavior:
(This is with patched in -lgmp, so normally there would be double the number of warnings.)
Versions
on Fedora Linux
Additional Information
I am currently working around it by directly patching pkgconf --libs output into
src/cmake/Modules/Find*.cmake(and for stage0 of course).See https://github.com/fedora-haskell/lean4/commit/c88870c2df115c294b80e11f15b8dfc24877b4c8
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.