changes to lake and FFI

Stream: lean4

[Tomas Skrivan]

With recent changes to lake I'm unable to get my FFI setup working again.

To demonstrate the problem I have set up a simple project which has:

FFI/Basic.lean

def hello := "world"

FFI/Compiled.lean

@[extern "print_usize"]
opaque printUSize (n : USize) : IO Unit

FFI.lean

import FFI.Basic
import FFI.Compiled

Main.lean

import FFI

def main : IO Unit := do
  IO.println s!"Hello, {hello}!"
  printUSize 42

#eval main

lakefile.lean (inspired by lake ffi example)

lakefile.lean

import Lake
open System Lake DSL

package ffi where

input_file ffi.c where
  path := "c" / "ffi.c"
  text := true

target ffi.o pkg : FilePath := do
  let srcJob ← ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
  buildO oFile srcJob weakArgs #["-fPIC"] "cc"

target libleanffi pkg : FilePath := do
  let ffiO ← ffi.o.fetch
  let name := nameToStaticLib "leanffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

lean_lib FFI where
  roots := #[`FFI]
  precompileModules := true
  moreLinkObjs := #[libleanffi]

@[default_target]
lean_exe test where
  root := `Main

I have few issues I do not know how to resolve:

1. lake build has no problem evaluating #eval main but infoview in VS Code and Emacs hangs on it.
2. How can I change the setup such that FFI/Basic.lean is not compiled but FFI/Compiled.lean is compiled? The reason for doing this is that FFI/Basic.lean imports large part of mathlib which I do not want to compile.

Previously I just replaced

lean_lib FFI where
  roots := #[`FFI]
  precompileModules := true
  moreLinkObjs := #[libleanffi]

with

lean_lib FFI

lean_lib FFICompiled where
  roots := #[`FFI.Compiled]
  precompileModules := true
  moreLinkObjs := #[libleanffi]

but now this fails with

info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading plugin, initializer not found 'initialize_FFICompiled'
error: Lean exited with code 134
Some required builds logged failures:
- FFI

[Kim Morrison]

@Mac Malone

[Mac Malone]

@Tomas Skrivan FFICompiled should be

lean_lib FFI.Compiled where
  precompileModules := true
  moreLinkObjs := #[libleanffi]

[Tomas Skrivan]

What if I have 20 lean files I want to compile? Do I have to make one lean_lib for each?

[Tomas Skrivan]

Why is the name of lean_lib important? It didn't use to be. The files to compile were specified through the roots field.

[Tomas Skrivan]

Ok, I can turn FFI.Compiled.lean into a folder and all the files in it will be compiled. I'm still confused about the lean_lib naming and the roots field.

[Mac Malone]

Tomas Skrivan said:

What if I have 20 lean files I want to compile? Do I have to make one lean_lib for each?

The standard approach would to have a single precompiled root module which imports the 20.

Tomas Skrivan said:

Why is the name of lean_lib important? It didn't use to be. The files to compile were specified through the roots field.

Lake now tries to load the library as plugin if it can (i.e., via lean --plugin instead of lean --load-dynlib). This requires the root and the library to be named in a speciifc way and Lake's heuristic for detecting this is currently inaccurate. lean4#8528 will fix this.

[Tomas Skrivan]

Why does the order of lean_lib matter?

This works:

lean_lib FFI

lean_lib FFI.Compiled where
  precompileModules := true
  moreLinkObjs := #[libleanffi]

but this does not:

lean_lib FFI.Compiled where
  precompileModules := true
  moreLinkObjs := #[libleanffi]

lean_lib FFI

Why is that? I find it quite confusing as there has to be some dependency between the two that is not explicitly written.

[Mac Malone]

Tomas Skrivan said:

Why does the order of lean_lib matter?

Later libraries shadow earlier ones. Both FFI and FFI.Compiled match FFI.Compiled. That is, they overlap -- FFI matches any module FFI.* and FFI.Compiled matches any module FFI.Compiled.*. If FFI.Compiled comes later, its configuration is used; otherwise, the configuration of FFI is used.

[Tomas Skrivan]

Thanks! I have it working now on v4.19.0

[Tomas Skrivan]

However, not I'm trying to bump to v4.20.0-rc5 and I'm getting bunch of undefined reference errors. For examples:

ld.lld: error: undefined symbol: l_Array_emptyWithCapacity
>>> referenced by Congr.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Congr.c.o.export:(initialize_Batteries_Tactic_Congr)

full error message

info: stderr:
ld.lld: error: undefined symbol: l_Array_emptyWithCapacity
>>> referenced by Congr.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Congr.c.o.export:(initialize_Batteries_Tactic_Congr)
>>> referenced by Util.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Util.c.o.export:(initialize_ProofWidgets_Util)
>>> referenced by Compat.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Compat.c.o.export:(initialize_ProofWidgets_Compat)

