Load SAT libs from dir relative to exe using linker flags

src/comp/Makefile

@@ -55,6 +55,14 @@ YICES_HS = ../vendor/yices/include_hs
 YICES_INC_FLAGS = -I../vendor/yices/include
 YICES_LIB_FLAGS = -L../vendor/yices/lib -lyices
 
+# Set the linker flags so ld.so searches for shared libraries in lib/SAT
+# dir in the install.
+ifeq ($(OSTYPE), Darwin)
+SAT_LINK_FLAGS=-optl '-Wl,-rpath,@executable_path/../../lib/SAT'
+else
+SAT_LINK_FLAGS=-optl '-Wl,-rpath,$$ORIGIN/../../lib/SAT'
+endif
+
 # HTCL
 HTCL_HS = ../vendor/htcl
 HTCL_INC_FLAGS = -L$(HTCL_HS)
@@ -280,6 +288,7 @@ POSTBUILDCOMMAND = $(BUILDDONE)
 BSC_BUILDLIBS = \
 	$(STP_LIB_FLAGS) \
 	$(YICES_LIB_FLAGS) \
+	$(SAT_LINK_FLAGS) \
 
 BLUETCL_BUILDLIBS = \
 	$(BSC_BUILDLIBS) \

src/comp/wrapper.sh

@@ -10,16 +10,6 @@ BINDIR=`dirname "${ABSNAME}"`
 BLUESPECDIR="$(cd ${BINDIR}/../lib; pwd -P)"
 export BLUESPECDIR
 
-# Add the dynamically-linked SAT libraries to the load path
-if [ -n "$BLUESPEC_LD_LIBRARY_PATH" ] ; then
-    LD_LIBRARY_PATH=${BLUESPEC_LD_LIBRARY_PATH}:${LD_LIBRARY_PATH}
-    DYLD_LIBRARY_PATH=${BLUESPEC_LD_LIBRARY_PATH}:${DYLD_LIBRARY_PATH}
-fi
-LD_LIBRARY_PATH=${LD_LIBRARY_PATH}:${BLUESPECDIR}/SAT
-DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH}:${BLUESPECDIR}/SAT
-export LD_LIBRARY_PATH
-export DYLD_LIBRARY_PATH
-
 # Determine the actual executable to run
 BLUESPECEXEC=${BINDIR}/core/${SCRIPTNAME}
 

src/vendor/stp/src/Makefile

