Unable to build on Linux: can't find carl header file

[rpgoldman]

When I try to build according to the instructions here, I get this error during cmake:

pg@achilles:~/src/smtrat-pub-onecell-1/build$ cmake ..
-- The CXX compiler identification is GNU 7.5.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
fatal: not a git repository (or any parent up to mount point /)
Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).
-- Could not parse version from git, using default 21.05
-- Did not find clang-tidy, target tidy is disabled.
-- not using cotire
-- Using g++ 7.5.0
-- CXX Flags:  -Wunknown-pragmas -std=c++17 -pthread -fmax-errors=5 -fdiagnostics-color=auto
-- CXX Debug Flags: -g -O1
-- CXX Release Flags: -O3 -DNDEBUG -O3
-- Build type: RELEASE
-- Use system version of carl 22.09 (required 21.05) from /home/rpg/src/carl-master/src
-- Did not find libssh, disabled SSH backend.
-- Did not find libssh_threads. If you have a libssh version < 0.8, then this is an error. Beginning from 0.8, libssh_threads is not required.
-- Configuring done
CMake Error at src/cli/CMakeLists.txt:49 (add_dependencies):
  The dependency target "carl-shared" of target "smtrat-objects" does not
  exist.


-- Generating done
-- Build files have been written to: /home/rpg/src/smtrat-pub-onecell-1/build

Question about work-around

I have been able to download the most recent carl distribution and build it on the same machine. Is there some way to tell cmake for smtrat not to build carl, but instead to use the version I have built? Is there perhaps an environment variable I could set to point to my ~/src/carl-master/ directory (or perhaps something inside carl-master such as carl-master/build)?

Note that I do not have root access to this machine

Trying to continue with make

If I try to continue with make after the above cmake error,m I get an error that Carl headers are not found:

-- Installing: /home/rpg/src/smtrat-pub-onecell-1/build/resources/include/immer/flex_vector_transient.hpp
[  6%] Completed 'Immer-EP'
[  6%] Built target Immer-EP
Scanning dependencies of target resources
[  6%] Built target resources
Scanning dependencies of target smtrat-unsat-cores-objects
[  6%] Building CXX object src/smtrat-unsat-cores/CMakeFiles/smtrat-unsat-cores-objects.dir/smtrat-unsat-cores.cpp.o
In file included from /home/rpg/src/smtrat-pub-onecell-1/src/smtrat-common/smtrat-common.h:6:0,
                 from /home/rpg/src/smtrat-pub-onecell-1/src/smtrat-unsat-cores/UnsatCore.h:4,
                 from /home/rpg/src/smtrat-pub-onecell-1/src/smtrat-unsat-cores/smtrat-unsat-cores.h:3,
                 from /home/rpg/src/smtrat-pub-onecell-1/src/smtrat-unsat-cores/smtrat-unsat-cores.cpp:1:
/home/rpg/src/smtrat-pub-onecell-1/src/smtrat-common/settings/Settings.h:3:10: fatal error: carl/util/Singleton.h: No such file or directory
 #include <carl/util/Singleton.h>
          ^~~~~~~~~~~~~~~~~~~~~~~
compilation terminated.

This is from the pub-onecell-1 downloaded archive.

[modass]

I believe this error may be related to the recent interface change in CArL. The target carl-shared and carl-master should not exist anymore. Thus, linking in SMT-RAT fails, I believe.

@derjasper I think linking to the individual carl-libraries and updating the includes should do the trick, maybe.

[rpgoldman]

Is there any work-around for this? Or is it possible to install an older version of carl and get a build going using that?

I would very much like to try out SMT-RAT on a hybrid system, but that’s impossible as far as I can tell

[derjasper]

pub-onecell-1 is an old release which is not compatible with the current CArL version. I marked the newer version tags as release; then, it should just work.
You can also tell SMT-RAT to use a specific CArL version using the carl_DIR cmake parameter.

[rpgoldman]

Thank you!