more build system work

diff --git a/Makefile b/Makefile
index 707f3cda3f21a114bc0be1e511f63f05a4ff587d..74a1e169b0911df98f9e35d918094c888a3d00a0 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
-.PHONY: default
-default: all
+.PHONY: _default_build_
+_default_build_: all
 %:
        @if test -e builds; then \
                echo cd builds; \

diff --git a/Makefile.am b/Makefile.am
index 02d9e1bea8838961a3379d608f34f51debbc9850..76130be4513530a6e05ed373147dab9c29e37c0b 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -6,7 +6,7 @@ ACLOCAL_AMFLAGS = -I config
 SUBDIRS = src test doc contrib
 
 .PHONY: production debug default competition
-production: ; @srcdir@/configure --with-build=production && $(MAKE)
-debug:      ; @srcdir@/configure --with-build=debug && $(MAKE)
-default:    ; @srcdir@/configure --with-build=default && $(MAKE)
-competition:; @srcdir@/configure --with-build=competition && $(MAKE)
+production: ; (cd @top_srcdir@ && ./configure --with-build=production && $(MAKE))
+debug:      ; (cd @top_srcdir@ && ./configure --with-build=debug && $(MAKE))
+default:    ; (cd @top_srcdir@ && ./configure --with-build=default && $(MAKE))
+competition:; (cd @top_srcdir@ && ./configure --with-build=competition && $(MAKE))

diff --git a/Makefile.builds b/Makefile.builds
deleted file mode 100644 (file)
index 0fb0776..0000000
--- a/Makefile.builds
+++ /dev/null
@@ -1,23 +0,0 @@
-include current
-
-.PHONY: default
-default: all
-all:
-       @if (cd $(CURRENT_BUILD) && $(MAKE) $@); then \
-               mkdir -pv bin lib; \
-               echo $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la `pwd`/lib; \
-               $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la `pwd`/lib; \
-               echo $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la `pwd`/lib; \
-               $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la `pwd`/lib; \
-               echo "libdir=`pwd`/lib; progdir=`pwd`/bin; file=cvc4"; \
-               libdir=`pwd`/lib; progdir=`pwd`/bin; file=cvc4; \
-               echo `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$libdir -Wl,-rpath:'`; \
-               eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$libdir -Wl,-rpath:'`; \
-               echo "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
-               eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
-       else \
-               echo Build failure.; \
-       fi
-
-%:
-       (cd $(CURRENT_BUILD) && $(MAKE) $@)

diff --git a/Makefile.builds.in b/Makefile.builds.in
new file mode 100644 (file)
index 0000000..f6e17b4
--- /dev/null
+++ b/Makefile.builds.in
@@ -0,0 +1,39 @@
+# -*- makefile -*-
+
+include current
+
+@SET_MAKE@
+
+install_sh = @install_sh@
+mkinstalldirs = $(install_sh) -d
+exec_prefix = @exec_prefix@
+prefix = @prefix@
+bindir = @bindir@
+libdir = @libdir@
+abs_builddir = @abs_builddir@
+
+.PHONY: _default_build_
+_default_build_: all
+all:
+       (cd $(CURRENT_BUILD) && $(MAKE) $@)
+       # populate builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib
+       $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)"
+       $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "$(abs_builddir)$(libdir)"
+       $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "$(abs_builddir)$(libdir)"
+       thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
+               eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
+               eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
+       ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
+       ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
+       # populate builds/bin and builds/lib
+       mkdir -pv ".$(bindir)" ".$(libdir)"
+       $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
+       $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
+       thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
+               eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
+               eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
+       ln -sfv ".$(libdir)" lib
+       ln -sfv ".$(bindir)" bin
+
+%:
+       (cd $(CURRENT_BUILD) && $(MAKE) $@)

diff --git a/configure.ac b/configure.ac
index c7f4611281e815bc78592ed6d409f70d4cf7374b..f4320aeb4a5de8d544bb4abb05e130e4c419098d 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -7,6 +7,11 @@ AC_CONFIG_AUX_DIR([config])
 #AC_CONFIG_LIBOBJ_DIR([lib])
 AC_CONFIG_MACRO_DIR([config])
 
+CVC4_RELEASE=prerelease
+CVC4_LIBRARY_RELEASE_CODE=0:0:0
+CVC4_LIBRARY_VERSION=0:0:0
+CVC4_PARSER_LIBRARY_VERSION=0:0:0
+
 # really irritating: AC_CANONICAL_* bash $@
 config_cmdline="$@"
 
@@ -92,11 +97,15 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
   AC_MSG_RESULT([this one (in builds/)])
 elif test -e src/include/cvc4.h; then
   AC_MSG_RESULT([builds/$target/$build_type])
