New comment by tornaria on void-packages repository https://github.com/void-linux/void-packages/pull/35907#issuecomment-1055730991 Comment: > Just patch out buggy tests, we don't need to check upstream coding conventions for our builds. That was not obvious. I had to rewrite `do_check()` to use `ctest -E `. The build-style uses `ninja test` for this, but I didn't see a way to pass options to `ctest`. I wish xbps-src had some tools to make skipping tests by name easier for the standard test frameworks (cmake, autotools, pytest, etc). > The one you found on i686 looks like a real bug at first, however. Can you reproduce that in a LSP editor? I've just disabled since I don't want to worry about 32 bit right now. TBH, I don't yet know how to actually USE lean locally -- I want to learn lean so I've been playing with some of the tutorials using the online version. I don't have a clue how to move forward with this. Apparently I need more stuff, like `leanproject` to install mathlib, etc. And I take that this cannot be run from CLI, I need some sort of plugin (unfortunately, it seems there is no vim plugin, only a neovim one).