Tobias Grosser

I also just got the "Could not store account credentials" message after the password prompt.

@bollwyvl, the readonly trick works. Funny enough, if you then use File -> "Save Notebook As" and select a different filename, you get an error that the file already exists...

> > Funny enough, if you then use File -> "Save Notebook As" and select a different filename, you get an error that the file already exists and the previous...

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...

I can not find src/Lean/Compiler/IR/EmitLLVM.cpp.

@bollu, this build went through: https://github.com/tobiasgrosser/lean4/pull/6

In particular, you need sth like: ``` if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") find_package(ZLIB REQUIRED) message("ZLIB_LIBRARY: ${ZLIB_LIBRARY}") cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH) string(APPEND LEAN_EXTRA_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}") string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt...

I just managed to get a virtualbox installed to reproduce and bisect this. AFAIU this never worked, but the issue seems to be limited to tblgen-lsp-server. For some reason, we...

The issue I see is similar to the one that has been reported and fixed in https://reviews.llvm.org/D134637. > Build a version of the support library that does not link against...

No, I did not apply it. I feel I would need something similar for MLIR, but this will require some programming that I did not yet find the time to...