Installing Storm on macOS with Apple M1

[alebugariu]

Hi, I am trying to build and install Storm from sources (v1.8.0) on macOS with Apple M1 (I would like to use stormpy and unfortunately it does not seem to work with my homebrew installation).

However, the build fails at the step [ 0%] Performing build step for 'sylvan'. The file sylvan-build-err.log contains the following error:

storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter.h:3:
In file included from /storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter_Private.h:8:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/FactorizedPolynomial.h:14:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/PolynomialFactorizationPair.h:307:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/PolynomialFactorizationPair.tpp:15:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/MultivariateGCD.h:11:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/MonomialOrdering.h:9:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/Term.h:10:
In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/../interval/Interval.h:39:
In file included from /opt/local/include/boost/numeric/interval.hpp:18:
/opt/local/include/boost/numeric/interval/hw_rounding.hpp:42:4: error: Boost.Numeric.Interval: Please specify rounding control mechanism.
#  error Boost.Numeric.Interval: Please specify rounding control mechanism.
   ^
1 error generated.
make[5]: *** [src/CMakeFiles/sylvan.dir/sylvan_obj.cpp.o] Error 1
make[4]: *** [src/CMakeFiles/sylvan.dir/all] Error 2
make[3]: *** [all] Error 2

Could you please advise me how to fix this issue? Thank you very much for your time and help, Alexandra

[volkm]

Hi, if you want to use stormpy, you indeed have to manually build all dependencies (carl-storm, Storm, pycarl and stormpy). To avoid problems, I recommend to first uninstall the homebrew packages: brew uninstall carl-storm stormchecker. Currently, Storm is still using an (old) carl installation from homebrew.

After removing the homebrew packages, you can start by building Carl and then continue with Storm. Maybe this already fixes your issue. If not, please let us know and provide us the complete CMake output from Storm. Then we can take a look into it.

[alebugariu]

Thank you for your suggestion. I have uninstalled the homebrew packages carl-storm and stormchecker and I successfully built Carl. However, when trying to build Storm, I get the same error as before. The output of make from Storm is:

[  0%] Creating directories for 'l3pp_ext'
[  0%] Performing download step (git clone) for 'l3pp_ext'
Cloning into 'l3pp'...
HEAD is now at e4f8d7f Fix some references to log4carl
[  0%] No update step for 'l3pp_ext'
[  0%] No patch step for 'l3pp_ext'
[  0%] No configure step for 'l3pp_ext'
[  0%] No build step for 'l3pp_ext'
[  0%] No install step for 'l3pp_ext'
[  0%] Completed 'l3pp_ext'
[  0%] Built target l3pp_ext
[  0%] Creating directories for 'eigen_src'
[  0%] Performing download step (git clone) for 'eigen_src'
Cloning into 'StormEigen'...
HEAD is now at b0eded878 DOC: Update documentation for 3.4.x
[  0%] No update step for 'eigen_src'
[  0%] Performing patch step for 'eigen_src'
[  0%] No configure step for 'eigen_src'
[  0%] No build step for 'eigen_src'
[  0%] No install step for 'eigen_src'
[  0%] Completed 'eigen_src'
[  0%] Built target eigen_src
[  0%] Creating directories for 'cudd3'
[  1%] No download step for 'cudd3'
[  1%] No update step for 'cudd3'
[  1%] Performing patch step for 'cudd3'
[  1%] Performing configure step for 'cudd3'
-- cudd3 configure command succeeded.  See also /storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-configure-*.log
[  1%] Performing build step for 'cudd3'
-- cudd3 build command succeeded.  See also /storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-build-*.log
[  1%] Performing install step for 'cudd3'
-- cudd3 install command succeeded.  See also /storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-install-*.log
[  1%] Completed 'cudd3'
[  1%] Built target cudd3
[  1%] Creating directories for 'sylvan'
[  1%] No download step for 'sylvan'
[  1%] No update step for 'sylvan'
[  1%] No patch step for 'sylvan'
[  1%] Performing configure step for 'sylvan'
-- sylvan configure command succeeded.  See also /storm/build/sylvan/src/sylvan-stamp/sylvan-configure-*.log
[  1%] Performing build step for 'sylvan'
CMake Error at /storm/build/sylvan/src/sylvan-stamp/sylvan-build-RELEASE.cmake:49 (message):
  Command failed: 2

   '/Library/Developer/CommandLineTools/usr/bin/make'

  See also

    /storm/build/sylvan/src/sylvan-stamp/sylvan-build-*.log

