FFI on windows

Stream: lean4

[James Randolf]

I'm trying to use FFI on Windows and I'm getting the following error when it tries to compile ffi.c, am I doing something wrong?

fatal error: 'stddef.h' file not found
#include <stddef.h>
         ^~~~~~~~~~
1 error generated.
error: external command `clang` exited with code 1

[Mac Malone]

@James Randolf What does your lakefile look like (how are you compiling your FFI)?

[James Randolf]

import Lake
open Lake DSL

package test
lean_lib Test

@[default_target] lean_exe test {
  root := `Main
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.c"
  let flags := #["-I", (← getLeanIncludeDir).toString]
  buildO "ffi.c" oFile srcJob flags "clang"

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]

[James Randolf]

ffi.c is

#include <lean/lean.h>

int test(int x) {
    return x * 2;
}

[James Randolf]

It seems that without the #include, everything works, but as soon as I try to include anything at all I get a fatal error: '...' file not found error.

[Mac Malone]

@James Randolf The error indicates it cannot find the C standard library includes (in this case, the compiler-specific stddef) in its default search path. How did you install clang?

[Mac Malone]

Windows does not come with a C compiler and library by default, so it is quite easy to get this error if something went wrong in the the setup of whatever compiler you do install (Clang in your case).

[James Randolf]

It seems to be using the clang at C:\Users\James\.elan\toolchains\leanprover--lean4---nightly-2023-08-19\bin\clang.exe

[Mac Malone]

@James Randolf Oh, in that case, yeah that will not work. Lean does not ship a standard library with tis bundled Clang.

[Mac Malone]

You need to install a C compiler yourself and use that to build.

[James Randolf]

I see, thanks a lot!

[Mac Malone]

Quick example: to install Clang in MSYS2 you can execute the following in a MSYS2 shell.

pacman -S mingw-w64-x86_64-clang

Then, as long as you run lake build from the MSYS2 shell, it should use the clang installed.