Issue with linking

Stream: lean4

[z battleman]

I'm currently working on a project that uses openBLAS for optimized computation. I have a matrix multiplication function which is implented with cblas, and a matrix exponentiation function which is implemented with cblas as well. If its relevant, in Lean, the exponentiation function is defined by recursive calls to multiplication (but it's extern'ed anyway) When I try to compile, I get

/home/z/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean: symbol lookup error: ./build/lib/libleanffi.so: undefined symbol: cblas_dgemm

but what's strange is that this only occurs when I use the exponentiation function. When I compile with just the multiplication function (which also uses cblas_dgemm I have no issues.

If it helps, here is the exponentiation code

@[extern "mathMatrix_exp"]
def exp (M : mathMatrix n n) : (e : Nat) -> mathMatrix n n
| 0 => mathMatrix.id n
| Nat.succ m => M.multiply_MM (exp M m)

as well as the underlying FFI code

lean_object* mathMatrix_mul_MM(lean_object* m_, lean_object* n_, lean_object* k_, lean_object* M1_, lean_object* M2_) {
    mathMatrix* M1 = mathMatrix_unboxer(M1_);
    mathMatrix* M2 = mathMatrix_unboxer(M2_);
    uint32_t m = M1->rows;
    uint32_t n = M1->cols;
    uint32_t k = M2->cols;

    assert(n == M2->rows);

    mathMatrix* out_struct = mathMatrix_alloc(m, k);

    double* result = malloc(sizeof(double)*m*k);
    for (size_t i = 0; i < m*k; i++) {
        result[i] = 0.0;
    }

    cblas_dgemm(CblasRowMajor, CblasNoTrans, CblasNoTrans,
                m, k, n, 1.0, M1->data, n, M2->data, k, 0.0, result, k);

    out_struct->data = result;

    return mathMatrix_boxer(out_struct);
}

lean_object* mathMatrix_exp (lean_object* n_, lean_object* M_, lean_object* e_) {
    mathMatrix* M = mathMatrix_unboxer(M_);
    uint32_t e = lean_unbox_uint32(e_);
    uint32_t n = M->rows;
    mathMatrix* result = mathMatrix_struct_id(n);

    for (size_t i = 0; i < e; i++) {
        cblas_dgemm(CblasRowMajor, CblasNoTrans, CblasNoTrans,
                    n, n, n, 1.0, result->data, n, M->data, n, 0.0, result->data, n);
    }

    return mathMatrix_boxer(result);
}

Edit: The issue fixed when I removed precompileModules = true from my lakefile. Though ideally it would still be able to have it enabled

[Sebastian Ullrich]

Is your library properly linked against cblas (lld build/lib/libleanffi.so should list it)?

[z battleman]

There are a couple of functions which are not properly linked

ld: warning: cannot find entry symbol _start; not setting start address
ld: build/lib/libleanffi.so: undefined reference to `lean_big_usize_to_nat'
ld: build/lib/libleanffi.so: undefined reference to `l_Fin_ofNat'
ld: build/lib/libleanffi.so: undefined reference to `cblas_dgemv'
ld: build/lib/libleanffi.so: undefined reference to `lean_register_external_class'
ld: build/lib/libleanffi.so: undefined reference to `lean_mk_string'
ld: build/lib/libleanffi.so: undefined reference to `lean_apply_1'
ld: build/lib/libleanffi.so: undefined reference to `cblas_dgemm'
ld: build/lib/libleanffi.so: undefined reference to `lean_inc_ref_cold'
ld: build/lib/libleanffi.so: undefined reference to `lean_mk_io_user_error'
ld: build/lib/libleanffi.so: undefined reference to `lean_notify_assert'
ld: build/lib/libleanffi.so: undefined reference to `lean_alloc_small'

Admittedly though, I'm not sure how to fix it as I think I am correctly linking as shown here in my lakefile

package LeanAlg {
  -- customize layout
  --srcDir := "LeanAlg"
  --libRoots := #[`mathVec, `mathMatrix]
  -- specify the lib as an additional target
  --moreLibTargets := #[cLibTarget __dir__]
  moreLinkArgs := #["-L", "./third_party/OpenBLASLib/lib",
                    "-lopenblas",
                    "-Wl,-R./third_party/OpenBLASLib/lib"]

  --precompileModules := true
  packagesDir := "third_party"
}

def pkgDir := __dir__
def cSrcDir := pkgDir / "c"
def cBuildDir := pkgDir / _package.buildDir / "c"
def libBuildDir := pkgDir / _package.buildDir / "lib"

def oTarget (filename : String) : FileTarget :=
  let oFile := cBuildDir / s!"{filename}.o"
  let srcTarget := inputFileTarget <| cSrcDir / s!"{filename}.c"
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", "third_party/OpenBLASLib/include", "-fPIC",
                             "-I", (← getLeanIncludeDir).toString]

extern_lib cLib :=
  let libFile := libBuildDir / nameToStaticLib "leanffi"
  staticLibTarget libFile #[oTarget "./utils/utils", oTarget "mathVec_ffi", oTarget "mathMatrix_ffi"]

[Mac]

I think this is a bug in Lake due to the fact that I don't pass additional linking arguments to the linker when compiling a shared library from a static library here: https://github.com/leanprover/lake/blob/dcf8e1fc406acfd4dbbfd691f4ecf76966fae407/Lake/Build/Targets.lean#L84-L92

[zbatt]

Mac said:

I think this is a bug in Lake due to the fact that I don't pass additional linking arguments to the linker when compiling a shared library from a static library here: https://github.com/leanprover/lake/blob/dcf8e1fc406acfd4dbbfd691f4ecf76966fae407/Lake/Build/Targets.lean#L84-L92

What I think is really interesting is that it seems to only occur with some functions? For example if I just use the multiplication function (which also uses cblas_dgemm it compiles without complaining. Do you have a guess as to why that could be?

[Mac]

@zbatt I think I would need to look at the source of libleanffi to make any guesses as to why that would be the case.

[zbatt]

Mac said:

zbatt I think I would need to look at the source of libleanffi to make any guesses as to why that would be the case.

If it's helpful for debugging Lake, I would be more than happy to share the repository, but obviously you don't have to look at it for my bugs haha

[James Gallicchio]

(I'm also just interested in taking a gander :eyes:)

[Mac]

zbatt said:

If it's helpful for debugging Lake

I think it could be.

[zbatt]

Mac said:

zbatt said:

If it's helpful for debugging Lake

I think it could be.

https://github.com/zaxioms/LeanAlg
Here you go :D