LeanCopilot: LeanInfer could not build when tested on Github Codespace

The issues were posted on Zulip, please check there for more context.

TL;DR

1. Github Codespace can only compile after -stdlib=libc++ is removed
2. lake build hangs indefinitely in linking, and it’s not using much CPU

Issue Details

I’ve tried out lean4-example in Github Codespace, I got the following issues:

1. lake build fails to compile C++ with Clang++, resolved by removing all -stdlib=libc++from the lakefile of LeanInfer

lean4-example (improve-installation) $ lake build
[23/197] Compiling ffi.cpp
error: > clang++ -c -o ./lake-packages/LeanInfer/build/ffi.o ./lake-packages/LeanInfer/ffi.cpp -fPIC -std=c++11 -stdlib=libc++ -O3 -I /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
error: stderr:
In file included from ./lake-packages/LeanInfer/ffi.cpp:1:
/home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include/lean/lean.h:14:10: fatal error: 'atomic' file not found
#include <atomic>
         ^~~~~~~~
1 error generated.
error: external command `clang++` exited with code 1

I ran bash -c "$(wget -O - https://apt.llvm.org/llvm.sh)" from https://apt.llvm.org/ to fix it, no change. Then I test the clang++ command with extra options -E -x c++ -v at the end, it showed the following search path:

ignoring nonexistent directory "/include"
#include "..." search starts here:
#include <...> search starts here:
 /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

which is shorter than a raw clang++ -E -x c++ - -v < /dev/null 2>&1 which shows

ignoring nonexistent directory "/include"
ignoring duplicate directory "/usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9"
#include "..." search starts here:
#include <...> search starts here:
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/backward
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

Clearly Clang++ stop looking for the GNU C++ headers if -stdlib=libc++ is present. If Github Codespace misses it I guess it would be missed in the environments of many end-users.

1. After resolved issue 1, I end up having the same issue fatal error: 'onnxruntime_cxx_api.h' file not found, resolved by

( cd /workspace/ && wget https://github.com/microsoft/onnxruntime/releases/download/v1.15.1/onnxruntime-linux-x64-1.15.1.tgz && tar xzvf  onnxruntime-linux-x64-1.15.1.tgz)

Then add "-I", "/workspaces/onnxruntime-linux-x64-1.15.1/include" to flags in LeanInfer lakefile or just add CPATH environment variable as instructed.

1. Run lake build after step 2, I have the same linker error libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libonnxruntime.so.1.15.1: cannot open shared object file: No such file or directory, I tried to fix it by adding "-L", "/workspace/onnxruntime-linux-x64-1.15.1/lib/" to moreLinkArgs then

LD_LIBRARY_PATH=/workspaces/onnxruntime-linux-x64-1.15.1/lib/ lake build

But the build hangs indefinitely, and it’s not using much CPU (❤️%). So far, I’m stuck here.