FFI & C++ on Windows

Stream: general

[Jon Eugster]

I recently had an issue report which essentially said that a user didn't have C++ on their Windows machine and therefore failed to build a lean package that used FFI (foreign-function-interface).

The FFI used in lean4-i18n is following the official example:

target time.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "time.o"
  let srcJob ← inputFile <| pkg.dir / "time" / "c" / "time.cpp"
  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
  buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace

First of all, is it typical for Windows users to not have C++ available per default? And if so, what are the recommended instructions to fix this? Is there anything I could change on the setup to prevent beginners (on Windows) using the package to stumble across this error (error: failed to execute `c++`: no such file or directory (error code: 2))?

[Jon Eugster]

I would also be happy if there was a way to just not use the FFI if it's failing: It's only used for a function printing the system time, and if I could set it up in a way that this function just returns "" if C++ is not available, that would be satisfactory. But I assume that's not possible, is it?

[Richard Copley]

No, Windows doesn't have a "c++.exe", by default. (Neither does Ubuntu!) The usual way to get a native Windows g++ or clang++ available as c++ is to install MSYS2, but if the user doesn't already know that, it's a long path. I would suggest you recommend the user installs WSL2 and Ubuntu 24.04 and works there instead of in Windows (and installs build-essentials to get c++).

Alternatively, does it make sense to change "c++" to "leanc"?

[Jon Eugster]

Thanks for the explanation! Is leanc something that's available for anybody using Lean? That does sound like the best approach, although I know nothing about these things.

Is there a reason the official documentation for FFI does not use leanc there?

[Richard Copley]

I don't know details, but leanc is some kind of special build of clang, and it's always installed with Lean 4. Maybe there's a good reason not to use it as if it were a 'normal' compiler.

(I don't really understand how one expects to be able to make use of FFI without already knowing how to compile stuff. That's probably a bit uncharitable of me.)

[Jon Eugster]

Actually, with leanc I don't know how to do the imports, my example file was time.cpp:

#include <stdio.h>
#include <time.h>
#include <string>

#include <lean/lean.h>

extern "C" lean_obj_res formatLocalTime() {
    time_t rawtime;
    struct tm *timeinfo;
    char buffer[80];
    time(&rawtime);
    timeinfo = localtime(&rawtime);
    strftime(buffer, sizeof(buffer), "%c", timeinfo);
    return lean_io_result_mk_ok(lean_mk_string(buffer));
}

Sorry for not knowing a single thing about C/C++ anymore, but with leanc it says

info: stderr:
././time/c/time.cpp:1:10: fatal error: 'stdio.h' file not found
#include <stdio.h>
         ^~~~~~~~~

do you know how to do these includes correctly?

[Sebastian Ullrich]

leanc is an implementation detail. Don't use it.

[Jon Eugster]

ok good to know. But maybe I'll just drop the feature which uses FFI if there isn't any good way to make it work out of the box for everybody...

it's not really an important feature anyways, just printing a timestamp into a translation file when it's autogenerated...

[Jz Pan]

The Windows (in fact, also for Linux/Mac) version of Lean ships with a clang C++ compiler. It comes with C/C++ libraries, but not header files. You can look at this file https://github.com/acmepjz/md4lean/blob/main/lakefile.lean which uses it in an ad-hoc way.

[Jz Pan]

A possible solution is download a version of clang for Windows from its official website (https://releases.llvm.org/) and extract the header files. Hopefully the header files are of correct version.

[Jon Eugster]

thanks, especially the example shows some neat tricks, in particular Platform.isWindows and ← getLeanCc. However, this seems all too complicated for the little benefits of my use case. I just commented-out everything related to FFI and moved on :sweat_smile: