search

alexf91 / lean4-ctypes

FFI for Lean 4
Apache License 2.0
3 stars 0 forks source link

Improve build system #5

Open alexf91 opened 8 months ago

alexf91 commented 8 months ago

The lakefile.lean currently links against hardcoded system libraries. This works fine for examples and tests, but only when they are executed with lake exe <executable>.

Libraries depending on CTypes also require that the same libraries are set in the project as well. This should be inherited from CTypes.

Output of ldd build/bin/tests:

linux-vdso.so.1 (0x00007ffd7a3db000)
libffi.so.8 => /usr/lib/libffi.so.8 (0x00007f6ddf9ba000)
libc++.so.1 => /usr/lib/libc++.so.1 (0x00007f6ddc6b1000)
libc++abi.so.1 => /usr/lib/libc++abi.so.1 (0x00007f6ddc66e000)
libc.so.6 => /usr/lib/libc.so.6 (0x00007f6ddc48c000)
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007f6ddc200000)
libunwind.so.8 => /usr/lib/libunwind.so.8 (0x00007f6ddf9a0000)
libm.so.6 => /usr/lib/libm.so.6 (0x00007f6ddc113000)
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007f6ddc0ee000)
/lib64/ld-linux-x86-64.so.2 => /usr/lib64/ld-linux-x86-64.so.2 (0x00007f6ddf9c7000)
liblzma.so.5 => /usr/lib/liblzma.so.5 (0x00007f6ddc0bb000)

Output of lake env ldd build/bin/tests:

linux-vdso.so.1 (0x00007ffdfafc4000)
libffi.so.8 => /usr/lib/libffi.so.8 (0x00007fc7d15b0000)
libc++.so.1 => /home/alex/.elan/toolchains/leanprover--lean4---nightly-2023-10-31/lib/libc++.so.1 (0x00007fc7ce306000)
libc++abi.so.1 => /home/alex/.elan/toolchains/leanprover--lean4---nightly-2023-10-31/lib/libc++abi.so.1 (0x00007fc7ce2c3000)
libc.so.6 => /usr/lib/libc.so.6 (0x00007fc7ce0e1000)
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007fc7cde00000)
libunwind.so.8 => /usr/lib/libunwind.so.8 (0x00007fc7d1594000)
libm.so.6 => /usr/lib/libm.so.6 (0x00007fc7cdd13000)
libpthread.so.0 => /usr/lib/libpthread.so.0 (0x00007fc7d158f000)
librt.so.1 => /usr/lib/librt.so.1 (0x00007fc7d158a000)
libatomic.so.1 => /home/alex/.elan/toolchains/leanprover--lean4---nightly-2023-10-31/lib/libatomic.so.1 (0x00007fc7ce0d7000)
libunwind.so.1 => /home/alex/.elan/toolchains/leanprover--lean4---nightly-2023-10-31/lib/libunwind.so.1 (0x00007fc7ce0c7000)
libdl.so.2 => /usr/lib/libdl.so.2 (0x00007fc7ce0c2000)
/lib64/ld-linux-x86-64.so.2 => /usr/lib64/ld-linux-x86-64.so.2 (0x00007fc7d1606000)
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007fc7ce09d000)
liblzma.so.5 => /usr/lib/liblzma.so.5 (0x00007fc7cdce0000)
alexf91 commented 7 months ago

Some progress: Building everything with the system's clang++ seems to work, for both 15 and 16.

LEAN_CC=clang++ lake build tests

This results in a lot of warnings, because we can't set a separate compiler for C and C++ files:

[4/10] Compiling CTypes.Core.Basic
stderr:
clang-16: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]