-  rm -f config.log config.status confdefs.h
-  mkdir -p "builds/$target/$build_type"
-  test -e builds/Makefile || ln -sf ../Makefile.builds builds/Makefile
-  echo "CURRENT_BUILD = $target/$build_type" > builds/current
   echo
+  echo Setting up "builds/$target/$build_type"...
+  rm -fv config.log config.status confdefs.h
+  mkdir -pv "builds/$target/$build_type"
+  test -e builds/Makefile || ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
+  echo Creating builds/current...
+  (echo "# This is the most-recently-configured CVC4 build"; \
+   echo "# 'make' in the top-level source directory applies to this build"; \
+   echo "CURRENT_BUILD = $target/$build_type") > builds/current
   echo cd "builds/$target/$build_type"
   cd "builds/$target/$build_type"
   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
@@ -216,7 +225,7 @@ if test "$enable_profiling" = yes; then
   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 fi
 
-AM_INIT_AUTOMAKE(cvc4, prerelease)
+AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE)
 AC_CONFIG_HEADERS([config.h])
 
 # keep track of whether the user set these (check here, because
@@ -301,8 +310,9 @@ fi
 # Checks for libraries.
 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
 # Check for antlr C++ runtime (defined in config/antlr.m4)
-AC_LIB_ANTLR
-
+if test "$enable_antlr" = yes; then
+  AC_LIB_ANTLR
+fi
 
 # Checks for header files.
 AC_CHECK_HEADERS([getopt.h unistd.h])
@@ -320,6 +330,9 @@ AC_TYPE_SIZE_T
 
 # Prepare configure output
 
+AC_SUBST(CVC4_LIBRARY_RELEASE_CODE)
+AC_SUBST(CVC4_LIBRARY_VERSION)
+AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
 if test "$user_cppflags" = no; then
   CPPFLAGS="$CVC4CPPFLAGS"
 fi
