From 7b7397c8fd04093e3e50666bc56954133805bd25 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 3 Oct 2012 21:41:15 +0000 Subject: [PATCH] better documentation, allow examples to be installed, etc --- Makefile | 8 +++-- Makefile.builds.in | 1 + contrib/Makefile.am | 1 + contrib/build-cudd-with-libtool.sh | 2 +- examples/Makefile.am | 4 +++ examples/README | 49 ++++++++++++++++++++---------- examples/hashsmt/Makefile.am | 4 +++ examples/nra-translate/Makefile.am | 4 +++ library_versions | 16 ++++++++++ 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 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 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 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) -- 2.30.2