make[2]: *** [sylvan/src/sylvan-stamp/sylvan-build] Error 1
make[1]: *** [CMakeFiles/sylvan.dir/all] Error 2
make: *** [all] Error 2

And now sylvan-build-err.log contains:

In file included from /storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter.h:3:
In file included from /storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter_Private.h:8:
In file included from /carl-storm/src/carl/core/FactorizedPolynomial.h:14:
In file included from /carl-storm/src/carl/core/PolynomialFactorizationPair.h:307:
In file included from /carl-storm/src/carl/core/PolynomialFactorizationPair.tpp:15:
In file included from /carl-storm/src/carl/core/MultivariateGCD.h:11:
In file included from /carl-storm/src/carl/core/MonomialOrdering.h:9:
In file included from /carl-storm/src/carl/core/Term.h:10:
In file included from /carl-storm/src/carl/core/../interval/Interval.h:39:
In file included from /opt/local/include/boost/numeric/interval.hpp:18:
/opt/local/include/boost/numeric/interval/hw_rounding.hpp:42:4: error: Boost.Numeric.Interval: Please specify rounding control mechanism.
#  error Boost.Numeric.Interval: Please specify rounding control mechanism.
   ^
1 error generated.
make[5]: *** [src/CMakeFiles/sylvan.dir/sylvan_obj.cpp.o] Error 1
make[4]: *** [src/CMakeFiles/sylvan.dir/all] Error 2
make[3]: *** [all] Error 2

[volkm]

Can you also add the output of CMake?

[alebugariu]

Yes, sorry, I have forgotten to add it in my previous message:

CMake Deprecation Warning at CMakeLists.txt:3 (cmake_policy):
  Compatibility with CMake < 3.5 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.

-- The CXX compiler identification is AppleClang 15.0.0.15000100
-- The C compiler identification is AppleClang 15.0.0.15000100
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Library/Developer/CommandLineTools/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /Library/Developer/CommandLineTools/usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Storm - CMake install dir: /usr/local/lib/CMake/storm
-- Storm - Building RELEASE version.
-- Storm - Could not find ccache.
-- Storm - Detected operating system Mac OS.
-- Storm - Detected that target system uses Apple Silicon.
CMake Warning at CMakeLists.txt:194 (message):
  Compiling natively on Apple Silicon is experimental.  Please report issues
  to support@stormchecker.org.  For more information visit
  https://www.stormchecker.org/documentation/obtain-storm/apple-silicon.html

CMake Warning at CMakeLists.txt:197 (message):
  CLN and GiNaC are currently not supported on Apple Silicon-based
  architectures.  Disabling Storm and carl usage of the libraries.

-- Storm - Assuming extension for shared libraries: .dylib
-- Storm - Assuming extension for static libraries: .a
-- Storm - Build static libraries.
CMake Warning at CMakeLists.txt:247 (message):
  Disabling stack checks for AppleClang version 11.0.0 or higher.

-- Storm - Enabling link-time optimizations.
-- Performing Test COMPILER_C_WORKS
-- Performing Test COMPILER_C_WORKS - Success
-- Performing Test COMPILER_CXX_WORKS
-- Performing Test COMPILER_CXX_WORKS - Success
-- Storm - Using compiler configuration AppleClang 15.0.0.15000100.
-- Storm - Building external resources with 5 job(s) in parallel.
-- Storm - Including Eigen 3.4.0 commit b0eded878d5d162d61583a286c0d8a45406ad1bc.
-- Storm - Using workaround for Boost >= 1.81
-- Storm - Using boost 108400 (library version 1_84).
-- Storm - Including ExprTk.
-- Storm - Including Parallel Hashmap.
-- Storm - Including cpphoafparser 0.99.2
-- Storm - Including ModernJSON.
-- Storm - Linking with Z3 (version 4.12.2). (Z3 version supports optimization)
-- Storm - Using system version of glpk.
-- Storm - Linking with glpk 5.0
CMake Warning at resources/3rdparty/include_cudd.cmake:39 (message):
  There are some known issues compiling CUDD on some setups.  We implemented
  a workaround that mostly works, but if you still have problems compiling
  CUDD, especially if you do not use the default compiler of your system,
  please contact the Storm developers.
Call Stack (most recent call first):
  resources/3rdparty/CMakeLists.txt:287 (include)
  CMakeLists.txt:473 (include)

