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