@@ -11,10 +11,14 @@ HEADERS=c_interface/*.h
 ifeq ($(OSTYPE), Darwin)
 LIBRARIES=lib/libstp.dylib
 SNAME = libstp.dylib
+# When linked into a binary, use this 'install_name'. @rpath makes library
+# be loaded relative to the rpath baked into the binary.
+INAME = @rpath/$(SNAME)
 CP = cp -Rf
 else
 LIBRARIES=lib/libstp.so.1 lib/libstp.so
 SNAME = libstp.so.1
+INAME = $(SNAME)
 CP = cp -df
 endif
 
@@ -66,7 +70,7 @@ lib/$(SNAME):  c_interface/c_interface.o \
 	@# For some reason, this line doesn't work
 	@# $(CXX) $(CFLAGS) $(SHAREDFLAG) -o $@ $^
 	@# We use --whole-archive to ensure that all symbols in to-sat are used
-	$(CXX) $(CFLAGS) $(SHAREDFLAG)  -Wl,$(SONAMEFLAG),$(SNAME) -o $@ $(LIBCCARGS)
+	$(CXX) $(CFLAGS) $(SHAREDFLAG)  -Wl,$(SONAMEFLAG),$(INAME) -o $@ $(LIBCCARGS)
 
 ifneq ($(OSTYPE), Darwin)
 lib/libstp.so: lib/libstp.so.1

src/vendor/yices/v2.6/Makefile

@@ -14,14 +14,14 @@ ifeq ($(OSTYPE), Darwin)
 #    the absolute install path. For cases where yices knows the correct
 #    install path of the library, this makes sense, but for bsc, we don't want
 #    this, as we're going to eventually install this in a separate directory
-#    of our own.
+#    of our own controlled by the binary's @rpath.
 # 2. libyices.2.dylib dynamically links against ligmp, which probably comes
 #    from Homebrew. We don't want this, because this makes our installation
 #    depend on Homebrew. Instead, statically link libgmp into libyices.
 #    Note that we must statically link by using the archive file as Apple's ld
 #    doesn't understand -Bstatic.
 LIBGMPA=$(shell pkg-config --variable=libdir gmp)/libgmp.a
-BUILD_ARGS=libyices_install_name=libyices.2.dylib LIBS=$(LIBGMPA)
+BUILD_ARGS=libyices_install_name=@rpath/libyices.2.dylib LIBS=$(LIBGMPA)
 endif
 
 .PHONY: all
@@ -33,7 +33,7 @@ ifeq ($(YICES_STUB),)
 	(cd $(YICES_SRC) ; \
 		autoconf ; \
 		./configure --prefix=$(YICES_INST) ; \
-		$(MAKE) $(BUILD_ARGS); \
+		$(MAKE) $(BUILD_ARGS) ; \
 		$(MAKE) install \
 		)
 else

src/vendor/yices/v2.6/stub/Makefile

@@ -26,8 +26,15 @@ HEADERS = \
 
 FULLVER = $(VER).$(SUBVER)
 
+ifeq ($(OSTYPE), Darwin)
+SNAME = $(LIBNAME).$(VER).dylib
+FULLNAME = $(LIBNAME).$(FULLVER).dylib
+NOVERNAME = $(LIBNAME).dylib
+else
 SNAME = $(LIBNAME).so.$(VER)
 FULLNAME = $(LIBNAME).so.$(FULLVER)
+NOVERNAME = $(LIBNAME).so
+endif
 OBJECTS = $(addsuffix .o, $(basename $(SRC)))
 
 # -------------------------
@@ -50,20 +57,24 @@ endif
 ifeq ($(OSTYPE), Darwin)
 SHAREDFLAG = -dynamiclib
 SONAMEFLAG = -install_name
+# When linked into a binary, use this 'install_name'. @rpath makes library
+# be loaded relative to the rpath baked into the binary.
+INAME = @rpath/$(SNAME)
 else
 SHAREDFLAG = -shared
 SONAMEFLAG = -soname
+INAME = $(SNAME)
 endif
 
 # -------------------------
 
 all: $(FULLNAME)
 	ln -sf $< $(SNAME)
-	ln -sf $< $(LIBNAME).so
+	ln -sf $< $(NOVERNAME)
 
 
 $(FULLNAME): $(OBJECTS)
-	$(CC) $(SHAREDFLAG) -Wl,$(SONAMEFLAG),$(SNAME) -o $@ $<
+	$(CC) $(SHAREDFLAG) -Wl,$(SONAMEFLAG),$(INAME) -o $@ $<
 
 
 $(LIBNAME).a:	$(OBJECTS)
@@ -75,14 +86,14 @@ $(LIBNAME).a:	$(OBJECTS)
 
 install: all
 	mkdir -p $(YICES_INST)/lib
-	$(CP) $(FULLNAME) $(SNAME) $(LIBNAME).so  $(YICES_INST)/lib/
+	$(CP) $(FULLNAME) $(SNAME) $(NOVERNAME)  $(YICES_INST)/lib/
 	mkdir -p $(YICES_INST)/include
 	$(CP) $(HEADERS) $(YICES_INST)/include/
 
 .PHONY: clean full_clean
 
 clean:
-	$(RM) *.o $(FULLNAME) $(SNAME) $(LIBNAME).so
+	$(RM) *.o $(FULLNAME) $(SNAME) $(NOVERNAME)
 
 full_clean: clean
 	$(RM) $(YICES_INST)/lib