ld.lld: error: undefined symbol: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextEdit____x40_Lean_Data_Lsp_Basic___hyg_1976____spec__2
>>> referenced by MakeEditLink.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/MakeEditLink.c.o.export:(l___private_ProofWidgets_Component_MakeEditLink_0__ProofWidgets_fromJsonMakeEditLinkProps____x40_ProofWidgets_Component_MakeEditLink___hyg_147_)
>>> did you mean: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextEdit____x40_Lean_Data_Lsp_Basic___hyg_1976____spec__1
>>> defined in: /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib/lean/libLean.a(Basic.o)

ld.lld: error: undefined symbol: l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_2014____spec__2
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l___private_ProofWidgets_Component_Basic_0__ProofWidgets_fromJsonRpcEncodablePacket____x40_ProofWidgets_Component_Basic___hyg_69_)
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l___private_ProofWidgets_Component_Basic_0__ProofWidgets_fromJsonRpcEncodablePacket____x40_ProofWidgets_Component_Basic___hyg_329_)
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l___private_ProofWidgets_Component_Basic_0__ProofWidgets_fromJsonRpcEncodablePacket____x40_ProofWidgets_Component_Basic___hyg_645_)

ld.lld: error: undefined symbol: l_List_flatMapTR_go___at___private_Lean_Util_Paths_0__Lean_toJsonLeanPaths____x40_Lean_Util_Paths___hyg_55____spec__2
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l___private_ProofWidgets_Component_Basic_0__ProofWidgets_toJsonRpcEncodablePacket____x40_ProofWidgets_Component_Basic___hyg_152_)
>>> referenced by MakeEditLink.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/MakeEditLink.c.o.export:(l___private_ProofWidgets_Component_MakeEditLink_0__ProofWidgets_toJsonMakeEditLinkProps____x40_ProofWidgets_Component_MakeEditLink___hyg_292_)
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l___private_ProofWidgets_Component_Basic_0__ProofWidgets_toJsonRpcEncodablePacket____x40_ProofWidgets_Component_Basic___hyg_412_)
>>> referenced 2 more times

ld.lld: error: undefined symbol: l___private_Lean_Widget_TaggedText_0__Lean_Widget_fromJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_407____at_Lean_Widget_TaggedText_instRpcEncodable___spec__5
>>> referenced by Basic.c
>>>               /home/tskrivan/Documents/LeanBLAS/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c.o.export:(l_ProofWidgets_instRpcEncodableInteractiveCodeProps_dec____x40_ProofWidgets_Component_Basic___hyg_44_)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/clang' exited with code 1
Some required builds logged failures:
- CBLASLevelOneTest
error: build failed

Right now I do not know how to minimize it. I'm updating LeanBLAS, this v4.19.0 commit works but this v4.20.0-rc5 commit does not.

[Tomas Skrivan]

Interestingly it fails with a different error on Linux during CI

info: stderr:
ld.lld: error: undefined symbol: __libc_csu_fini
>>> referenced by start.S:101 (../sysdeps/x86_64/start.S:101)
>>>               /home/runner/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib/Scrt1.o:(_start)

ld.lld: error: undefined symbol: __libc_csu_init
>>> referenced by start.S:102 (../sysdeps/x86_64/start.S:102)
>>>               /home/runner/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/lib/Scrt1.o:(_start)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/runner/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/clang' exited with code 1
Some required builds logged failures:
- CBLASLevelOneTest
error: build failed

and on MacOS it passes

[Tomas Skrivan]

Now I'm updating SciLean that uses LeanBLAS and I'm getting an odd error

✖ [1847/1856] Running LeanBLAS.FFI:shared
error: type mismtach in target 'libleanblasc': expected 'filepath', got unknown

where libleanblasc is the target in LeanBLAS that build the C library

target libleanblasc pkg : FilePath := do
    ...
    buildStaticLib (pkg.sharedLibDir / name) (oFiles)

[Tomas Skrivan]

This makes me wonder if there is an issue when having a project with FFI as a dependency.

I try to reproduce it with the simple ffi project.

[Mac Malone]

The first set of errors seems like it may be an issue caused by an incompatibility with the new LLVM toolchain used in Lean v4.20.0. LLVM has been upgraded from 15 to 19. On your local machine, it might be worth clobbering the .lake directory and seeing if that changes the errors to mirror the CI (some aspect of the version update may have not been caught by Lake).

The 'filepath' issue, on the other hand, may more likely be a Lake problem.

[Tomas Skrivan]

I can't reproduce the filepath problem with the minimal example but with LeanBLAS

Steps to reproduce on Ubuntu:

$ sudo apt-get install libopenblas-dev
$ mkdir leanblasdep; cd leanblasdep
$ lake init leanblasdep .lean

