Extend STP_STUB and YICES_STUB flag

src/vendor/stp/Makefile

@@ -5,25 +5,77 @@ PREFIX?=$(TOP)/inst
 
 .PHONY: all install clean full_clean
 
-ifeq ($(STP_STUB),)
-SRC = src
-else
-SRC = src_stub
+ifneq ($(STP_STUB),) # STP_STUB didn't work for 3 years anyway
+$(error STP_STUB is deprecated: Use STP_USE_LIB=disable instead)
+endif
+
+ifeq ($(STP_USE_LIB),) # use default
+STP_USE_LIB=included
 endif
 
+define ispath
+$(shell echo "$1" | grep -E "^/*")
+endef
+
 ifeq ($(OSTYPE), Darwin)
-SNAME=libstp.dylib
+SO=dylib
 else
-SNAME=libstp.so.1
+SO=so
 endif
 
+ifeq ($(STP_USE_LIB),included)      # compile from provided source
+    SRC = src
+    ifeq ($(OSTYPE), Darwin)
+        SNAME=libstp_incl.dylib
+    else
+        SNAME=libstp_incl.so.1
+    endif
+else ifeq ($(STP_USE_LIB),disable)  # disable STP
+    SRC = src_stub
+    SNAME=libstp_disabled.$(SO)
+else ifeq ($(STP_USE_LIB),placeholder)  # use stub to be replaced by real library later
+    SRC = src_stub
+    SNAME=libstp.$(SO)
+else ifeq ($(STP_USE_LIB),system)   # use system STP
+    SRC = src_sys
+    ifeq ($(OSTYPE), Darwin)
+        SNAME=libstp_sys.dylib
+        STP_LIBPATH = /usr/local/opt/stp@
+    else # Linux
+        SNAME=libstp_sys.so
+        STP_LIBPATH=$(shell find /usr/lib/ -name "libstp.so*" -type f -print0 | tr '\0' '\n' | grep "/[a-z0-9.]*$$" | head -n 1)
+        ifeq ($(STP_LIBPATH),)
+            $(error No valid library found in /usr/lib)
+        endif
+    endif
+    export STP_LIBPATH
+else ifneq ($(call ispath,"$(STP_USE_LIB)"),) # use STP at the absolute path provided by STP_USE_LIB
+    SRC = src_sys
+    SNAME=libstp_custom.$(SO)
+    STP_LIBPATH = $(STP_USE_LIB)
+    export STP_LIBPATH
+else # unknown option for STP_USE_LIB
+    $(error Unknown option for STP_USE_LIB: $(STP_USE_LIB))
+endif
+export SNAME
+
 all: install
 
 install:
 	$(MAKE) -C $(SRC) install
 	ln -fsn HaskellIfc include_hs
+	@# necessary for bsc linker (src/comp/Makefile:51)
+	ln -s "$(SNAME)" lib/libstp.$(SO) || true
+# put self-compiled library in path where it can be found at runtime
+ifeq ($(STP_USE_LIB), $(findstring $(STP_USE_LIB), included disable placeholder))
 	install -m 755 -d $(PREFIX)/lib/SAT
-	install -m 644 lib/$(SNAME) $(PREFIX)/lib/SAT
+	install -m 644 "lib/$(SNAME)" $(PREFIX)/lib/SAT
+endif
+# make it obvious that the library is a placeholder
+ifeq ($(STP_USE_LIB), $(findstring $(STP_USE_LIB), placeholder))
+	mv "$(PREFIX)/lib/SAT/$(SNAME)" libstp_placeholder.$(SO)
+	ln -s libstp_placeholder.$(SO) "$(PREFIX)/lib/SAT/$(SNAME)"
+endif
 
 clean:
 	$(MAKE) -C $(SRC) clean

src/vendor/stp/src/Makefile

@@ -14,13 +14,7 @@ else
 CP = cp -df
 endif
 
-ifeq ($(OSTYPE), Darwin)
-LIBRARIES=lib/libstp.dylib
-SNAME = libstp.dylib
-else
-LIBRARIES=lib/libstp.so.1 lib/libstp.so
-SNAME = libstp.so.1
-endif
+LIBRARIES=lib/$(SNAME)
 
 .PHONY: all
 all: $(LIBRARIES)
@@ -72,12 +66,6 @@ lib/$(SNAME):  c_interface/c_interface.o \
 	@# We use --whole-archive to ensure that all symbols in to-sat are used
 	$(CXX) $(CFLAGS) $(SHAREDFLAG)  -Wl,$(SONAMEFLAG),$(SNAME) -o $@ $(LIBCCARGS)
 
-ifneq ($(OSTYPE), Darwin)
-lib/libstp.so: lib/libstp.so.1
-	-rm -f $@
-	(cd lib; ln -s libstp.so.1 libstp.so)
-endif
-
 
 # During the build of AST some classes are built that most of the other
 # classes depend upon. So in a parallel make, AST should be made first.

src/vendor/stp/src_stub/Makefile

@@ -10,9 +10,9 @@ LIB_DIR=../lib
 INC_DIR=../include
 
 ifeq ($(OSTYPE), Darwin)
-LDFLAGS = -dynamiclib -Wl,-install_name,libstp_stub.so
+LDFLAGS = -dynamiclib -Wl,-install_name,$(SNAME)
 else
-LDFLAGS = -shared -Wl,-soname,libstp_stub.so
+LDFLAGS = -shared -Wl,-soname,$(SNAME)
 endif
 
 .PHONY: all
@@ -21,18 +21,16 @@ all: install
 stp_stub.o: stp_stub.c stp_c_interface.h
 	$(CC) $(CFLAGS) -c -o $@ $<
 
-libstp_stub.so: stp_stub.o
+$(SNAME): stp_stub.o
 	$(CC) $(CFLAGS) $(LDFLAGS) -o $@ $<
 
-libstp.so: libstp_stub.so
+libstp.so: $(SNAME)
 	$(RM) $@
 	ln -s $< $@
 
-install: libstp_stub.so
+install: $(SNAME)
 	mkdir -p $(LIB_DIR)
-	$(CP) libstp_stub.so $(LIB_DIR)/
-	ln -fsn libstp.so.1 $(LIB_DIR)/libstp.so
-	ln -fsn libstp_stub.so $(LIB_DIR)/libstp.so.1
+	$(CP) $(SNAME) $(LIB_DIR)/
 	mkdir -p $(INC_DIR)
 	$(CP) stp_c_interface.h $(INC_DIR)/
 

src/vendor/stp/src_sys/Makefile

@@ -0,0 +1,35 @@
+PWD:=$(shell pwd)
+TOP:=$(PWD)/../../../..
+
+include $(TOP)/platform.mk
+
+RM ?= rm -rf
+CP ?= cp
+
+LIB_DIR=../lib
+INC_DIR=../include
+
+.PHONY: all
+all: install
+
+
+$(SNAME):
+	$(CP) "$(STP_LIBPATH)" ./$(SNAME)
+
+install: $(SNAME)
+	mkdir -p $(LIB_DIR)
+	$(CP) $(SNAME) $(LIB_DIR)/
+	mkdir -p $(INC_DIR)
+	$(CP) stp_c_interface.h $(INC_DIR)/
+
+.PHONY: clean full_clean
+
+clean:
+	$(RM) *.o *.so
+
+full_clean: clean
+	$(RM) -R $(LIB_DIR)
+	$(RM) -R $(INC_DIR)
+
+
+