cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Error building LFSC #47

Closed blishko closed 4 years ago

blishko commented 4 years ago

Hi, when I try building LFSC I ran into a compilation error when compiling lexer.cpp file. The CMake configuration step finished successfully and found FLEX (2.6.4) on my system. I trying to build on MacOS, using AppleClang.

This is the first compilation error:

/Users/mblicha/projects/LFSC/build/src/lexer.cpp:2870:8: error: member reference type 'std::istream *' (aka 'basic_istream<char> *') is a pointer; did you mean to use '->'?
                        yyin.rdbuf(std::cin.rdbuf());
                        ~~~~^

Any advice? I am trying to build exactly according to your instructions for a regular build.

alex-ozdemir commented 4 years ago

Hi @blishko,

Sorry for the delayed response. Hopefully we can help you sort this out.

The offending line is one generated by the flex binary, and is not from the LFSC source tree. This suggests that the flex binary and the FlexLexer.h header on your system may be out of sync. Likely your header is version 2.5.x, and your binary is version 2.6.x. Either is fine for building LFSC, but it's important that they are the same.

This comment contains some steps which will help you confirm the problem. You should check that the header contains the pointer definition of yyin, and then that flex -V reports version 2.6.x.

If the two are indeed out of sync, then the root cause is likely two conflicting flex installations. You could fix this by removing one of them.

blishko commented 4 years ago

Hi @alex-ozdemir , thanks for your reply. You were right there were two versions of FlexLexer.h on my system and of course the older one was found first.

Unfortunately, I am not able to remove the old header files, I don't what to mess with Apple's system files. I have found the following solution:

  1. I needed to make sure that find_package(FLEX) finds the right include directory. Surprisingly, at the beginning, the variable FLEX_INCLUDE_DIRS was set to FLEX_INCLUDE_DIR-NOTFOUND even though find_package is used with REQUIRE keyword. To me this seems like a bug in CMake's FindFLEX.cmake, I would expect the find_package to fail if it did not find the include directory. I managed to fix this by providing a hint to CMake where it should look using CMAKE_INCLUDE_PATH variable.
  2. After making sure CMake finds the right include directory I needed to ensure this include directory is added to your target. I added include_directories(${FLEX_INCLUDE_DIRS}) to your main CMakeLists and finally it worked!

Thanks for pointing me to the right direction. I still believe you should explicitly add to your target the include directory found by the find_package command. Otherwise you don't allow the user to choose which version of Flex should be used when there are multiple incompatible versions on their system, as was my case.

alex-ozdemir commented 4 years ago

Hi @blishko,

Thanks for letting me know how you resolved this issue.

I still believe you should explicitly add to your target the include directory found by the find_package command.

You're absolutely correct. We should probably also check FLEX_INCLUDE_DIR-NOTFOUND ourselves and leave a note in the README about providing a hint to CMake. Would you like to submit a PR doing this, or should I go ahead and do it, crediting you?

blishko commented 4 years ago

Would you like to submit a PR doing this, or should I go ahead and do it, crediting you?

Please, go ahead. You know better the coding and the documentation style you use, it will be faster. I think it is enough to link the PR to this issue.