reverse ffi errors

Stream: Program verification

[Cody Roux]

Hi all, I'm getting a fiddly error in my reverse-ffi test example:

/usr/bin/ld: lean/.lake/build/lib/libControl.so: undefined reference to `initialize_Mathlib_Data_Complex_Trigonometric'
/usr/bin/ld: lean/.lake/build/lib/libControl.so: undefined reference to `initialize_Mathlib_Analysis_SpecialFunctions_Trigonometric_Basic'

For info, here's my messy makefile:

LAKE ?= lake

lake:
    $(LAKE) --dir=lean build

OUT_DIR = out
LEAN_SYSROOT ?= $(shell lean --print-prefix)
LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean
LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lean/.lake/build/lib

all: pendulum
pendulum: src/pendulum.c lake
    @gcc -o $@ $< -Os -lncursesw -lm -lpthread -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lean/.lake/build/lib -lControl -lInit_shared -lleanshared_1 -lleanshared $(LINK_FLAGS)

run:
    @./pendulum

clean:
    @rm -f pendulum
    @echo "Cleaned"

It's a bit cargo-culty so please forgive me. I'm sure the headers are _somewhere_ since I compiled all of Mathlib for an hour or so while calling lake update.

[Sebastian Ullrich]

How did you build libControl.so? I think there should be a libMathlib.so somewhere in your build directory that you'll need to throw into gcc as well - perhaps iteratively with further dependencies

[Cody Roux]

I think just the lake --dir=lean build takes care of that? There's definitely a libControl.so in the build directory coming from the Control.lean in my /lean directory, but not much else, I think (I'll check again when I get home).

Are they perhaps somewhere else?

[Sebastian Ullrich]

So I assume you are using the shared facet in your lakefile to generate it? If there is "not much else" in your build directory, where is mathlib stored?

@Mac Malone Is it correct that building Control:shared should also trigger Mathlib:shared if there is any dependency? Is it the case right now that shared outputs on Unix do not automatically link (in the ldd sense) against their dependencies and if so do we have/should we open an issue about it?

[Cody Roux]

Ok well now I'm getting errors like

error: Batteries/Data/Nat/Gcd.lean:21:17: 'Nat.Coprime' has already been declared

So I'm clearly doing something wrong :man_facepalming:

FWIW, here's the lakefile:

import Lake
open System Lake DSL

package control

require "leanprover-community" / "mathlib"

@[default_target]
lean_lib Control where
  defaultFacets := #[LeanLib.sharedFacet]

Which I just stole from https://github.com/leanprover/lean4/blob/master/src/lake/examples/reverse-ffi/lib/lakefile.lean

[Sebastian Ullrich]

It looks like you are using a different version of Lean from batteries/mathlib. Make sure the lean-toolchains coincide.

[Cody Roux]

How do I do that? Sorry my questions are so elementary; I really am not grokking the build system yet.

[Sebastian Ullrich]

Usually lake new math would do this for you but in this context I think you can run lake update to trigger an automatic toolchain sync

[Mac Malone]

Sebastian Ullrich said:

Mac Malone Is it correct that building Control:shared should also trigger Mathlib:shared if there is any dependency?

Yes.

Sebastian Ullrich said:

Is it the case right now that shared outputs on Unix do not automatically link (in the ldd sense) against their dependencies and if so do we have/should we open an issue about it?

Shared ouptuts do not link against their dependencies (on non-Windows). I do not believe there is an issue about it. It is also not clear to me whether this would be a good thing to do.

[Cody Roux]

I'll try lake update as soon as I get back home (but I thought I'd done this).

[Cody Roux]

Ah it works from within the directory, but not above, which makes sense. I'm back to the undefined reference error.

And I now find the libMathlib.so files! I guess I just need to add something like lean/.lake/packages/**/.lake/build/lib to the LINK_FLAGS?

[Sebastian Ullrich]

I think you can just pass all the .sos directly to gcc