-- Storm - Linking with CUDD 3.0.0.
-- Storm - Found carl-storm version
-- Storm - Use system version of carl.
-- Storm - Linking with preinstalled carl 14.26 (include: /carl-storm/src, library lib_carl, CARL_USE_CLN_NUMBERS: OFF, CARL_USE_GINAC: OFF).
-- Storm - Use system version of xerces.
-- Storm (GSPN) - Linking with Xerces-c 3.2.4: /opt/homebrew/lib/libxerces-c.dylib
CMake Warning at resources/3rdparty/include_spot.cmake:23 (message):
  Storm - Could not find Spot.  Model checking of LTL formulas (beyond PCTL)
  will not be supported.  You may want to set cmake option
  STORM_USE_SPOT_SHIPPED to install Spot automatically.  If you already
  installed Spot, consider setting cmake option SPOT_ROOT.  Unset
  STORM_USE_SPOT_SYSTEM to silence this warning.
Call Stack (most recent call first):
  resources/3rdparty/CMakeLists.txt:581 (include)
  CMakeLists.txt:473 (include)

-- Storm - Using shipped version of sylvan.
-- Storm - Linking with sylvan.
-- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE) 
-- Storm - Version is 1.8.1 (version 1.8.1 + 0 commits), building from git: 3f74f3e59acfba3b61c686af01a864962d44af97 (dirty: DirtyState::Clean).
-- Registered with cmake
-- Configuring done (2.3s)
-- Generating done (0.4s)
-- Build files have been written to: /storm/build

[volkm]

Thanks. At first glance I do not see anything out of the ordinary. It could be that it is a problem with Boost. Can you go to the carl build directory and build the tests?

make
make test

[alebugariu]

Works well:

Running tests...
Test project /carl-storm/build
    Start 1: util
1/5 Test #1: util .............................   Passed    1.63 sec
    Start 2: numbers
2/5 Test #2: numbers ..........................   Passed    0.59 sec
    Start 3: core
3/5 Test #3: core .............................   Passed    0.36 sec
    Start 4: formula
4/5 Test #4: formula ..........................   Passed    0.17 sec
    Start 5: interval
5/5 Test #5: interval .........................   Passed    0.15 sec

100% tests passed, 0 tests failed out of 5

Total Test time (real) =   2.92 sec

[sjunges]

Hi, let me also add my suspicion:

For me this looks like as if sylvan is still linking with the carl version from home-brew: storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter.h:3: In file included from /storm/resources/3rdparty/sylvan/../../../src/storm/adapters/RationalFunctionAdapter_Private.h:8: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/FactorizedPolynomial.h:14: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/PolynomialFactorizationPair.h:307: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/PolynomialFactorizationPair.tpp:15: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/MultivariateGCD.h:11: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/MonomialOrdering.h:9: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/Term.h:10: In file included from /opt/homebrew/Cellar/carl-storm/14.25/include/carl/core/../interval/Interval.h:39: In file included from /opt/local/include/boost/numeric/interval.hpp:18: /opt/local/include/boost/numeric/interval/hw_rounding.hpp:42:4: error: Boost.Numeric.Interval: Please specify rounding control mechanism.

error Boost.Numeric.Interval: Please specify rounding control mechanism.

^ 1 error generated. make[5]: [src/CMakeFiles/sylvan.dir/sylvan_obj.cpp.o] Error 1 make[4]: [src/CMakeFiles/sylvan.dir/all] Error 2 make[3]: *** [all] Error 2 In particular, I think we have a problem that sylvan is not properly cleared when rebuilding… can you remove sylvan from your build folder/work from a clean build folder?

Best, Sebastian

On 19 Feb 2024, at 17:51, Alexandra-Olimpia BUGARIU @.***> wrote:

Works well:

Running tests... Test project /carl-storm/build Start 1: util 1/5 Test #1: util ............................. Passed 1.63 sec Start 2: numbers 2/5 Test #2: numbers .......................... Passed 0.59 sec Start 3: core 3/5 Test #3: core ............................. Passed 0.36 sec Start 4: formula 4/5 Test #4: formula .......................... Passed 0.17 sec Start 5: interval 5/5 Test #5: interval ......................... Passed 0.15 sec

100% tests passed, 0 tests failed out of 5

Total Test time (real) = 2.92 sec

— Reply to this email directly, view it on GitHub https://github.com/moves-rwth/storm/issues/502#issuecomment-1952869095, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADH67DA4RXGK5TAFQ4SL7RLYUN7HTAVCNFSM6AAAAABDPTH6X6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNJSHA3DSMBZGU. You are receiving this because you are subscribed to this thread.

[alebugariu]

Thank you, Sebastian, but unfortunately this does not solve the problem.