diff --git a/src/comp/Makefile b/src/comp/Makefile index 08ece9fea..b9b5bf307 100644 --- a/src/comp/Makefile +++ b/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) \ diff --git a/src/comp/wrapper.sh b/src/comp/wrapper.sh index 742c8fa51..1403509d8 100755 --- a/src/comp/wrapper.sh +++ b/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} diff --git a/src/vendor/stp/src/Makefile b/src/vendor/stp/src/Makefile index f803bb29d..e76826e50 100644 --- a/src/vendor/stp/src/Makefile +++ b/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 diff --git a/src/vendor/yices/v2.6/Makefile b/src/vendor/yices/v2.6/Makefile index 34a643fd3..42b209de5 100644 --- a/src/vendor/yices/v2.6/Makefile +++ b/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 diff --git a/src/vendor/yices/v2.6/stub/Makefile b/src/vendor/yices/v2.6/stub/Makefile index 44d5b47e2..1f155c69c 100644 --- a/src/vendor/yices/v2.6/stub/Makefile +++ b/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