lean4
lean4 copied to clipboard
Bump up to LLVM 15
Let us refactor the patch that adds LLVM support to Lean4 into another component: We first bump up LLVM to LLVM 15, and then add the bindings.
We see that the windows build breaks at this stage in itself. Help debugging this would be great, @Kha !
Thanks for your contribution! Please make sure to follow our Commit Convention.
The failure on windows is surprising to me. Here a couple of things I already looked into:
https://releases.llvm.org/15.0.0/projects/libcxx/docs/ReleaseNotes.html mentions:
The _LIBCPP_ABI_USE_CXX03_NULLPTR_EMULATION macro controlling whether we use an emulation for std::nullptr_t in C++03 mode has been removed. After this change, _LIBCPP_ABI_USE_CXX03_NULLPTR_EMULATION will not be honoured anymore and there will be no way to opt back into the C++03 emulation of std::nullptr_t.
which is further discussed at https://reviews.llvm.org/D109459 and https://reviews.llvm.org/D114786. I had tried to build lean4 stage 1 with C++11, but could not get it working.
There are also a small number of reports that point to wrong include directories (mostly for apple builds). I am not sure what is breaking here.