better documentation, allow examples to be installed, etc

9 files changed, 70 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 86a04dc3e..849d6eeab 100644
--- a/Makefile
+++ b/Makefile
@@ -7,8 +7,8 @@
 #
 builddir = builds
 
-.PHONY: all
-all .DEFAULT:
+.PHONY: all install
+all install .DEFAULT:
 	@if test -d $(builddir); then \
 		echo cd $(builddir); \
 		cd $(builddir); \
@@ -42,6 +42,10 @@ doc-internals: doc-internals-builds
 examples: all
 	(cd examples && $(MAKE) $(AM_MAKEFLAGS))
 
+.PHONY: install-examples
+install-examples:
+	(cd examples && $(MAKE) $(AM_MAKEFLAGS) install-data)
+
 YEAR := $(shell date +%Y)
 submission submission-main:
 	@if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
diff --git a/Makefile.builds.in b/Makefile.builds.in
index dd2a394ae..baf9237b2 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -186,6 +186,7 @@ endif
 #	set up builds/bin and builds/lib
 	$(AM_V_at)test -e lib || ln -sfv ".$(libdir)" lib
 	$(AM_V_at)test -e bin || ln -sfv ".$(bindir)" bin
+	rm -f doc; ln -sf "$(CURRENT_BUILD)/doc" doc
 	rm -f examples; ln -sf "$(CURRENT_BUILD)/examples" examples
 
 # The descent into "src" with target "check" is to build check
diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 780200917..52b3edeea 100644
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -11,6 +11,7 @@ EXTRA_DIST = \
 	configure-in-place \
 	depgraph \
 	get-antlr-3.4 \
+	build-cudd-with-libtool.sh \
 	mac-build \
 	run-script-smtcomp2012 \
 	theoryskel/kinds \
diff --git a/contrib/build-cudd-with-libtool.sh b/contrib/build-cudd-with-libtool.sh
index f291272b2..55f4c779e 100755
--- a/contrib/build-cudd-with-libtool.sh
+++ b/contrib/build-cudd-with-libtool.sh
@@ -5,7 +5,7 @@
 #
 # This script applies the patch, builds cudd, and, assuming there are no
 # errors, reverses the patch.
-# 
+#
 # -- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 13 Jul 2011 18:03:11 -0400
 #
 
diff --git a/examples/Makefile.am b/examples/Makefile.am
index efa35efd5..19c460c92 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -72,6 +72,10 @@ simple_vc_compat_cxx_LINK = $(CXXLINK)
 simple_vc_compat_c_LINK = $(LINK)
 endif
 
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
+
 MOSTLYCLEANFILES = $(noinst_DATA)
 
 # for silent automake rules
diff --git a/examples/README b/examples/README
index 0861092e7..246388085 100644
--- a/examples/README
+++ b/examples/README
@@ -1,16 +1,33 @@
-These are examples of how to use CVC4 with each of its in-memory, library
-interfaces.  They are essentially "hello world" examples, and do not
-fully demonstrate the interfaces, but function as a starting point to
-using simple expressions and solving functionality through each library.
-
-These examples are built as a separate step.  After building CVC4, you
-can make the examples by running "make" from inside the examples
-directory.  With the default configuration, you'll find them in
-builds/examples in the top-level source directory (if you configured
-your own build directory, you'll find them there).
-
-Many of the examples (python, ocaml, ruby, etc.) do not need to be
-compiled to run.  These are not compiled by "make"---see the comments
-in the files for ideas on how to run them.
-
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 16 Nov 2011 02:48:19 -0500
+This directory contains usage examples of CVC4's different language
+bindings, library APIs, and also tutorial examples from the tutorials
+available at http://cvc4.cs.nyu.edu/wiki/Tutorials
+
+*** Files named SimpleVC*, simple_vc*
+
+These are examples of how to use CVC4 with each of its library
+interfaces (APIs) and language bindings.  They are essentially "hello
+world" examples, and do not fully demonstrate the interfaces, but
+function as a starting point to using simple expressions and solving
+functionality through each library.
+
+*** Installing example source code
+
+Examples are not automatically installed by "make install".  If you
+wish to install them, use "make install-examples" after you configure
+your CVC4 source tree.  They'll appear in your documentation
+directory, under the "examples" subdirectory (so, by default,
+in /usr/local/share/doc/cvc4/examples).
+
+*** Building examples
+
+Examples can be built as a separate step, after building CVC4 from
+source.  After building CVC4, you can run "make examples" (or just
+"make" from *inside* the examples directory).  You'll find the built
+binaries in builds/examples (or just in "examples" if you configured a
+build directory outside of the source tree).
+
+Many of the language bindings examples (python, ocaml, ruby, etc.) do
+not need to be compiled to run.  These are not compiled by
+"make"---see the comments in the files for ideas on how to run them.
+
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 03 Oct 2012 15:47:33 -0400
diff --git a/examples/hashsmt/Makefile.am b/examples/hashsmt/Makefile.am
index 64dc60899..b385856e7 100644
--- a/examples/hashsmt/Makefile.am
+++ b/examples/hashsmt/Makefile.am
@@ -15,3 +15,7 @@ sha1smt_SOURCES = \
 	sha1.hpp
 sha1smt_LDADD = \
 	@builddir@/../../src/libcvc4.la
+
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/nra-translate/Makefile.am b/examples/nra-translate/Makefile.am
index 63bd8c0c1..081ada412 100644
--- a/examples/nra-translate/Makefile.am
+++ b/examples/nra-translate/Makefile.am
@@ -55,3 +55,7 @@ normalize_SOURCES = \
 normalize_LDADD = \
 	@builddir@/../../src/parser/libcvc4parser.la \
 	@builddir@/../../src/libcvc4.la
+
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/library_versions b/library_versions
index 4e5a7b826..bffb2b014 100644
--- a/library_versions
+++ b/library_versions
@@ -11,6 +11,22 @@
 # column, are then used.  If there are no matching lines, an error
 # is raised and the configure script is not generated.
 #
+# The library version numbers are in the form current:revision:age
+# and are passed to libtool with -version-info
+#
+#   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
+#
+# A good description of what all this means is here:
+# http://www.gnu.org/software/libtool/manual/html_node/Updating-version-info.html
+#
 # When a new CVC4 release is cut, this library_versions file should
 # be extended to provide library version information for that
 # release.  PLEASE DON'T REMOVE LINES (or edit historical lines)