better documentation, allow examples to be installed, etc

diff --git a/Makefile b/Makefile
index 86a04dc3e7ec217b83c21425d85d8c3adb221f71..849d6eeaba22648efde67d63616fd4e4a2daccc8 100644 (file)
--- 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 dd2a394ae57a9eb44e363dda8bb9d843c5d36639..baf9237b21d08d330547b35a4ddd9c58c4870cd9 100644 (file)
--- 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 780200917e42f152c1b8176e6863be5933551105..52b3edeea1f0200fea0bfc962a4fd14ca6c8796e 100644 (file)
--- 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 f291272b2571b886ba7d04d0b1c30fd41a19f699..55f4c779eb17df9724d0be0e36c086ac93dbb649 100755 (executable)
--- 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 efa35efd5d88ad0362edca5e5a0ccd83d59e7a79..19c460c923f006b502e8f78033e2812829bccf49 100644 (file)
--- 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 0861092e7a58b18e065bfa5beec762c0a40c94cc..24638808508c43417c3c4e6f4be9b3f6a76710dd 100644 (file)
--- 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 64dc608997489ea14aeea0a235a224fe6e918456..b385856e7e72525045b3d94d8e9886edd9b7554e 100644 (file)
--- 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 63bd8c0c15c771a65d9f932b4da5caa886e9d15d..081ada412c75c6d5dc6e55295910daee960037a6 100644 (file)
--- 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 4e5a7b82651d6f996196ada38dc64d0d5a128b08..bffb2b0144cbafeee87889ca813ee6d58ee69382 100644 (file)
--- 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)