lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Bump up to LLVM 15

Open bollu opened this issue 3 years ago • 2 comments

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 !

bollu avatar Oct 05 '22 21:10 bollu

Thanks for your contribution! Please make sure to follow our Commit Convention.

github-actions[bot] avatar Oct 05 '22 21:10 github-actions[bot]

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.

tobiasgrosser avatar Oct 06 '22 09:10 tobiasgrosser