better documentation, allow examples to be installed, etc

4 files changed, 45 insertions, 16 deletions

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)