From 52b8d1508d91a2284c29e3fae02a22307e42a476 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 23 Oct 2015 18:31:30 -0700 Subject: [PATCH] This commit removes using absolute paths in the generation of the .subdirs file. This also rearranges generation of the file so that one .subdirs file is generated once per Makefile.am file. This keeps using relative paths clean. --- src/Makefile.am | 40 +++++++++++++++++++++--------- src/Makefile.theories | 3 +++ src/expr/Makefile.am | 49 +++++++++++++++++++++---------------- src/mksubdirs | 16 ++++++++++++ src/theory/Makefile.subdirs | 7 ------ 5 files changed, 75 insertions(+), 40 deletions(-) create mode 100644 src/Makefile.theories create mode 100755 src/mksubdirs delete mode 100644 src/theory/Makefile.subdirs diff --git a/src/Makefile.am b/src/Makefile.am index 95ca44e63..9502afa9c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -20,7 +20,8 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main -THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl +# The THEORIES list has been moved to Makefile.theories +include @top_srcdir@/src/Makefile.theories lib_LTLIBRARIES = libcvc4.la @@ -232,7 +233,7 @@ libcvc4_la_SOURCES = \ theory/builtin/theory_builtin.cpp \ theory/datatypes/theory_datatypes_type_rules.h \ theory/datatypes/type_enumerator.h \ - theory/datatypes/type_enumerator.cpp \ + theory/datatypes/type_enumerator.cpp \ theory/datatypes/theory_datatypes.h \ theory/datatypes/datatypes_rewriter.h \ theory/datatypes/theory_datatypes.cpp \ @@ -465,7 +466,8 @@ endif BUILT_SOURCES = \ theory/rewriter_tables.h \ theory/theory_traits.h \ - theory/type_enumerator.cpp + theory/type_enumerator.cpp \ + $(top_builddir)/src/.subdirs CLEANFILES = \ svn_versioninfo.cpp \ @@ -476,7 +478,8 @@ CLEANFILES = \ gitinfo \ theory/rewriter_tables.h \ theory/theory_traits.h \ - theory/type_enumerator.cpp + theory/type_enumerator.cpp \ + $(top_builddir)/src/.subdirs EXTRA_DIST = \ include/cvc4_private_library.h \ @@ -486,6 +489,7 @@ EXTRA_DIST = \ include/cvc4_public.h \ include/cvc4.h \ cvc4.i \ + Makefile.theories \ smt/smt_options_template.cpp \ smt/modal_exception.i \ smt/logic_exception.i \ @@ -496,7 +500,6 @@ EXTRA_DIST = \ theory/type_enumerator_template.cpp \ theory/mktheorytraits \ theory/mkrewriter \ - theory/Makefile.subdirs \ theory/uf/kinds \ theory/bv/kinds \ theory/idl/kinds \ @@ -633,28 +636,41 @@ uninstall-local: # fails. %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" -include @top_srcdir@/src/theory/Makefile.subdirs +#include @top_srcdir@/src/theory/Makefile.subdirs +$(top_builddir)/src/.subdirs: $(top_srcdir)/src/Makefile.theories @top_srcdir@/src/mksubdirs + $(AM_V_at)test -d $(top_builddir)/src || mkdir $(top_builddir)/src + $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs + $(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/.subdirs.tmp + @if ! diff -q $(top_builddir)/src/.subdirs $(top_builddir)/src/.subdirs.tmp &>/dev/null; then \ + echo " GEN " $@; \ + $(am__mv) $(top_builddir)/src/.subdirs.tmp $(top_builddir)/src/.subdirs; \ + fi + +# $(AM_V_at)(\ +# grep '^THEORIES = ' $(top_srcdir)/src/Makefile.theories | \ +# cut -d' ' -f3- | tr ' ' "\n" | \ +# xargs -I__D__ echo $(top_srcdir)/src/theory/__D__/kinds ) >$(top_builddir)/src/.subdirs.tmp -theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +theory/rewriter_tables.h: theory/rewriter_tables_template.h theory/mkrewriter @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/theory/mkrewriter $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/theory/mkrewriter \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/.subdirs` \ > $@) || (rm -f $@ && exit 1) -theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +theory/theory_traits.h: theory/theory_traits_template.h theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/.subdirs` \ > $@) || (rm -f $@ && exit 1) -theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +theory/type_enumerator.cpp: theory/type_enumerator_template.cpp theory/mktheorytraits @top_builddir@/src/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/theory/mktheorytraits $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/theory/mktheorytraits \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/.subdirs` \ > $@) || (rm -f $@ && exit 1) diff --git a/src/Makefile.theories b/src/Makefile.theories new file mode 100644 index 000000000..8b5cef4d5 --- /dev/null +++ b/src/Makefile.theories @@ -0,0 +1,3 @@ + + +THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 13358d294..c5a032abc 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -80,7 +80,7 @@ BUILT_SOURCES = \ expr_manager.h \ expr_manager.cpp \ type_checker.cpp \ - $(top_builddir)/src/theory/.subdirs + $(top_builddir)/src/expr/.subdirs CLEANFILES = \ kind.h \ @@ -91,72 +91,79 @@ CLEANFILES = \ expr_manager.cpp \ type_checker.cpp \ type_properties.h \ - $(top_builddir)/src/theory/.subdirs - -include @top_srcdir@/src/theory/Makefile.subdirs - -kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(top_builddir)/src/expr/.subdirs + +$(top_builddir)/src/expr/.subdirs: $(top_srcdir)/src/Makefile.theories @top_srcdir@/src/mksubdirs + $(AM_V_at)test -d $(top_builddir)/src/expr || mkdir $(top_builddir)/src/expr + $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs + $(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/expr/.subdirs.tmp + @if ! diff -q $(top_builddir)/src/expr/.subdirs $(top_builddir)/src/expr/.subdirs.tmp &>/dev/null; then \ + echo " GEN " $@; \ + $(am__mv) $(top_builddir)/src/expr/.subdirs.tmp $(top_builddir)/src/expr/.subdirs; \ + fi + +kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkkind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkkind \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkmetakind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkmetakind \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkkind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkkind \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) -type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - `cat @top_builddir@/src/theory/.subdirs` \ + `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) .PHONY: builts diff --git a/src/mksubdirs b/src/mksubdirs new file mode 100755 index 000000000..c96437caa --- /dev/null +++ b/src/mksubdirs @@ -0,0 +1,16 @@ +#!/bin/bash +# +# The purpose of this file is to generate a .subdirs file in the build process. +# This file contains a file of relative paths to all of the theories relative +# to the current directory. Each Makefile.am should thus build its own .subdirs file. +# This assumes it is passed the equivalent of the $top_srcdir configure variable. +# +# Invocation: +# +# mksubdirs + +TOP_SRCDIR=$1 + +grep '^THEORIES = ' $TOP_SRCDIR/src/Makefile.theories | \ + cut -d' ' -f3- | tr ' ' "\n" | \ + xargs -I__D__ echo "$TOP_SRCDIR/src/theory/__D__/kinds" diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs deleted file mode 100644 index 42582c67f..000000000 --- a/src/theory/Makefile.subdirs +++ /dev/null @@ -1,7 +0,0 @@ -$(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/Makefile.am - $(AM_V_at)test -d $(top_builddir)/src/theory || mkdir $(top_builddir)/src/theory - $(AM_V_at)grep '^THEORIES = ' $(abs_top_srcdir)/src/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -I__D__ echo $(abs_top_srcdir)/src/theory/__D__/kinds >$(abs_top_builddir)/src/theory/.subdirs.tmp - @if ! diff -q $(abs_top_builddir)/src/theory/.subdirs $(abs_top_builddir)/src/theory/.subdirs.tmp &>/dev/null; then \ - echo " GEN " $@; \ - $(am__mv) $(abs_top_builddir)/src/theory/.subdirs.tmp $(abs_top_builddir)/src/theory/.subdirs; \ - fi -- 2.30.2