whitemech / lydia

A tool for LDLf translation to DFA and for LDLf synthesis.
GNU Lesser General Public License v3.0
23 stars 4 forks source link

compilation issues #122

Open adl opened 3 weeks ago

adl commented 3 weeks ago

After a discussion with @Shufang-Zhu, I'm trying to compile and install LydiaSyft on Debian, and encountered several issues during the compilation of Lydia.

Spdlog is necessary

It should probably be listed in the list of dependencies.

/home/adl/git/LydiaSyft/submodules/lydia/lib/include/lydia/logger.hpp:20:10: fatal error: spdlog/spdlog.h: No such file or directory
   20 | #include <spdlog/spdlog.h>
      |          ^~~~~~~~~~~~~~~~~
compilation terminated.

A non-standard installation of Mona is necessary

Mona has a package in Debian, so I wanted to use that, but it seems Lydia uses stuff that isn't installed by a standard installation of Mona. The mona/hash.h file isn't installed by Mona's makefile, so it isn't part of the Debian package. (Mona's source code actually contains two different hash.h files.) It looks like I really need to install the Mona fork listed in the dependencies instead, but I think testing for the existence of mona/hash.h with CMake would allow a better error message than the following:

In file included from /home/adl/git/LydiaSyft/submodules/lydia/lib/src/mona_ext/mona_ext_base.cpp:18:
/home/adl/git/LydiaSyft/submodules/lydia/lib/include/lydia/mona_ext/mona_ext_base.hpp:31:10: fatal error: mona/hash.h: No such file or directory
   31 | #include <mona/hash.h>
      |          ^~~~~~~~~~~~~
compilation terminated.

A bug in Catch2 forbid further compilation

The following misleading message is caused by uint8_t not being defined at this point.

/home/adl/git/LydiaSyft/build/_deps/catch2-src/src/catch2/../catch2/catch_test_case_info.hpp:47:10: warning: elaborated-type-specifier for a scoped enum must not use the ‘class’ keyword
   47 |     enum class TestCaseProperties : uint8_t {
      |     ~~~~ ^~~~~

https://github.com/catchorg/Catch2/issues/2713 suggests that this might be fixed in a newer version of Catch2.

adl commented 2 weeks ago

the source depends on some CLI library

But I don't see this dependency listed in the README.

[ 84%] Building CXX object src/synthesis/CMakeFiles/synthesis.dir/source/Utils.cpp.o
/home/adl/git/LydiaSyft/src/synthesis/source/Utils.cpp:7:10: fatal error: CLI/CLI.hpp: No such file or directory
    7 | #include <CLI/CLI.hpp>
      |          ^~~~~~~~~~~~~
compilation terminated.

Apparently the git submodules of LydiaSyft where installed, but not recursively, so Lydia's third-party modules were empty. Running git submodule update --init --recursive manually did the trick.