From: Morgan Deters Date: Wed, 22 Aug 2012 20:19:27 +0000 (+0000) Subject: fix some build dependencies in options-building; should fix a strange bug Andy saw... X-Git-Tag: cvc5-1.0.0~7854 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ba847f7c4c6385cc4a788c3b965498acb3f0f08;p=cvc5.git 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 --- 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 \ @@ -32,37 +54,67 @@ liboptions_la_SOURCES = \ option_exception.h 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 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