fix some build dependencies in options-building; should fix a strange bug Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be

2 files changed, 97 insertions, 41 deletions

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index e1cd721f3..088c972b3 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -1,23 +1,45 @@
+OPTIONS_FILES_SRCS = \
+	base_options.cpp \
+	base_options.h \
+	../expr/options.cpp \
+	../expr/options.h \
+	../theory/booleans/options.cpp \
+	../theory/booleans/options.h \
+	../theory/options.cpp \
+	../theory/options.h \
+	../theory/bv/options.cpp \
+	../theory/bv/options.h \
+	../theory/datatypes/options.cpp \
+	../theory/datatypes/options.h \
+	../theory/builtin/options.cpp \
+	../theory/builtin/options.h \
+	../theory/arith/options.cpp \
+	../theory/arith/options.h \
+	../theory/uf/options.cpp \
+	../theory/uf/options.h \
+	../theory/arrays/options.cpp \
+	../theory/arrays/options.h \
+	../theory/quantifiers/options.cpp \
+	../theory/quantifiers/options.h \
+	../theory/rewriterules/options.cpp \
+	../theory/rewriterules/options.h \
+	../prop/options.cpp \
+	../prop/options.h \
+	../proof/options.cpp \
+	../proof/options.h \
+	../printer/options.cpp \
+	../printer/options.h \
+	../smt/options.cpp \
+	../smt/options.h \
+	../decision/options.cpp \
+	../decision/options.h \
+	../main/options.cpp \
+	../main/options.h \
+	../parser/options.cpp \
+	../parser/options.h
+
 OPTIONS_FILES = \
-	options/base_options \
-	expr/options \
-	theory/booleans/options \
-	theory/options \
-	theory/bv/options \
-	theory/datatypes/options \
-	theory/builtin/options \
-	theory/arith/options \
-	theory/uf/options \
-	theory/arrays/options \
-	theory/quantifiers/options \
-	theory/rewriterules/options \
-	prop/options \
-	proof/options \
-	printer/options \
-	smt/options \
-	decision/options \
-	main/options \
-	parser/options
+	$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
 
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
@@ -34,35 +56,65 @@ liboptions_la_SOURCES = \
 nodist_liboptions_la_SOURCES = \
 	options.cpp \
 	options_holder.h \
-	$(OPTIONS_FILES:%=../%.cpp) \
-	$(OPTIONS_FILES:%=../%.h)
-nodist_liboptions_la_OBJECTS = \
-	$(patsubst %.cpp,%.lo,$(filter %.cpp,$(nodist_liboptions_la_SOURCES)))
-
-BUILT_SOURCES = \
-	options.cpp \
-	options_holder.h \
 	base_options.cpp \
 	base_options.h \
+	../expr/options.cpp \
+	../expr/options.h \
+	../theory/booleans/options.cpp \
+	../theory/booleans/options.h \
+	../theory/options.cpp \
+	../theory/options.h \
+	../theory/bv/options.cpp \
+	../theory/bv/options.h \
+	../theory/datatypes/options.cpp \
+	../theory/datatypes/options.h \
+	../theory/builtin/options.cpp \
+	../theory/builtin/options.h \
+	../theory/arith/options.cpp \
+	../theory/arith/options.h \
+	../theory/uf/options.cpp \
+	../theory/uf/options.h \
+	../theory/arrays/options.cpp \
+	../theory/arrays/options.h \
+	../theory/quantifiers/options.cpp \
+	../theory/quantifiers/options.h \
+	../theory/rewriterules/options.cpp \
+	../theory/rewriterules/options.h \
+	../prop/options.cpp \
+	../prop/options.h \
+	../proof/options.cpp \
+	../proof/options.h \
+	../printer/options.cpp \
+	../printer/options.h \
+	../smt/options.cpp \
+	../smt/options.h \
+	../decision/options.cpp \
+	../decision/options.h \
+	../main/options.cpp \
+	../main/options.h \
+	../parser/options.cpp \
+	../parser/options.h
+
+BUILT_SOURCES = \
+	exprs-builts \
 	../smt/smt_options.cpp \
-	$(OPTIONS_FILES:%=../%.cpp) \
-	$(OPTIONS_FILES:%=../%.h) \
-	exprs-builts
+	options.cpp \
+	options_holder.h
 
 DISTCLEANFILES = \
+	$(OPTIONS_FILES_SRCS) \
 	$(BUILT_SOURCES) \
 	options-stamp
 
 EXTRA_DIST = \
 	mkoptions \
-	base_options \
 	base_options_template.h \
 	base_options_template.cpp \
 	options_template.cpp \
 	options_holder_template.h \
 	options.i \
 	option_exception.i \
-	$(OPTIONS_FILES:%=../%)
+	$(OPTIONS_FILES)
 
 if CVC4_DEBUG
 # listing Debug_tags too ensures that make doesn't auto-remove it
@@ -116,8 +168,8 @@ MOSTLYCLEANFILES = \
 	Debug_tags.h \
 	Trace_tags.h
 
-options_holder.h options.cpp ../smt/smt_options.cpp base_options.cpp base_options.h $(OPTIONS_FILES:%=../%.cpp) $(OPTIONS_FILES:%=../%.h): options-stamp
-options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES:%=../%)
+options_holder.h options.cpp ../smt/smt_options.cpp $(OPTIONS_FILES_SRCS): options-stamp
+options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES)
 	$(AM_V_at)chmod +x @srcdir@/mkoptions
 	$(AM_V_GEN)(@srcdir@/mkoptions \
 		@srcdir@/options_holder_template.h @builddir@/options_holder.h \
@@ -126,11 +178,11 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options
 		@top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \
 		-t \
 		@srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \
-		$(foreach o,$(OPTIONS_FILES),"$(srcdir)/../$(o)" "$(dir $(builddir)/../$(o))") \
+		$(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(dir $(builddir)/$(o))") \
 	)
 	touch "$@"
 
-base_options $(OPTIONS_FILES:%=../%):;
+$(OPTIONS_FILES):;
 
 .PHONY: exprs-builts
 exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true
diff --git a/src/options/mkoptions b/src/options/mkoptions
index a551d5bd9..540e2b77a 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -2,7 +2,7 @@
 #
 # mkoptions
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2011  The CVC4 Project
+# Copyright (c) 2011-2012  The CVC4 Project
 #
 # The purpose of this script is to create options.{h,cpp}
 # from template files and a list of options.
@@ -12,7 +12,7 @@
 #   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
 #
 
-copyright=2011
+copyright=2011-2012
 
 me=$(basename "$0")
 
@@ -1103,14 +1103,18 @@ EOF
 
   ) >"$output.tmp"
 
-  diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
-  rm -f "$output.tmp"
+  if diff -q "$output" "$output.tmp" &>/dev/null; then
+    rm -f "$output.tmp"
+  else
+    mv -f "$output.tmp" "$output"
+    echo "regenerated $output"
+  fi
 }
 
 while [ $# -gt 0 ]; do
   kf="$1"; shift
   if [ $# -eq 0 ]; then
-    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    echo "$me: error: mismatched number of templates and output files (after -t)" >&2
     usage
     exit 1
   fi