From e491c34a2d7508d47f0f23cfccecf6f4e46c601a Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Fri, 16 Nov 2018 16:56:24 -0800
Subject: [PATCH] Issues with linking Z3 on OSX
---
configure.ac | 6 ++----
include/z3librc.in | 1 +
src/_tags.in | 38 ++++++++++++++++++++------------------
3 files changed, 23 insertions(+), 22 deletions(-)
diff --git a/configure.ac b/configure.ac
index aaef5726..04d6ac0c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -108,7 +108,7 @@ AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
)
AS_IF([test "x$z3" = "xyes"], [
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
- AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)")
+ AC_SUBST(LUSTREV_Z3_TAG, "<**/*verifier.native> or <tools/zustre/*.ml> or <tools/zustre/*.mli>: package($z3name)")
AS_IF([test "x$z3name" = "xZ3"],
[define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
AC_SUBST(Z3LIBPATH, "Z3path")],
@@ -118,8 +118,6 @@ AS_IF([test "x$z3" = "xyes"], [
])
-
-
# Tiny
AC_MSG_CHECKING(tiny library (optional))
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
@@ -270,7 +268,7 @@ AC_MSG_NOTICE(******** Verifiers ********)
if (test "x$z3" = xyes); then
AC_MSG_NOTICE([Zustre enabled])
- AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.)
+ AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH in OSX).)
dnl 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)
diff --git a/include/z3librc.in b/include/z3librc.in
index ee0b231e..26843ee9 100644
--- a/include/z3librc.in
+++ b/include/z3librc.in
@@ -1 +1,2 @@
export LD_LIBRARY_PATH=@Z3LIBPATH@:$LD_LIBRARY_PATH
+export DYLD_LIBRARY_PATH=@Z3LIBPATH@:$DYLD_LIBRARY_PATH
diff --git a/src/_tags.in b/src/_tags.in
index 235bf568..98c554d9 100644
--- a/src/_tags.in
+++ b/src/_tags.in
@@ -29,27 +29,29 @@ true: bin_annot, color(always)
<**/.svn>: not_hygienic
# packages
-<**/*.native> : package(ocamlgraph)
+<**/*.native> or <**/*.ml{,i}> : package(num)
+<**/*.native> or <**/*.ml{,i}> : package(ocamlgraph)
+<**/*verifier.native> or <**/*.ml{,i}> : package(yojson)
+
<**/*.native> : use_str
<**/*.native> : use_unix
-<utils.*> : use_unix
-<**/*.native> : package(num)
-<**/*.ml> : package(logs)
-<**/*.native> : package(logs)
-<**/*.native> : package(yojson)
-<tools/zustre/zustre_cex.*> : package(yojson)
-<**/json_parser.ml> : package(yojson)
-<**/main_parse_json_file.*> : package(cmdliner)
-<**/main_parse_json_file.*> : package(fmt.tty)
-<**/main_parse_json_file.*> : package(fmt.cli)
-<**/main_parse_json_file.*> : package(logs.fmt)
-<**/main_parse_json_file.*> : package(logs.cli)
-<**/main_parse_json_file.*> : package(yojson)
-<**/test_*.*> : package(oUnit)
-<**/test_json*.*> : package(yojson)
-# Required for ocamldoc. Otherwise failed to build
-<**/*.ml{,i}>: package(ocamlgraph)
+# <**/*.ml> : package(logs)
+# <**/*.native> : package(logs)
+# <**/*.native> : package(yojson)
+# <tools/zustre/zustre_cex.*> : package(yojson)
+# <**/json_parser.ml> : package(yojson)
+# <**/main_parse_json_file.*> : package(cmdliner)
+# <**/main_parse_json_file.*> : package(fmt.tty)
+# <**/main_parse_json_file.*> : package(fmt.cli)
+# <**/main_parse_json_file.*> : package(logs.fmt)
+# <**/main_parse_json_file.*> : package(logs.cli)
+# <**/main_parse_json_file.*> : package(yojson)
+# <**/test_*.*> : package(oUnit)
+# <**/test_json*.*> : package(yojson)
+
+# # Required for ocamldoc. Otherwise failed to build
+# <**/*.ml{,i}>: package(ocamlgraph)
# Plugin dependencies
@SALSA_TAG@
--
GitLab