@@ -331,6 +344,7 @@ if test "$user_ldflags" = no; then
 fi
 
 AC_CONFIG_FILES([
+  Makefile.builds
   Makefile
   contrib/Makefile
   doc/Makefile
@@ -384,7 +398,10 @@ CPPFLAGS     : $CPPFLAGS
 CXXFLAGS     : $CXXFLAGS
 LDFLAGS      : $LDFLAGS
 
-Using ANTLR parsers: $enable_antlr
+Using ANTLR parsers  : $enable_antlr
+Library releases     : $CVC4_LIBRARY_RELEASE_CODE
+libcvc4 version      : $CVC4_LIBRARY_VERSION
+libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION
 
 Now just type make, followed by make check or make install, as you like.
 

diff --git a/src/Makefile.am b/src/Makefile.am
index 128e47bd5c59db48d1a45d64d2929c80c1a9f576..afbb587a8c8892ed8ff59762f0f7d85ec4e895bd 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,3 +1,20 @@
+# LIBCVC4_VERSION (-version-info) is in the form current:revision:age
+#
+# current -
+#   increment if interfaces have been added, removed or changed
+# revision -
+#   increment if source code has changed
+#   set to zero if current is incremented
+# age -
+#   increment if interfaces have been added
+#   set to zero if interfaces have been removed
+#   or changed
+#
+# LIBCVC4_RELEASE (-release) should match the CVC4 release version
+#
+LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
+LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
+
 INCLUDES = -I@srcdir@/include -I@srcdir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
@@ -6,6 +23,8 @@ SUBDIRS = util expr context prop smt theory . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 
+libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
+
 libcvc4_la_SOURCES =
 libcvc4_la_LIBADD = \
        @builddir@/util/libutil.la \
@@ -22,10 +41,10 @@ publicheaders = \
        include/cvc4_expr.h
 
 install-data-local: $(publicheaders)
-       $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4; \
-       @for f in $(publicheaders); do
-               echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"
-               $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"
+       $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
+       @for f in $(publicheaders); do \
+               echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
+               $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
        done
 
 include/cvc4.h: smt/smt_engine.h

diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
index ccc07b40a1a7bbe3635d85cbb69a9b046f864f19..95fac9aaa5d5a0bca3d90eb247892bccd686f2e5 100644 (file)
--- a/src/include/cvc4_config.h
+++ b/src/include/cvc4_config.h
@@ -10,35 +10,27 @@
  ** [[ Add file-specific comments here ]]
  **/
 
-#ifdef __BUILDING_CVC4LIB
-
-#  if defined _WIN32 || defined __CYGWIN__
-#    ifdef BUILDING_DLL
-#      ifdef __GNUC__
-#        define CVC4_PUBLIC __attribute__((dllexport))
-#      else /* ! __GNUC__ */
-#        define CVC4_PUBLIC __declspec(dllexport)
-#      endif /* __GNUC__ */
-#    else /* BUILDING_DLL */
-#      ifdef __GNUC__
-#        define CVC4_PUBLIC __attribute__((dllimport))
-#      else /* ! __GNUC__ */
-#        define CVC4_PUBLIC __declspec(dllimport)
-#      endif /* __GNUC__ */
-#    endif /* BUILDING_DLL */
-#  else /* !( defined _WIN32 || defined __CYGWIN__ ) */
-#    if __GNUC__ >= 4
-#      define CVC4_PUBLIC __attribute__ ((visibility("default")))
-#    else /* !( __GNUC__ >= 4 ) */
-#      define CVC4_PUBLIC
-#    endif /* __GNUC__ >= 4 */
-#  endif /* defined _WIN32 || defined __CYGWIN__ */
-
-#else /* ! __BUILDING_CVC4LIB */
-
-#  define CVC4_PUBLIC
-
-#endif /* __BUILDING_CVC4LIB */
+#if defined _WIN32 || defined __CYGWIN__
+#  ifdef BUILDING_DLL
+#    ifdef __GNUC__
+#      define CVC4_PUBLIC __attribute__((dllexport))
+#    else /* ! __GNUC__ */
+#      define CVC4_PUBLIC __declspec(dllexport)
+#    endif /* __GNUC__ */
+#  else /* BUILDING_DLL */
+#    ifdef __GNUC__
+#      define CVC4_PUBLIC __attribute__((dllimport))
+#    else /* ! __GNUC__ */
+#      define CVC4_PUBLIC __declspec(dllimport)
+#    endif /* __GNUC__ */
+#  endif /* BUILDING_DLL */
+#else /* !( defined _WIN32 || defined __CYGWIN__ ) */
+#  if __GNUC__ >= 4
+#    define CVC4_PUBLIC __attribute__ ((visibility("default")))
+#  else /* !( __GNUC__ >= 4 ) */
+#    define CVC4_PUBLIC
+#  endif /* __GNUC__ >= 4 */
+#endif /* defined _WIN32 || defined __CYGWIN__ */
 
 #define EXPECT_TRUE(x) __builtin_expect( (x), true)
 #define EXPECT_FALSE(x) __builtin_expect( (x), false)

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 36e4c0342806949074d750d383d8bc8d5ed92bb2..0992a434ad3dba94a7ecba0594109ed147df92aa 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
+AM_CPPFLAGS =
 
 bin_PROGRAMS = cvc4
 

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 7eb52d3e9845055f98f8be19865d151ac6869ef9..7e3cee751e7154614cb86371589502d3f72fae38 100644 (file)
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,14 +1,37 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
+# LIBCVC4PARSER_VERSION (-version-info) is in the form current:revision:age
+#
+# current -
+#   increment if interfaces have been added, removed or changed
+# revision -
+#   increment if source code has changed
+#   set to zero if current is incremented
+# age -
+#   increment if interfaces have been added
+#   set to zero if interfaces have been removed
+#   or changed
+#
+# LIBCVC4PARSER_RELEASE (-release) should match the CVC4 release version
+#
+LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
+LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+
+INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
+AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 if USE_ANTLR
   SUBDIRS = smt
+  INCLUDES += $(ANTLR_INCLUDES)
 endif
 
-nobase_lib_LTLIBRARIES = libcvc4parser.la
+lib_LTLIBRARIES = libcvc4parser.la
+
+libcvc4parser_la_LDFLAGS = -version-info $(LIBCVC4PARSER_VERSION) -release $(LIBCVC4PARSER_RELEASE)
+
+if USE_ANTLR
+  libcvc4parser_la_LDFLAGS += $(ANTLR_LDFLAGS)
+endif
 
-libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
 libcvc4parser_la_LIBADD = \
        ../libcvc4.la
 
@@ -22,7 +45,7 @@ libcvc4parser_la_SOURCES = \
        smtlib.ypp
 
 if USE_ANTLR
-libcvc4parser_la_SOURCES += \
+  libcvc4parser_la_SOURCES += \
        antlr_parser.cpp \
        antlr_parser.h
 endif USE_ANTLR

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 89276872c37ed90ae9d50239dae2af84b8707ef2..cd03f21f25069f819d6174a915fa5a2d5a2299da 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -12,6 +12,7 @@
 
 #include <iostream>
 
+#include "cvc4_config.h"
 #include "parser/parser.h"
 #include "util/command.h"
 #include "util/assert.h"

diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index bb2018e2e7429c186332a94244f3c6699f123ba3..acb95849f8b9587ab33b1f356153e39fa6dec849 100644 (file)
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -1,6 +1,6 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
+AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 noinst_LTLIBRARIES = libparsersmt.la