Revision ad4774b0 configure.ac
| configure.ac | ||
|---|---|---|
| 55 | 55 |
|
| 56 | 56 |
# Checks for libraries. |
| 57 | 57 |
# OCamlgraph |
| 58 |
AC_MSG_CHECKING(ocaml libraries required)
|
|
| 58 |
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num))
|
|
| 59 | 59 |
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1], |
| 60 | 60 |
[],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)], |
| 61 | 61 |
) |
| ... | ... | |
| 67 | 67 |
[yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)], |
| 68 | 68 |
) |
| 69 | 69 |
|
| 70 |
# Seal |
|
| 71 |
AC_MSG_CHECKING(seal library (optional)) |
|
| 72 |
AS_IF([ocamlfind query seal >/dev/null 2>&1], |
|
| 73 |
[seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)], |
|
| 74 |
) |
|
| 75 |
AS_IF([test "x$seal" = "xyes"], [ |
|
| 76 |
AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);") |
|
| 77 |
AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)") |
|
| 78 |
]) |
|
| 79 |
|
|
| 80 |
# z3 |
|
| 81 |
AC_MSG_CHECKING(z3 library (optional)) |
|
| 82 |
AS_IF([ocamlfind query z3 >/dev/null 2>&1], |
|
| 83 |
[z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)], |
|
| 84 |
) |
|
| 85 |
AS_IF([test "x$z3" = "xyes"], [ |
|
| 86 |
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);") |
|
| 87 |
AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)") |
|
| 88 |
]) |
|
| 89 |
|
|
| 90 |
# Tiny |
|
| 91 |
AC_MSG_CHECKING(tiny library (optional)) |
|
| 92 |
AS_IF([ocamlfind query tiny >/dev/null 2>&1], |
|
| 93 |
[tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)], |
|
| 94 |
) |
|
| 95 |
AS_IF([test "x$tiny" = "xyes"], [ |
|
| 96 |
AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);") |
|
| 97 |
AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)") |
|
| 98 |
]) |
|
| 99 |
|
|
| 70 | 100 |
# Salsa |
| 71 | 101 |
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa], |
| 72 | 102 |
[disable Salsa plugin. Enabled by default if available.])]) |
| ... | ... | |
| 79 | 109 |
|
| 80 | 110 |
AS_IF([test "x$enable_salsa" != "xno"], [ |
| 81 | 111 |
if (test "x$salsa" = xyes ); then |
| 82 |
AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.PluginType);")
|
|
| 112 |
AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
|
|
| 83 | 113 |
AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)") |
| 84 | 114 |
fi |
| 85 | 115 |
]) |
| ... | ... | |
| 156 | 186 |
src/Makefile |
| 157 | 187 |
src/version.ml |
| 158 | 188 |
src/pluginList.ml |
| 189 |
src/verifierList.ml |
|
| 159 | 190 |
src/_tags |
| 160 | 191 |
src/ocaml_utils.ml |
| 161 | 192 |
]) |
| ... | ... | |
| 190 | 221 |
AC_MSG_NOTICE([lustresf not available]) |
| 191 | 222 |
fi |
| 192 | 223 |
fi |
| 224 |
AC_MSG_NOTICE(******** Verifiers ********) |
|
| 225 |
|
|
| 226 |
if (test "x$seal" = "xyes"); then |
|
| 227 |
AC_MSG_NOTICE([Seal enabled]) |
|
| 228 |
else |
|
| 229 |
AC_MSG_NOTICE([Seal disabled. Require Seal library]) |
|
| 230 |
fi |
|
| 231 |
|
|
| 232 |
if (test "x$z3" = xyes); then |
|
| 233 |
AC_MSG_NOTICE([Zustre enabled]) |
|
| 234 |
else |
|
| 235 |
AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library]) |
|
| 236 |
fi |
|
| 237 |
|
|
| 238 |
if (test "x$tiny" = xyes); then |
|
| 239 |
AC_MSG_NOTICE([Tiny enabled]) |
|
| 240 |
else |
|
| 241 |
AC_MSG_NOTICE([Tiny disabled. Require Tiny library]) |
|
| 242 |
fi |
|
| 193 | 243 |
|
| 194 | 244 |
AC_MSG_NOTICE(****** Regression Tests ******) |
| 195 | 245 |
if (test "x$valid_test_path" = xfalse); then |
Also available in: Unified diff