Addressed many of the concerns of bug 10 (build system code review).

Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

1 files changed, 49 insertions, 6 deletions

diff --git a/Makefile.builds.in b/Makefile.builds.in
index 789fb0bae..650d7be6d 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -1,9 +1,27 @@
 # -*- makefile -*-
+#
+# This Makefile produces the Makefile in the top-level builds/
+# directory for standard-path builds (e.g., those configured from the
+# source tree).  It has some autoconf cruft in it, documented below.
+#
+# Its main purposes are to:
+# 1. build the current build profile
+# 2. install into "builds/$(CURRENT_BUILD)/$(prefix)"
+# 3. set up "builds/$(CURRENT_BUILD)/{bin,lib}" symlinks
+# 4. install into "builds/$(prefix)"
+# 5. set up "builds/bin" and "builds/lib"
+#
+# Steps 2 and 4 require libtool-relinking for dynamically-linked
+# executables and libraries, since build/bin is not the final
+# installation path.
 
+# Include the "current" build profile.
 include current
 
+# Set up $(MAKE)
 @SET_MAKE@
 
+# Set up some basic autoconf make vars
 install_sh = @install_sh@
 mkinstalldirs = $(install_sh) -d
 exec_prefix = @exec_prefix@
@@ -11,39 +29,64 @@ prefix = @prefix@
 bindir = @bindir@
 libdir = @libdir@
 abs_builddir = @abs_builddir@
+
+# Are we building static/dynamic libraries?  One or the other can be
+# on, or both.
 BUILDING_STATIC = @BUILDING_STATIC@
 BUILDING_SHARED = @BUILDING_SHARED@
 
 .PHONY: _default_build_ all
 _default_build_: all
 all:
+#	build the current build profile
 	(cd $(CURRENT_BUILD) && $(MAKE) $@)
+#	set up builds/$(CURRENT_BUILD)/...prefix.../bin
+#	and builds/$(CURRENT_BUILD)/...prefix.../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)"
+#	install libcvc4
+	$(CURRENT_BUILD)/libtool --mode=install install -v \
+		$(CURRENT_BUILD)/src/libcvc4.la \
+		"$(abs_builddir)$(libdir)"
+#	install libcvc4parser
+	$(CURRENT_BUILD)/libtool --mode=install install -v \
+		$(CURRENT_BUILD)/src/parser/libcvc4parser.la \
+		"$(abs_builddir)$(libdir)"
 ifeq ($(BUILDING_SHARED),1)
-	thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
+#	if we're building shared libs, relink
+	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)"
 endif
 ifeq ($(BUILDING_STATIC),1)
-	install -v $(CURRENT_BUILD)/src/main/cvc4 "$(abs_builddir)$(bindir)"
+#	if we're building static libs, just install them directly
+	$(install_sh) \
+		$(CURRENT_BUILD)/src/main/cvc4 \
+		"$(abs_builddir)$(bindir)"
 endif
+#	set up builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib
 	test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
 	test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
-	mkdir -pv ".$(bindir)" ".$(libdir)"
+#	set up builds/...prefix.../bin and builds/...prefix.../lib
+	$(mkinstalldirs) ".$(bindir)" ".$(libdir)"
+#	install libcvc4
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
+#	install libcvc4parser
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
 ifeq ($(BUILDING_SHARED),1)
+#	if we're building shared libs, relink
 	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)"
 endif
 ifeq ($(BUILDING_STATIC),1)
-	install -v $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
+#	if we're building static libs, just install them directly
+	$(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
 endif
+#	set up builds/bin and builds/lib
 	test -e lib || ln -sfv ".$(libdir)" lib
 	test -e bin || ln -sfv ".$(bindir)" bin
 
+# any other target than the default doesn't do the extra stuff above
 %:
 	(cd $(CURRENT_BUILD) && $(MAKE) $@)