Revision 57d61d67
Added by Pierre-Loïc Garoche over 6 years ago
configure.ac | ||
---|---|---|
77 | 77 |
AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)") |
78 | 78 |
]) |
79 | 79 |
|
80 |
# z3 |
|
81 |
AC_MSG_CHECKING(z3 library (optional)) |
|
82 |
define([z3path], esyscmd([ocamlfind query Z3 | tr -d '\n'])) |
|
80 |
# z3 (optional) |
|
81 |
|
|
82 |
# option to rely on github version if installed |
|
83 |
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github], |
|
84 |
[Rely on Z3 as distributed by the official github |
|
85 |
repo rather then the opam distribution. Disabled by default.])]) |
|
86 |
|
|
87 |
AS_IF([test "x$with_z3_github" != "xyes"], |
|
88 |
[z3name=z3], |
|
89 |
[z3name=Z3] |
|
90 |
) |
|
91 |
|
|
92 |
AC_MSG_CHECKING(z3 library) |
|
93 |
|
|
94 |
|
|
95 |
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n'])) |
|
83 | 96 |
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n'])) |
84 | 97 |
|
85 |
AS_IF([ocamlfind query Z3 >/dev/null 2>&1],
|
|
86 |
[z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
|
|
98 |
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
|
|
99 |
[z3=yes; AC_MSG_RESULT([yes])],[seal=no; AC_MSG_RESULT(no)],
|
|
87 | 100 |
) |
88 | 101 |
AS_IF([test "x$z3" = "xyes"], [ |
89 | 102 |
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);") |
90 |
AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(Z3)") |
|
91 |
AC_SUBST(Z3LIBPATH, "z3path") |
|
103 |
AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)") |
|
104 |
AS_IF([test "x$z3name" = "xZ3"], |
|
105 |
[define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n'])) |
|
106 |
AC_SUBST(Z3LIBPATH, "Z3path")], |
|
107 |
[define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n'])) |
|
108 |
AC_SUBST(Z3LIBPATH, "z3path")] |
|
109 |
) |
|
92 | 110 |
]) |
93 | 111 |
|
94 | 112 |
|
... | ... | |
244 | 262 |
if (test "x$z3" = xyes); then |
245 | 263 |
AC_MSG_NOTICE([Zustre enabled]) |
246 | 264 |
AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.) |
247 |
AC_MSG_WARN(It is currently located in "z3path") |
|
265 |
dnl AC_MSG_WARN(It is currently located in "z3path")
|
|
248 | 266 |
AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc") |
249 | 267 |
AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc) |
250 | 268 |
else |
Also available in: Unified diff
New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation