From c5de2e9715182efd62701ada94f7f9081130a844 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 14 Mar 2018 19:50:10 -0700
Subject: [PATCH] Add the script to update LD_LIBRARY_PATH for z3
---
configure.ac | 13 ++++++++++++-
include/z3librc.in | 1 +
2 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 include/z3librc.in
diff --git a/configure.ac b/configure.ac
index 5a253935..886ca896 100644
--- a/configure.ac
+++ b/configure.ac
@@ -79,14 +79,20 @@ AS_IF([test "x$seal" = "xyes"], [
# z3
AC_MSG_CHECKING(z3 library (optional))
+define([z3path], esyscmd([ocamlfind query z3]))
+
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
[z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
)
AS_IF([test "x$z3" = "xyes"], [
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)")
+ AC_SUBST(Z3LIBPATH, "z3path")
])
+
+
+
# Tiny
AC_MSG_CHECKING(tiny library (optional))
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
@@ -189,6 +195,7 @@ AC_CONFIG_FILES([Makefile
src/verifierList.ml
src/_tags
src/ocaml_utils.ml
+ include/z3librc
])
AC_OUTPUT
@@ -231,7 +238,11 @@ AC_MSG_NOTICE(******** Verifiers ********)
if (test "x$z3" = xyes); then
AC_MSG_NOTICE([Zustre enabled])
- else
+ AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.)
+ AC_MSG_WARN(It is currently located in "z3path")
+ AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
+ AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
+else
AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
fi
diff --git a/include/z3librc.in b/include/z3librc.in
new file mode 100644
index 00000000..ee37a372
--- /dev/null
+++ b/include/z3librc.in
@@ -0,0 +1 @@
+export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:@Z3LIBPATH@
\ No newline at end of file
--
GitLab