Linking error when building Debug version in Cygwin

[inpefess]

I followed instruction from wiki https://github.com/vprover/vampire/wiki/Cygwin

cmake .. and then make builds with no errors.

But after cmake .. -DCMAKE_BUILD_TYPE=Debug, make fails with the following errors:

[100%] Linking CXX executable bin/vampire_z3_dbg_master_6994.exe
/usr/lib/gcc/x86_64-pc-cygwin/11/../../../../x86_64-pc-cygwin/bin/ld: CMakeFiles/test_obj.dir/Test/TestUtils.cpp.o: in function `Test::Pretty<Kernel::Literal*>::prettyPrint(std::ostream&) const':
~/vampire/Test/TestUtils.cpp:105: multiple definition of `Test::Pretty<Kernel::Literal*>::prettyPrint(std::ostream&) const'; CMakeFiles/InterpretedFunctions_obj.dir/UnitTests/tInterpretedFunctions.cpp.o:~/vampire/Test/TestUtils.hpp:151: first defined here
/usr/lib/gcc/x86_64-pc-cygwin/11/../../../../x86_64-pc-cygwin/bin/ld: CMakeFiles/test_obj.dir/Test/TestUtils.cpp.o: in function `Test::Pretty<Kernel::Clause>::prettyPrint(std::ostream&) const':
~/vampire/Test/TestUtils.cpp:110: multiple definition of `Test::Pretty<Kernel::Clause>::prettyPrint(std::ostream&) const'; CMakeFiles/GaussianElimination_obj.dir/UnitTests/tGaussianElimination.cpp.o:~/vampire/Test/TestUtils.hpp:114: first defined here
/usr/lib/gcc/x86_64-pc-cygwin/11/../../../../x86_64-pc-cygwin/bin/ld: CMakeFiles/test_obj.dir/Test/TestUtils.cpp.o: in function `Test::Pretty<Kernel::Literal>::prettyPrint(std::ostream&) const':
~/vampire/Test/TestUtils.cpp:125: multiple definition of `Test::Pretty<Kernel::Literal>::prettyPrint(std::ostream&) const'; CMakeFiles/InterpretedFunctions_obj.dir/UnitTests/tInterpretedFunctions.cpp.o:~/vampire/Test/TestUtils.hpp:114: first defined here
collect2: error: ld returned 1 exit status
make[2]: *** [CMakeFiles/vtest.dir/build.make:640: vtest.exe] Error 1
make[1]: *** [CMakeFiles/Makefile2:1913: CMakeFiles/vtest.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[100%] Built target vampire
make: *** [Makefile:101: all] Error 2

[MichaelRawson]

Is this definitely failing while linking the main Vampire executable? Test code shouldn't be linked to that, so this is very surprising! Let's fix this first and go back to #518.

If you run make VERBOSE=1, what do you get?

[inpefess]

So, to reproduce (on Cygwin):

git clone https://github.com/vprover/vampire
cd vampire
mkdir test_build
cd test_build
cmake .. -DCMAKE_BUILD_TYPE=Debug
make -j11 VERBOSE=1 > build.log 2>&1

build.log

[MichaelRawson]

@joe-hauns - sorry to disturb with IJCAR/LPAR coming up, but do you know how this works?

I'm not actually sure how this compiles on my machine/CI. There's a template for Pretty<T>, specialised to various things, including Pretty<Literal *> (I think this one's redundant with respect to the existing T * specialisation), Pretty<Literal>, and Pretty<Clause>.

These last three are declared and defined in TestUtils.cpp, but are probably also used elsewhere (?). I think they probably want to get at least declared in the header file.

[joe-hauns]

Yeah so the issue is definitely that the test code is being compiled into the main binary. I think i fixed this one issue (try compiling the branch cygwin-test-fix), but as compiling the tests into main is not expected there might be other issues coming up from time to time, e.g. if someone uses the same function names in multiple tests (e.g. test01 or other informative names ;) ), so test functions should not be compiled into main after all.

[MichaelRawson]

Yeah so the issue is definitely that the test code is being compiled into the main binary.

Ah, sorry, I forgot to mention that - it isn't, just looks like it because of the multicore build output. Looking at the build log the failed command links vtest.exe...but it sounds like you expect each test to be a separate binary?

[joe-hauns]

Oh well actually you're right there. The tests are really one binary. I forgot that the TEST_FUN macro appends a prefix to every test function to prevent the error with test01 i was hinting at. So everything sould be fine if we merge cygwin-test-fix (given this actually fixes the issue for that compiler).

[inpefess]

I confirm that cygwin-test-fix builds under Cygwin and all the tests pass. @joe-hauns thank you!

[MichaelRawson]

Merged directly, thanks @joe-hauns !