extern static inline function

Stream: lean4

[Tomas Skrivan]

I'm a bit confused on how am I supposed to work with extern function that is static inline on C level similar to function like lean_float_array_uget.

The way it seems to work is:

Have bytearray.c with the function without static inline

#include <lean/lean.h>
LEAN_EXPORT double scilean_byte_array_uget_float(b_lean_obj_arg a, size_t i){
  return ( (double*)(lean_sarray_cptr(a)))[i];
}

and have bytearray.h with static inline

#include <lean/lean.h>
static inline double scilean_byte_array_uget_float(b_lean_obj_arg a, size_t i){
  return ( (double*)(lean_sarray_cptr(a)))[i];
}

and add moreLeancArgs := #["-include", "./C/bytearray.h"] to my project. Is this the intended way of doing this? Without the bytearray.c I get linker error complaining about undefined reference scilean_byte_array_uget_float.

[Eric Wieser]

A hacky option might be to put __attribute__((used)) on the declaration in the header (and include it in the C file), though this is GCC-only

[Tomas Skrivan]

Doesn't Lean use clang now by default?

[Eric Wieser]

You need it in the c file one way or another because of callers that go from lean via dlsym, which needs the symbol to existing in the static library

[Eric Wieser]

https://clang.llvm.org/docs/AttributeReference.html#used suggests used is in clang too

[Tomas Skrivan]

Yeah that makes sense, so current approach is likely the right one.

Eric Wieser said:

A hacky option might be to put __attribute__((used)) on the declaration in the header (and include it in the C file), though this is GCC-only

What is this supposed to solve? I don't understand what is this mean to do.

[Sebastian Ullrich]

(deleted)

[Tomas Skrivan]

Sebastian Ullrich said:

(deleted)

Not sure how to use extern c inline but this works

@[extern c inline "((double*)(lean_sarray_cptr(#1)))[#2]"]
opaque ByteArray.ugetFloat (a : @& ByteArray) (i : USize) (hi : i.toNat*8 + 7 < a.size) : Float

[Eric Wieser]

Concretely, my proposal was

// in bytearray.h
#include <lean/lean.h>
static inline double scilean_byte_array_uget_float(b_lean_obj_arg a, size_t i) __attribute__((used)) {
  return ( (double*)(lean_sarray_cptr(a)))[i];
}

// in bytearray.c
#include <lean/lean.h>
#include "bytearray.h"

[Eric Wieser]

It solves the problem of the function being written twice

[Sebastian Ullrich]

It doesn't make sense to have it in both .c and .h, I think that just shows that your header file is currently unused. There is no way currently to add new includes to the generated C files.

[Eric Wieser]

It would make sense to have it in both if it was included in generated C files, right?

[Tomas Skrivan]

The compiler flag -include has to work to include h file to generated c files. I'm getting 10x speed up in my code when I add it.

[Eric Wieser]

Is -include just an alias for -I? I assume @Sebastian Ullrich confused these the way I did. -include literally pastes #include in the file

[Sebastian Ullrich]

That's good to hear, I had to look that up just now. Then really you should find out where that undefined reference is coming from

[Eric Wieser]

It would be from the dlsym from the interpreter, I assume?

[Sebastian Ullrich]

That would not be a linker error

[Sebastian Ullrich]

And it's not how the interpreter works iirc

[Eric Wieser]

Ah, I did not se the word linker

[Eric Wieser]

The interpreter definitely uses dlsym to pick up @[extern]s

[Tomas Skrivan]

Even if I have precompiledModules:=true?

[Eric Wieser]

What if you call a function in the same file it was defined? The module hasn't yet been precompiled in that case.

[Eric Wieser]

Can you share the full linker error?

[Tomas Skrivan]

The linker error happens only if I have only the bytearray.c file and in there the function is marked static inline

[Tomas Skrivan]

The error is

info: stderr:
ld.lld: error: undefined symbol: scilean_byte_array_uget_float
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_SciLean_DataArrayN_iget2)
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_SciLean_DataArrayN_iget2___boxed)
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_ByteArray_iget2___rarg)
>>> referenced 10 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang' exited with code 1
Some required builds logged failures:
- KMeansProfile
error: build failed

[Eric Wieser]

That's expected, since the function won't survive as static in the C file alone (without used, anyway)

[Eric Wieser]

What happens if you only have the .h file?

[Tomas Skrivan]

Yes the .h file + -include flag works fine

[Tomas Skrivan]

Ohh sorry you said only the .h file, let me try.

[Tomas Skrivan]

That gives me

info: stderr:
ld.lld: error: undefined symbol: scilean_byte_array_uget_float
>>> referenced by ByteArray.c
>>>               ././.lake/build/ir/SciLean/Data/ByteArray.c.o.export:(l_ByteArray_ugetFloat___boxed)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang' exited with code 1
Some required builds logged failures:
- KMeansProfile
error: build failed

[Tomas Skrivan]

Oh wait I added -include flag only to a separate lean_exe but I should add it to the whole project.

[Tomas Skrivan]

Ok only .h file works too.

I have to add -include to the whole project

@[default_target]
lean_lib SciLean {
  roots := #[`SciLean]
  moreLeancArgs := #["-include", "./C/bytearray.h"]
}

and in the .h file it is important to add #pragma once

#pragma once
#include <lean/lean.h>

static inline double scilean_byte_array_uget_float(b_lean_obj_arg a, size_t i){
  return ((double*)(lean_sarray_cptr(a)))[i];
}

[Eric Wieser]

Eric Wieser said:

What if you call a function in the same file it was defined? The module hasn't yet been precompiled in that case.

Are you able to test this?

[Eric Wieser]

Tomas Skrivan said:

I have to add -include to the whole project

And every downstream project too, unless you provide the C file as well

[Tomas Skrivan]

Eric Wieser said:

Tomas Skrivan said:

I have to add -include to the whole project

And every downstream project too, unless you provide the C file as well

For this reason I'm going with @[extern c inline "((double*)(lean_sarray_cptr(#1)))[#2]"]

[Tomas Skrivan]

Eric Wieser said:

Eric Wieser said:

What if you call a function in the same file it was defined? The module hasn't yet been precompiled in that case.

Are you able to test this?

Does not work

Could not find native implementation of external declaration 'ByteArray.ugetFloat' (symbols 'l_ByteArray_ugetFloat___boxed' or 'l_ByteArray_ugetFloat').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

[Eric Wieser]

Does it work with the empty C file with __attribute__((used))?

[Tomas Skrivan]

Eric Wieser said:

Does it work with the empty C file with __attribute__((used))?

I tried this without the -include flag it it failed again with

info: stderr:
ld.lld: error: undefined symbol: scilean_byte_array_uget_float
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_SciLean_DataArrayN_iget2)
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_SciLean_DataArrayN_iget2___boxed)
>>> referenced by KMeansProfile.c
>>>               ././.lake/build/ir/examples/KMeansProfile.c.o.export:(l_ByteArray_iget2___rarg)
>>> referenced 10 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang' exited with code 1
Some required builds logged failures:
- KMeansProfile
error: build failed

[Tomas Skrivan]

Interestingly enough I'm still getting 60% slower code using ByteArray.ugetFloat compared to FloatArray.uget for some reason :(

[Eric Wieser]

In that example are you compiling the bytearray.c file somehow?

[Tomas Skrivan]

Yes I think so, my current set up should gobble up all .c files in ./C/ directory.