From 7b568f370f6ec4105414b562ee2a6fcb3d7048f2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 1 Nov 2011 17:08:55 +0000 Subject: [PATCH] Improvements to header installation on user machines. Internally, we can still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include --- contrib/cut-release | 44 ++++++++++++++----- src/Makefile.am | 10 ++++- src/bindings/compat/c/c_interface.cpp | 2 +- src/bindings/compat/c/c_interface.h | 2 +- .../compat/java/include/cvc3/JniUtils.h | 7 +-- src/expr/node_builder.h | 4 +- src/main/interactive_shell.cpp | 8 ++-- src/main/main.cpp | 4 +- src/main/util.cpp | 2 +- src/parser/antlr_input.cpp | 14 +++--- src/parser/antlr_input.h | 6 +-- src/parser/antlr_input_imports.cpp | 6 +-- src/parser/bounded_token_factory.cpp | 2 +- src/parser/input.cpp | 6 +-- src/parser/parser.cpp | 6 +-- src/parser/parser_builder.cpp | 6 +-- src/parser/smt/smt_input.cpp | 2 +- src/parser/smt2/smt2_input.cpp | 2 +- src/proof/cnf_proof.cpp | 2 +- src/theory/arrays/array_info.cpp | 2 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/bv/equality_engine.cpp | 2 +- 22 files changed, 86 insertions(+), 55 deletions(-) diff --git a/contrib/cut-release b/contrib/cut-release index 5ca8d5a9b..8f707dcc3 100755 --- a/contrib/cut-release +++ b/contrib/cut-release @@ -31,7 +31,7 @@ if [ $# -lt 1 ]; then fi if ! [ -e src/expr/node.h -a -e .svn ]; then - echo "$(basename "$0"): ERROR: you should run this from the top-level of a CVC4 subversion working directory" >&2 + echo "$(basename "$0"): ERROR: You should run this from the top-level of a CVC4 subversion working directory" >&2 exit 1 fi @@ -39,7 +39,7 @@ version="$1" shift if echo "$version" | grep '[^a-zA-Z0-9_.+(){}^%#-]' &>/dev/null; then - echo "$(basename "$0"): ERROR: version designation \`$version' contains illegal characters" >&2 + echo "$(basename "$0"): ERROR: Version designation \`$version' contains illegal characters" >&2 exit 1 fi @@ -63,14 +63,16 @@ echo "Version: $version" echo isthatright +echo "Checking whether release \`$version' already exists..." if ! svn ls "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" 2>&1 >/dev/null | grep non-existent >/dev/null; then - echo "$(basename "$0"): ERROR: subversion repo already contains a release \`$version'" >&2 + echo "$(basename "$0"): ERROR: Subversion repo already contains a release \`$version'" >&2 $dryrun || exit 1 fi +echo "Checking working directory for local modifications..." if $dryrun; then if [ -n "$(svn status -q configure.ac)" ]; then - echo "$(basename "$0"): ERROR: in dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2 + echo "$(basename "$0"): ERROR: In dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2 exit 1 fi elif [ -n "$(svn status -q)" ]; then @@ -80,20 +82,41 @@ fi root="$(svn info | grep "^Repository Root: https://subversive.cims.nyu.edu/.*" | cut -f3 -d' ')" if [ -z "$root" ]; then - echo "$(basename "$0"): ERROR: can't get repository root URL" 2>&1 + echo "$(basename "$0"): ERROR: Can't get repository root URL" 2>&1 $dryrun || exit 1 fi +echo "Checking repo for unmerged updates..." if [ `svn -uq status | wc -l` -ne 1 ]; then - echo "$(basename "$0"): ERROR: this working directory isn't up to date" 2>&1 + echo "$(basename "$0"): ERROR: This working directory isn't up to date" 2>&1 $dryrun || exit 1 fi +echo "Checking sources for broken public headers..." +suspect_files="\ +$(grep -r --exclude-dir=.svn '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src | + grep -v '"cvc4parser_public\.h"' | + grep -v '"cvc4_public\.h"' | + grep -v '"cvc4_private\.h"' | + grep -v '"cvc4autoconfig\.h"' | + grep -v '"cvc4parser_private\.h"' | + cut -f1 -d: | + sort -u | + xargs grep -l '^[ \t]*#[ \t]*include[ \t]*"cvc4.*public\.h"' | + xargs echo)" +if [ -n "$suspect_files" ]; then + echo "$(basename "$0"): ERROR: The following publicly-installed headers appear" 2>&1 + echo "$(basename "$0"): ERROR: to have relative #includes and may be broken up" 2>&1 + echo "$(basename "$0"): ERROR: on install: $suspect_files" 2>&1 + $dryrun || exit 1 +fi + +echo "Adjusting version info lines in configure.ac..." if ! grep '^m4_define(_CVC4_MAJOR, *[0-9][0-9]* *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_MINOR, *[0-9][0-9]* *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_RELEASE, *[0-9][0-9]* *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_EXTRAVERSION, *\[.*\] *)' configure.ac &>/dev/null; then - echo "$(basename "$0"): ERROR: cannot locate the version info lines of configure.ac" >&2 + echo "$(basename "$0"): ERROR: Cannot locate the version info lines of configure.ac" >&2 $dryrun || exit 1 fi perl -pi -e 's/^m4_define\(_CVC4_MAJOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MAJOR, ${1}'"$major"'$2)/; @@ -114,7 +137,7 @@ if ! grep '^m4_define(_CVC4_MAJOR, *'"$major"' *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_MINOR, *'"$minor"' *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_RELEASE, *'"$release"' *)' configure.ac &>/dev/null || ! grep '^m4_define(_CVC4_EXTRAVERSION, *\['"$extra"'\] *)' configure.ac &>/dev/null; then - echo "$(basename "$0"): INTERNAL ERROR: cannot find the modified version info lines in configure.ac, bailing..." >&2 + echo "$(basename "$0"): INTERNAL ERROR: Cannot find the modified version info lines in configure.ac, bailing..." >&2 exit 1 fi if [ -z "$(svn status -q configure.ac)" ]; then @@ -122,6 +145,7 @@ if [ -z "$(svn status -q configure.ac)" ]; then exit 1 fi +echo "Building and checking distribution \`cvc4-$version'..." if ! $SHELL -c '\ version="'$version'"; \ set -ex; \ @@ -140,11 +164,11 @@ if ! $SHELL -c '\ fi if ! [ -e release-$version/cvc4-$version.tar.gz ]; then - echo "$(basename "$0"): INTERNAL ERROR: cannot find the distribution tarball I just built" >&2 + echo "$(basename "$0"): INTERNAL ERROR: Cannot find the distribution tarball I just built" >&2 exit 1 fi if ! [ -e release-$version/src/main/cvc4 ]; then - echo "$(basename "$0"): INTERNAL ERROR: cannot find the binary I just built" >&2 + echo "$(basename "$0"): INTERNAL ERROR: Cannot find the binary I just built" >&2 exit 1 fi diff --git a/src/Makefile.am b/src/Makefile.am index 906a64a65..627a89a67 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -99,6 +99,7 @@ svninfo.tmp: install-data-local: (echo include/cvc4.h; \ echo include/cvc4_public.h; \ + echo include/cvc4parser_public.h; \ find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ (cd "$(srcdir)" && find * -name '*.h' | \ @@ -111,16 +112,21 @@ install-data-local: $(mkinstalldirs) "$$(dirname "$(DESTDIR)$(includedir)/cvc4/$$d")"; \ if [ -e "$$f" ]; then \ path="$$f"; \ + fixpath="$$f.fix"; \ else \ path="$(srcdir)/$$f"; \ + fixpath="$(builddir)/$$f.fix"; \ + $(MKDIR_P) "`dirname "$$fixpath"`"; \ fi; \ - echo $(INSTALL_DATA) "$$path" "$(DESTDIR)$(includedir)/cvc4/$$d"; \ - $(INSTALL_DATA) "$$path" "$(DESTDIR)$(includedir)/cvc4/$$d"; \ + sed 's,^\([ \t]*#[ \t]*include[ \t*]\)"\(.*\)"\([ \t]*\)$$,\1\3,' "$$path" > "$$fixpath" || exit 1; \ + echo $(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d"; \ + $(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d" || exit 1; \ done uninstall-local: -(echo include/cvc4.h; \ echo include/cvc4_public.h; \ + echo include/cvc4parser_public.h; \ find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ (cd "$(srcdir)" && find * -name '*.h' | \ diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp index 58fb70dcb..6a8a98547 100644 --- a/src/bindings/compat/c/c_interface.cpp +++ b/src/bindings/compat/c/c_interface.cpp @@ -21,7 +21,7 @@ #include -#include "c_interface_defs.h" +#include "bindings/compat/c/c_interface_defs.h" #include "compat/cvc3_compat.h" //#include "vc.h" //#include "command_line_flags.h" diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h index ce372be70..14fea7478 100644 --- a/src/bindings/compat/c/c_interface.h +++ b/src/bindings/compat/c/c_interface.h @@ -24,7 +24,7 @@ #ifndef _cvc3__include__c_interface_h_ #define _cvc3__include__c_interface_h_ -#include "c_interface_defs.h" +#include "bindings/compat/c/c_interface_defs.h" //! Flags can be NULL VC vc_createValidityChecker(Flags flags); diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h index 3ce1e9224..c6bcc04f8 100644 --- a/src/bindings/compat/java/include/cvc3/JniUtils.h +++ b/src/bindings/compat/java/include/cvc3/JniUtils.h @@ -5,9 +5,10 @@ #include #include #include -#include "vcl.h" -#include "hash_map.h" -#include "exception.h" +#include "compat/cvc3_compat.h" +//#include "vcl.h" +//#include "hash_map.h" +//#include "exception.h" namespace Java_cvc3_JniUtils { diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 1914bb736..ded7ad8fe 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -151,8 +151,8 @@ #include "cvc4_private.h" /* strong dependency; make sure node is included first */ -#include "node.h" -#include "type_node.h" +#include "expr/node.h" +#include "expr/type_node.h" #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index ef576839c..f2d6f1714 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -27,7 +27,7 @@ #include "cvc4autoconfig.h" -#include "interactive_shell.h" +#include "main/interactive_shell.h" #include "expr/command.h" #include "parser/input.h" @@ -61,15 +61,15 @@ using __gnu_cxx::stdio_filebuf; char* commandGenerator(const char* text, int state); static const char* const cvc_commands[] = { -#include "cvc_tokens.h" +#include "main/cvc_tokens.h" };/* cvc_commands */ static const char* const smt_commands[] = { -#include "smt_tokens.h" +#include "main/smt_tokens.h" };/* smt_commands */ static const char* const smt2_commands[] = { -#include "smt2_tokens.h" +#include "main/smt2_tokens.h" };/* smt2_commands */ static const char* const* commandsBegin; diff --git a/src/main/main.cpp b/src/main/main.cpp index ef19e1604..ec0a00ff8 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,8 +26,8 @@ #include #include "cvc4autoconfig.h" -#include "main.h" -#include "interactive_shell.h" +#include "main/main.h" +#include "main/interactive_shell.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" diff --git a/src/main/util.cpp b/src/main/util.cpp index 255d84205..89aa5c6aa 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -30,7 +30,7 @@ #include "util/stats.h" #include "cvc4autoconfig.h" -#include "main.h" +#include "main/main.h" using CVC4::Exception; using namespace std; diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index ec3b7077e..e52145d4e 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -20,13 +20,13 @@ #include #include -#include "antlr_input.h" -#include "input.h" -#include "bounded_token_buffer.h" -#include "bounded_token_factory.h" -#include "memory_mapped_input_buffer.h" -#include "parser_exception.h" -#include "parser.h" +#include "parser/antlr_input.h" +#include "parser/input.h" +#include "parser/bounded_token_buffer.h" +#include "parser/bounded_token_factory.h" +#include "parser/memory_mapped_input_buffer.h" +#include "parser/parser_exception.h" +#include "parser/parser.h" #include "expr/command.h" #include "expr/type.h" diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 913dd8013..dca26ab75 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -28,9 +28,9 @@ #include #include -#include "bounded_token_buffer.h" -#include "parser_exception.h" -#include "input.h" +#include "parser/bounded_token_buffer.h" +#include "parser/parser_exception.h" +#include "parser/input.h" #include "util/Assert.h" #include "util/bitvector.h" diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 2805d518a..870edb928 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -54,9 +54,9 @@ #include #include -#include "antlr_input.h" -#include "parser.h" -#include "parser_exception.h" +#include "parser/antlr_input.h" +#include "parser/parser.h" +#include "parser/parser_exception.h" #include "util/Assert.h" using namespace std; diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index 71b8849e5..f05c9007a 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -19,7 +19,7 @@ #include #include #include -#include "bounded_token_factory.h" +#include "parser/bounded_token_factory.h" namespace CVC4 { namespace parser { diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 27b207342..70c887371 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -16,9 +16,9 @@ ** A super-class for input language parsers **/ -#include "input.h" -#include "parser_exception.h" -#include "parser.h" +#include "parser/input.h" +#include "parser/parser_exception.h" +#include "parser/parser.h" #include "expr/command.h" #include "expr/type.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 3f2ec107a..f1ad4b330 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -21,9 +21,9 @@ #include #include -#include "input.h" -#include "parser.h" -#include "parser_exception.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/parser_exception.h" #include "expr/command.h" #include "expr/expr.h" #include "expr/kind.h" diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index d4725c4bc..5c755b5f6 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -18,9 +18,9 @@ #include -#include "parser_builder.h" -#include "input.h" -#include "parser.h" +#include "parser/parser_builder.h" +#include "parser/input.h" +#include "parser/parser.h" #include "smt/smt.h" #include "smt2/smt2.h" diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index d368339f5..85a117dd0 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -18,7 +18,7 @@ #include -#include "smt_input.h" +#include "parser/smt/smt_input.h" #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index acd0e17f6..8f43b0acf 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -18,7 +18,7 @@ #include -#include "smt2_input.h" +#include "parser/smt2/smt2_input.h" #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index a8dc39765..5e5d55f63 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -17,7 +17,7 @@ ** \todo document this file **/ -#include "cnf_proof.h" +#include "proof/cnf_proof.h" using namespace CVC4::prop; namespace CVC4 { diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 1e06621b4..50ded8758 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -17,7 +17,7 @@ ** **/ -#include "array_info.h" +#include "theory/arrays/array_info.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7fa215bfc..366c2d3f7 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -24,7 +24,7 @@ #include "theory/theory.h" #include "theory/arrays/union_find.h" #include "util/congruence_closure.h" -#include "array_info.h" +#include "theory/arrays/array_info.h" #include "util/hash.h" #include "util/ntuple.h" #include "util/stats.h" diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp index ee4e9903c..a4d2e6329 100644 --- a/src/theory/bv/equality_engine.cpp +++ b/src/theory/bv/equality_engine.cpp @@ -17,7 +17,7 @@ ** \todo document this file **/ -#include "equality_engine.h" +#include "theory/bv/equality_engine.h" using namespace CVC4::theory::bv; -- 2.30.2