Project

General

Profile

« Previous | Next » 

Revision 57d61d67

Added by Pierre-Loïc Garoche over 6 years ago

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

View differences:

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