From: smccam Date: Fri, 31 Oct 2008 18:45:04 +0000 (+0000) Subject: Remove from SVN files that are automatically generated in the X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0eb7a7bebdfca7c3e9773c3a482c429f0b99d83c;p=francis%2Fstp.git 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 --- 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