arminbiere / cadical

CaDiCaL SAT Solver
MIT License
358 stars 126 forks source link

Project doesn't install anything #49

Open yurivict opened 1 year ago

yurivict commented 1 year ago

There's no 'install' target.

===>  Staging for cadical-1.5.3
===>   Generating temporary packing list
gmake[1]: Entering directory '/usr/ports/math/cadical/work/cadical-rel-1.5.3'
gmake[1]: *** No rule to make target 'install'.  Stop.
gmake[1]: Leaving directory '/usr/ports/math/cadical/work/cadical-rel-1.5.3'
*** Error code 2
arminbiere commented 1 year ago

The solver is currently mainly targeted towards developers and not end-users. Developers can be assumed to work directly with the source code and usually do not rely on installed packages anyhow. Therefore I assume that developers easily can pick up the code (the library) directly from the source code. If there is more binary only usage of the solver (including the wish to only link against the code dynamically) I would like to hear about those use cases first, before spending time on making this feature available.

pauljurczak commented 1 year ago

I would like to hear about those use cases

I was installing cvc5 solver (https://github.com/cvc5/cvc5) and installation failed due to unsatisfied CaDiCaL dependency. I've built CaDiCaL and noticed lack of install, too. Not sure how to proceed. Copy cadical.o somewhere?


I found an installation option for cvc5, which takes care of CaDiCaL dependency, so this is not a problem anymore.

arminbiere commented 1 year ago

This could in my view only a cvc5 build / installation issue. However, the cvc5 team is very careful in this regard and thus I tried to build cvc5 from scratch, which succeeded without problem (I used ./configure.sh --auto-download && make -j 32 build && sudo make install). The output says something about Built target CaDiCaL-EP and deps/lib/libcadical.a exists too. Further

$ nm --demangle /usr/local/lib/libcvc5.so.1|grep CaDiCaL::|wc
    858    5537  106728

I can not confirm your problems.

pauljurczak commented 1 year ago

@arminbiere Thank you. As I mentioned in my post, --auto-download takes care of this issue for me.

yurivict commented 3 months ago

The solver is currently mainly targeted towards developers and not end-users.

We have the FreeBSD port for cadical. It provides a pre-built package. This package is used as a dependency of math/boolector and math/boolector. It is also used when for example some other package uses a bundled version of cadical which doesn't build because it is missing some include statement. There are other use cases.

Your understanding that cadical will be only used as a bundled dependency doesn't match reality. Additionally such approach to dependencies isn't scalable, and obviously suffers from exponential dependency accumulation, when many packages would hypothetically depend on many other hierarchically bundled dependencies.