Project

General

Profile

Revision ad4774b0 configure.ac

View differences:

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