Run Tests

Stream: lean4

[Mac]

When adding a test that is just suppose tor run without error to Lean 4., does it go in the lean/test/run directory? If so, how do you make the test run when using make tests because it seems like tests added to that directory aren't automatically added to queue for make tests (or I may just be missing something).

[Daniel Selsam]

@Mac When I put a .lean file in tests/lean/run, it is automatically run as part of make test. Are you sure it isn't being run for you too? FYI the full test name should be "leanruntest_<oldname>.lean".

[Mac]

Hmm, that's what I thought should happen. Maybe it's because I didn't rebuild after adding the tests?

[Mac]

Oh! Yep, that's it! :smile:
I didn't think adding tests would require a rebuild.

[Daniel Selsam]

FYI It does not require a rebuild for me.

[Mac]

Interesting! That's weird.
(Fyi, just to clarify, by "rebuild" I mean running make -- the new lean binary is not necessary though)

[Mac]

This may have to due to with the fact I am on Windows, using VSCode, using MSYS2, and/or using GCC as my compiler. (I am using MSYS2/MINGW64 GCC because Lean 4 does not build properly with MSYS2/MINGW64 Clang 11 on my setup).

[Sebastian Ullrich]

We use globs in CMake to collect the tests, which is not recommended because of this issue, but I'm not aware of a reasonable alternative either

[Sebastian Ullrich]

Mac said:

MSYS2/MINGW64 GCC because Lean 4 does not build properly with MSYS2/MINGW64 Clang 11 on my setup).

That's weird, since that is how the official Windows release is built

[Mac]

Sebastian Ullrich said:

That's weird, since that is how the official Windows release is built

Yep. The first time I built it, I didn't notice that line and didn't specify it to build with Clang so CMake ended up defaulting to GCC . When I later discovered my mistake and tried a fresh rebuild with Clang things broke. Thus I ended up reverting back to using GCC and everything still works. Surprisingly, it was still building even when the Windows CI/CD broke due to symbol issues, so maybe GCC doesn't have the same symbol issues (or something else is weird)?

[Mac]

Oh! Technically, according to CMakeCache.txt, my build is using the MSYS2's c++ (which I believe is GCC -- based on it using other GNU Binutils such as ld):

$ c++ --version
c++.exe (Rev10, Built by MSYS2 project) 10.2.0
Copyright (C) 2020 Free Software Foundation, Inc.

[Sebastian Ullrich]

clang should also be using ld on Windows by default. It might be some minor difference like g++'s runtime library using fewer symbols than clang's or something