NeuralNetworkVerification/Marabou

Compilation failure on Linux

izzayacine opened this issue · 2 comments

It seems that cmake file is not properly configured.
I am trying to install Marabou on Linux (Red Hat Enterprise Linux release 8.4 (Ootpa)) using the following commands:

cd path/to/marabou/repo/folder
mkdir build 
cd build
cmake ..
cmake --build .

I first get this error:

[  0%] Building CXX object CMakeFiles/MarabouHelper.dir/src/engine/DnCManager.cpp.o
Path/To/Marabou/src/engine/DnCManager.cpp:135:5: error: use of undeclared identifier 'openblas_set_num_threads'
    openblas_set_num_threads( numWorkers );
    ^
Path/To/Marabou/src/engine/DnCManager.cpp:148:5: error: use of undeclared identifier 'openblas_set_num_threads'
    openblas_set_num_threads( 1 );
    ^
2 errors generated.

When I comment these functions in DnCManager.cpp and main.cpp, but I still other errors:

[ 11%] Built target MarabouHelper
[ 11%] Linking CXX executable Marabou
ld.lld: error: unable to find library -lm
ld.lld: error: unable to find library -lrt
ld.lld: error: unable to find library -lpthread
ld.lld: error: unable to find library -lpmi
ld.lld: error: unable to find library -lpmi2
ld.lld: error: unable to find library -lm
ld.lld: error: unable to find library -lpthread
ld.lld: error: unable to find library -lrt
ld.lld: error: unable to find library -lpthread
ld.lld: error: unable to find library -lpmi
ld.lld: error: unable to find library -lpmi2
ld.lld: error: unable to find library -lm
ld.lld: error: unable to find library -lrt
ld.lld: error: unable to find library -lpthread
ld.lld: error: unable to find library -lpmi

And if I use the debug mode, I got error in the tests:

61% tests passed, 27 tests failed out of 69

Label Time Summary:
basis_factorization unit       =  29.75 sec*proc (14 tests)
common unit                    =  14.56 sec*proc (19 tests)
engine unit                    =  44.17 sec*proc (25 tests)
network_level_reasoner unit    =   6.06 sec*proc (4 tests)
parser unit                    =   0.35 sec*proc (1 test)
proofs unit                    =   4.08 sec*proc (5 tests)
query_loader unit              =   0.27 sec*proc (1 test)

Total Test time (real) =   2.99 sec

The following tests FAILED:
	  1 - Test_AbsoluteValueConstraint (Failed)
	  3 - Test_BoundManager (Failed)
	  4 - Test_ConstraintMatrixAnalyzer (Failed)
	  5 - Test_CostFunctionManager (Failed)
	  8 - Test_DisjunctionConstraint (Failed)
	 10 - Test_Engine (Failed)
	 20 - Test_RowBoundTightener (Failed)
	 25 - Test_Tableau (Failed)
	 26 - Test_CSRMatrix (Failed)
	 27 - Test_CompareFactorizations (Failed)
	 28 - Test_ForrestTomlinFactorization (Failed)
	 29 - Test_LUFactorization (Failed)
	 30 - Test_LUFactors (Failed)
	 32 - Test_SparseFTFactorization (Failed)
	 33 - Test_SparseGaussianEliminator (Failed)
	 34 - Test_SparseLUFactorization (Failed)
	 35 - Test_SparseLUFactors (Failed)
	 36 - Test_SparseUnsortedArray (Failed)
	 37 - Test_SparseUnsortedArrays (Failed)
	 38 - Test_SparseUnsortedList (Failed)
	 39 - Test_SparseUnsortedLists (Failed)
	 57 - Test_Vector (Failed)
	 70 - Test_DeepPolyAnalysis (Failed)
	 71 - Test_NetworkLevelReasoner (Failed)
	 72 - Test_WsLayerElimination (Failed)
	 74 - Test_BoundExplainer (Failed)
	 78 - Test_UnsatCertificateUtils (Failed)
Errors while running CTest
gmake[2]: *** [CMakeFiles/build-tests.dir/build.make:76: build-tests] Error 8
gmake[1]: *** [CMakeFiles/Makefile2:881: CMakeFiles/build-tests.dir/all] Error 2
gmake: *** [Makefile:114: all] Error 2

It seems openblas is not correctly installed. Could you share the output when you run

cmake ..

Closing due to inactivity. Feel free to re-open if the issue persists.