I have installed Z3 on my computer (Mac with m1 chip) by running:
brew install z3
I am trying to install the z3 binding for Haskell.
On the library website, it is written:
Installation:
1) Install a Z3 4.x release. (Support for Z3 3.x is provided by the 0.3.2 version of these bindings.)
2) Just type cabal install z3 if you used the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include).
Otherwise use the --extra-lib-dirs and --extra-include-dirs Cabal flags when installing.
So I have done step 1, and in step 2, I type cabal install z3 which I get an error. I ran "find /opt/homebrew -name "z3.h" 2>/dev/null" in my terminal and got the following
/opt/homebrew/include/z3.h
/opt/homebrew/Cellar/z3/4.12.2/include/z3.h
I don't know why I have two headers to be honest and similarly I got the paths for the lib
/opt/homebrew/lib/libz3.4.12.dylib
/opt/homebrew/lib/libz3.4.12.2.0.dylib
/opt/homebrew/lib/libz3.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.2.0.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.dylib
So when I try either of the following
stack install z3 --extra-lib-dirs=/opt/homebrew/lib --extra-include-dirs=/opt/homebrew/include
OR
stack install z3 --extra-lib-dirs=/opt/homebrew/Cellar/z3/4.12.2/lib --extra-include-dirs=/opt/homebrew/Cellar/z3/4.12.2/include
I get an error:
z3> configure
z3> Configuring z3-408.2...
z3> build
z3> Preprocessing library for z3-408.2..
z3> compiling .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.c failed (exit code 1)
z3> rsp file was: ".stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/hsc2hscall47771-0.rsp"
z3> command was: /usr/bin/gcc -c .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.c -o .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.o --target=arm64-apple-darwin --target=arm64-apple-darwin -Wl,-no_fixup_chains -D__GLASGOW_HASKELL__=904 -Ddarwin_BUILD_OS=1 -Daarch64_BUILD_ARCH=1 -Ddarwin_HOST_OS=1 -Daarch64_HOST_ARCH=1 -I/opt/homebrew/include -I/opt/homebrew/include -I.stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/autogen -I.stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/global-autogen -include .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/autogen/cabal_macros.h -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/base-4.17.2.0/include -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/ghc-bignum-1.3/include -I/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/ffi -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/rts-1.0.2/include -I/Users/mehradhq/.ghcup/ghc/9.4.7/include/
z3> error: clang: warning: -Wl,-no_fixup_chains: 'linker' input unused [-Wunused-command-line-argument]
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:45:10: note: expanded from macro 'hsc_const'
z3> if ((x) < 0) \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:46:41: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%lld", (long long)(x)); \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:48:50: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%llu", (unsigned long long)(x));
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:45:10: note: expanded from macro 'hsc_const'
z3> if ((x) < 0) \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:46:41: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%lld", (long long)(x)); \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:48:50: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%llu", (unsigned long long)(x));
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> 6 errors generated.
z3>
Error: [S-7282]
Stack failed to execute the build plan.
While executing the build plan, Stack encountered the error:
[S-7011]
While building package z3-408.2 (scroll up to its section to see the
error) using:
/Users/mehradhq/.stack/setup-exe-cache/aarch64-osx/Cabal-simple_6HauvNHV_3.8.1.0_ghc-9.4.7 --verbose=1 --builddir=.stack-work/dist/aarch64-osx/Cabal-3.8.1.0 build --ghc-options " -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
I do not know what this is saying. I also ran it with cabal just to see if it works but again got the following error:
Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
Resolving dependencies...
Build profile: -w ghc-9.4.7 -O1
In order, the following will be built (use -v for more details):
- hsc2hs-0.68.10 (exe:hsc2hs) (requires download & build)
- z3-408.2 (lib) (requires download & build)
Downloading hsc2hs-0.68.10
Downloaded hsc2hs-0.68.10
Downloading z3-408.2
Starting hsc2hs-0.68.10 (exe:hsc2hs)
Downloaded z3-408.2
Building hsc2hs-0.68.10 (exe:hsc2hs)
Installing hsc2hs-0.68.10 (exe:hsc2hs)
Completed hsc2hs-0.68.10 (exe:hsc2hs)
Starting z3-408.2 (lib)
Failed to build z3-408.2. The failure occurred during the configure step.
Build log ( /Users/mehradhq/.cabal/logs/ghc-9.4.7/z3-408.2-f9eabcb0.log ):
Configuring library for z3-408.2..
cabal-3.6.2.0: Missing dependency on a foreign library:
* Missing (or bad) header file: z3.h
* Missing (or bad) C library: z3
This problem can usually be solved by installing the system package that
provides this library (you may need the "-dev" version). If the library is
already installed but in a non-standard location then you can use the flags
--extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
library file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
If the header file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
cabal: Failed to build z3-408.2. See the build log above for details.
The error messages are much clearer but I have everything installed and have defined the paths. I also looked at the Segmentation fault in Z3 (Haskell) question. I tried both ways proposed in the responses, none of them work. Also I am running on:
The Glorious Glasgow Haskell Compilation System, version 9.4.7
The GHCup Haskell installer, version 0.1.19.4
stack Version 2.11.1
cabal-install version 3.6.2.0
Can someone please explain what is the problem and how to fix it? thank you in advance.
Just for the sake that someone else is trying to run Z3 binding with haskell on mac (with an arm processor) and gets the same errors, I will post the solution that has worked for me here. So basically, installing Z3 by executing the following command
brew install Z3
in the terminal will install Z3 for you - you can verify this by running Z3 --version. However, the problem is that the Z3 version is 4.12.* whereas the Z3 binding for Haskell only accepts a Z3 version of 4.8.. So this doesn't work to bind Haskell with Z3. Unfortunately, brew does not have version 4.8. of Z3 to install, therefore you cannot use brew for this. Before proceeding you can run brew uninstall Z3 to uninstall the Z3. Now go to the website https://github.com/Z3Prover/z3/releases/tag/z3-4.8.17 and download https://z3-4.8.17-arm64-osx-10.16.zip/. Then run "cabal install z3" with the flags --extra-include-dirs and --extra-lib-dirs referring to the z3 headers and libz3.* directory respectively. (for me this was cabal install z3 -v3 --extra-include-dirs=/Users/PATH/z3-4.8.17-arm64-osx-10.16/include --extra-lib-dirs=/Users/PATH/z3-4.8.17-arm64-osx-10.16/bin) Even when I ran this I got the error that Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports 'ghc' version < 9.4 hence I asked the question yesterday. If you have ghcup installed then just use ghcup install ghc X*. In the placeholder X specify that version of ghc then use ghc setup ghc X to make that version the working version of ghc. The reason is that you need an older version of ghc than 9.4 to install z3. After doing so, again run the command cabal install z3 with the flags and if it works, then it works. For me it didn't so logging the errors, I had to change the version of my LLVM using brew. My version was 17 but the cabal install z3 wanted a version between 9-13. So I installed version 12 (to install you need to use brew. You need to further unlink and link the new version. You can google it or just simply ask Chatgpt). Then if you run cabal install z3 and it still doesn't work like me do the following: !!!!!
sudo cp /Users/PATH/z3-4.8.17-arm64-osx-10.16/bin/libz3.dylib /usr/local/lib/
!!!!! Okay I am NOT going to suggest this and it is NOT recommended to copy it to lib manually for safety reasons. However, this works (and I really needed it). Again just run cabal install z3 -v3 --extra-include-dirs=/Users/PATH/z3-4.8.17-arm64-osx-10.16/include and all should work. Please note that the last problem is due to that apparently the --extra-lib-dirs flag doesn't recognize the directory. So I put the file in the lib directory manually. I hope this helps someone as it took me a long time to get the z3 with haskell binding to work. The SBV library is a good alternative but I have been told that it does not work good with quantification over arrays. I haven't experimented it myself though.