From 0eb7a7bebdfca7c3e9773c3a482c429f0b99d83c Mon Sep 17 00:00:00 2001 From: smccam Date: Fri, 31 Oct 2008 18:45:04 +0000 Subject: [PATCH] Remove from SVN files that are automatically generated in the configure and build processes. Copy the changes to Makefile back to the original Makefile.in. After this change, you'll need to re-run "configure". git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@35 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile | 145 --------------------------------------------- Makefile.in | 39 +++++++++--- config.info | 1 - sat/core/depend.mk | 16 ----- 4 files changed, 31 insertions(+), 170 deletions(-) delete mode 100644 Makefile delete mode 100644 config.info delete mode 100644 sat/core/depend.mk diff --git a/Makefile b/Makefile deleted file mode 100644 index abd8739..0000000 --- a/Makefile +++ /dev/null @@ -1,145 +0,0 @@ - # STP (Simple Theorem Prover) top level makefile - # - # To make in debug mode, type 'make "CLFAGS=-ggdb" - # To make in optimized mode, type 'make "CFLAGS=-O2" - - -include Makefile.common config.info - -BIN_DIR=$(PREFIX)/bin -LIB_DIR=$(PREFIX)/lib -INCLUDE_DIR=$(PREFIX)/include/stp - -BINARIES=bin/stp -LIBRARIES=lib/libstp.a -HEADERS=c_interface/*.h - -# NB: the TAGS target is a hack to get around this recursive make nonsense -# we want all the source and header files generated before we make tags -.PHONY: all -all: - $(MAKE) -C AST - $(MAKE) -C sat/core lib - $(MAKE) -C simplifier - $(MAKE) -C bitvec - $(MAKE) -C c_interface - $(MAKE) -C constantbv - $(MAKE) -C parser - $(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o - $(RANLIB) libstp.a - @mkdir -p lib - @mv libstp.a lib/ -# $(MAKE) TAGS - @echo "" - @echo "Compilation successful." - @echo "Type 'make install' to install STP." - - -.PHONY: install -install: all - @cp -f $(BINARIES) $(BIN_DIR) - @cp -f $(LIBRARIES) $(LIB_DIR) - @cp -f $(HEADERS) $(INCLUDE_DIR) - @echo "STP installed successfully." - -.PHONY: clean -clean: - rm -rf *~ - rm -rf *.a - rm -rf lib/*.a - rm -rf test/*~ - rm -rf bin/*~ - rm -rf bin/stp - rm -rf *.log - #rm -rf Makefile - #rm -rf config.info - rm -f TAGS - $(MAKE) clean -C AST - $(MAKE) clean -C sat/core - $(MAKE) clean -C simplifier - $(MAKE) clean -C bitvec - $(MAKE) clean -C parser - $(MAKE) clean -C c_interface - $(MAKE) clean -C constantbv - -# this is make way too difficult because of the recursive Make junk, it -# should be removed -TAGS: FORCE - find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags - - -FORCE: - -# The higher the level, the more tests are run (3 = all) -REGRESS_TESTS0 = test \ - test/EGT -REGRESS_LEVEL=4 -REGRESS_TESTS=$(REGRESS_TESTS0) -REGRESS_LOG = `date +%Y-%m-%d`"-regress.log" -PROGNAME=bin/stp -ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) - -.PHONY: regress -regress: - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - -# The higher the level, the more tests are run (3 = all) -REGRESS_TESTS0 = test \ - test/EGT -REGRESS_LEVEL=4 -REGRESS_TESTS=$(REGRESS_TESTS0) -#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log" -PROGNAME=bin/stp -ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) - -.PHONY: regressbigarray -regressbigarray: - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - bin/run_bigarray_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - -.PHONY: regressall -regressall: - $(MAKE) install - $(MAKE) regress - -GRIND_LOG = `date +%Y-%m-%d`"-grind.log" -GRINDPROG = valgrind --leak-check=full --undef-value-errors=no -GRIND_TAR = $(BIN_DIR)/stp -d -GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" -GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS) - - -.PHONY: grind -grind: - - $(MAKE) install CFLAGS="-ggdb -pg -g" - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - @echo "Starting tests at" `date` | tee -a $(GRIND_LOG) - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - bin/run_tests $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - @echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG) - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - diff --git a/Makefile.in b/Makefile.in index ae13078..e9ab2a3 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1,6 +1,6 @@ # STP (Simple Theorem Prover) top level makefile # - # To make in debug mode, type 'make "CLFAGS=-ggdb" + # To make in debug mode, type 'make "CFLAGS=-ggdb" # To make in optimized mode, type 'make "CFLAGS=-O2" @@ -19,13 +19,13 @@ HEADERS=c_interface/*.h .PHONY: all all: $(MAKE) -C AST - $(MAKE) -C sat + $(MAKE) -C sat/core lib $(MAKE) -C simplifier $(MAKE) -C bitvec $(MAKE) -C c_interface $(MAKE) -C constantbv $(MAKE) -C parser - $(AR) rc libstp.a AST/*.o sat/*.o simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o + $(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ @@ -34,6 +34,7 @@ all: @echo "Compilation successful." @echo "Type 'make install' to install STP." + .PHONY: install install: all @cp -f $(BINARIES) $(BIN_DIR) @@ -50,11 +51,11 @@ clean: rm -rf bin/*~ rm -rf bin/stp rm -rf *.log - rm -rf Makefile - rm -rf config.info + #rm -rf Makefile + #rm -rf config.info rm -f TAGS $(MAKE) clean -C AST - $(MAKE) clean -C sat + $(MAKE) clean -C sat/core $(MAKE) clean -C simplifier $(MAKE) clean -C bitvec $(MAKE) clean -C parser @@ -84,8 +85,30 @@ regress: @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) -# bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - bin/run_tests $(ALL_OPTIONS) 2>&1 | grep -v "ulimit" | grep -v "elapsed" | grep -v "swaps" | tee -a $(REGRESS_LOG); + bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + +# The higher the level, the more tests are run (3 = all) +REGRESS_TESTS0 = test \ + test/EGT +REGRESS_LEVEL=4 +REGRESS_TESTS=$(REGRESS_TESTS0) +#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log" +PROGNAME=bin/stp +ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) + +.PHONY: regressbigarray +regressbigarray: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + bin/run_bigarray_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) diff --git a/config.info b/config.info deleted file mode 100644 index 75dc56b..0000000 --- a/config.info +++ /dev/null @@ -1 +0,0 @@ -PREFIX=/Users/katelman/Work/projects/stp/svn/stp-fast-prover/trunk/stp diff --git a/sat/core/depend.mk b/sat/core/depend.mk deleted file mode 100644 index 4320d89..0000000 --- a/sat/core/depend.mk +++ /dev/null @@ -1,16 +0,0 @@ -Main.o: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h -Solver.o: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h -Main.op: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h -Solver.op: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h -Main.od: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h -Solver.od: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h -Main.or: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h -Solver.or: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ - ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h -- 2.47.3