replace lakefile.lean with:

import Lake
open Lake DSL

package "leanblasdep" where
  version := v!"0.1.0"
  moreLinkArgs := #["-L/usr/lib/x86_64-linux-gnu/", "-lblas", "-lm"]

lean_lib «Leanblasdep» where

@[default_target]
lean_exe "leanblasdep" where
  root := `Main

require leanblas from git "https://github.com/lecopivo/LeanBLAS" @ "v4.20.1"

Now running lake build LeanBLAS.FFI:static produces this error:

$ lake build LeanBLAS.FFI:static
✖ [13/14] Building leanblas/libleanblasc
trace: .> gcc -c -o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/leveltwoext.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/c/leveltwoext.c -I /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/include -DNDEBUG -O3 -fPIC
trace: .> gcc -c -o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/util.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/c/util.c -I /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/include -DNDEBUG -O3 -fPIC
trace: .> gcc -c -o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/levelone.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/c/levelone.c -I /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/include -DNDEBUG -O3 -fPIC
trace: .> gcc -c -o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/leveltwo.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/c/leveltwo.c -I /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/include -DNDEBUG -O3 -fPIC
trace: .> /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/llvm-ar rcs /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/lib/libleanblasc.a /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/leveltwoext.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/util.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/levelone.o /home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/c/leveltwo.o
info: stderr:
/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/llvm-ar: error: unable to load '/home/tskrivan/doodle/lean/leanblasdep/.lake/packages/leanblas/.lake/build/lib/libleanblasc.a': file too small to be an archive
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/llvm-ar' exited with code 1
✖ [14/14] Running LeanBLAS.FFI:static
error: type mismtach in target 'libleanblasc': expected 'filepath', got unknown
Some required builds logged failures:
- leanblas/libleanblasc
- LeanBLAS.FFI:static
error: build failed

[Tomas Skrivan]

I can reproduce with the SimpleFFI project now.

mkdir SimpleFFIDep; cd SimpleFFIDep
lake init simpleffidep .lean
echo 'require ffi from git "https://github.com/lecopivo/SimpleFFI" @ "alt"' >> lakefile.lean
{ echo 'import FFI'; cat Main.lean; } > tmp.lean && mv tmp.lean Main.lean
lake update
lake build

which ends with

$ lake build
✖ [13/23] Running FFI.Compiled:shared
error: type mismtach in target 'libleanffi': expected 'filepath', got unknown
✖ [23/23] Running simpleffidep
error: type mismtach in target 'libleanffi': expected 'filepath', got unknown
Some required builds logged failures:
- FFI.Compiled:shared
- simpleffidep
error: build failed

[Tomas Skrivan]

It has to do something with building the *.c files with

code

input_file ffi.c where
  path := "c" / "ffi.c"
  text := true

target ffi.o pkg : FilePath := do
  let srcJob ← ffi.c.fetch
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
  buildO oFile srcJob weakArgs #["-fPIC"] "cc"

target libleanffi pkg : FilePath := do
  let ffiO ← ffi.o.fetch
  let name := nameToStaticLib "leanffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

vs

code

target libleanffi pkg : FilePath := do
  pkg.afterBuildCacheAsync do
    let mut oFiles : Array (Job FilePath) := #[]
    for file in (← (pkg.dir / "c").readDir) do
      if file.path.extension == some "c" then
        let oFile := pkg.buildDir / "c" / (file.fileName.stripSuffix ".c" ++ ".o")
        let srcJob ← inputTextFile file.path
        let weakArgs := #["-I", (← getLeanIncludeDir).toString]
        oFiles := oFiles.push (← buildO oFile srcJob weakArgs (#["-DNDEBUG", "-O3", "-fPIC"]) "gcc" getLeanTrace)
    let name := nameToStaticLib "leanffi"

    buildStaticLib (pkg.sharedLibDir / name) (oFiles)

The first version works, the second does not. It is not clear to me how to generalize the first approach if I want to just compile all the *.c files in the c/ directory.

[Tomas Skrivan]

Ahh, it has something to do with pkg.afterBuildCacheAsync. It is leftover code when I was experimenting with github releases. Removing it solves the problem with filepath

[Tomas Skrivan]

However, I still have the problem executing ffi functions in the editor.

mwe:

git clone git@github.com:lecopivo/SimpleFFI.git
cd SimpleFFI
lake update
lake build

Open Main.lean in VS Code and the orange line does not go away for me. Same happens in emacs.

[Arthur Paulino]

Did anything change regarding the memory layout of Lean objects from 4.21 to 4.23? Like the ordering of constructor pointers or anything else?

Our FFI glue code is now segfaulting. We're trying to minimize the problem but any clue would help. Thanks a lot!

[Arthur Paulino]

(deleted)