Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cmake should make use of pkgconfig to detect shared libuv and gmp libs correctly #6183

Closed
1 task done
juhp opened this issue Nov 23, 2024 · 1 comment
Closed
1 task done
Labels
bug Something isn't working

Comments

@juhp
Copy link
Contributor

juhp commented Nov 23, 2024

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

See fedora-haskell/lean4@c88870c

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

@juhp juhp added the bug Something isn't working label Nov 23, 2024
@juhp juhp changed the title cmake should make use of pkgconf to detect shared libuv and gmp correctly cmake should make use of pkgconfig to detect shared libuv and gmp correctly Nov 23, 2024
@juhp juhp changed the title cmake should make use of pkgconfig to detect shared libuv and gmp correctly cmake should make use of pkgconfig to detect shared libuv and gmp libs correctly Nov 23, 2024
@Kha
Copy link
Member

Kha commented Dec 6, 2024

@tydeu Should be fixed with #6176 not passing LEAN_EXTRA_LINKER_FLAGS to codegen anymore?

@Kha Kha closed this as completed Dec 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants