add checks in configure + some cosmetic changes

Makefile.in

-
 ##########################################################################
 #                                                                        #
 #  Copyright (C) 2010-                                                   #
@@ -71,13 +70,15 @@ else
   MENHIRLIB =
 endif
 
+RUBBER = @RUBBER@
+
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
 BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES)
 OFLAGS = -w Ae -dtypes    -I src $(INCLUDES)
 
-ifeq (@ENABLE_PROFILING@,yes)
+ifeq (@enable_profiling@,yes)
 OFLAGS += -g -p
 STRIP = true
 endif
@@ -215,6 +216,7 @@ clean::
 ###############
 # installation
 ###############
+
 install_no_local::
 	mkdir -p $(BINDIR)
 	mkdir -p $(LIBDIR)/why3
@@ -240,13 +242,13 @@ install_no_local_lib::
 	cp -f META  $(OCAMLLIB)/why3
 	if test -f src/why.a; then cp -f src/why.a $(OCAMLLIB)/why3; fi
 
-ifeq ("@ENABLE_LOCAL@","no")
+ifeq (@enable_local@,yes)
+install install-lib:
+	@echo "Why is configured in local installation mode."
+	@echo "To install Why, run ./configure --disable-local ; make ; make install"
+else
 install: install_no_local
 install-lib: install_no_local_lib
-else
-install install-lib:
-	@echo "You use a local configuration you can't install with it."
-	@echo "Run ./configure without --enable-local"
 endif
 
 install-all: install install-lib
@@ -282,7 +284,7 @@ install_no_local::
 # Whyml
 ########
 
-PGMGENERATED = 
+PGMGENERATED =
 
 PGM_FILES = pgm_ttree pgm_types pgm_pretty \
 	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
@@ -459,6 +461,8 @@ endif
 # BENCH
 ###############
 
+ifeq (@enable_bench@,yes)
+
 BENCH_FILES = bench benchrc whybench
 
 BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
@@ -507,10 +511,14 @@ clean::
 install_no_local::
 	cp -f bin/whybench.@OCAMLBEST@ $(BINDIR)/why3bench
 
+endif
+
 ##############
 # Coq plugin
 ##############
+
 ifeq (@enable_coq_support@,yes)
+
 COQGENERATED = src/coq-plugin/g_whytac.ml
 
 COQ_FILES = whytac g_whytac
@@ -558,10 +566,13 @@ clean::
 	rm -f .depend.coq
 
 endif
+
 ########
 # Tptp2why
 ########
+
 ifeq (@enable_whytptp@,yes)
+
 TPTPGENERATED = src/tptp2why/tptpLexer.ml \
 	src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
 
@@ -580,7 +591,7 @@ $(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
 # build targets
 
 plugins.byte byte: plugins/whytptp.cmo
-plugins.opt  opt :  plugins/whytptp.cmxs
+plugins.opt  opt : plugins/whytptp.cmxs
 
 plugins/whytptp.cmxs plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
 plugins/whytptp.cmxs plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
@@ -602,12 +613,10 @@ plugins/whytptp.cmxs: plugins src/tptp2why/whytptp.cmxs
 plugins/whytptp.cmo: plugins src/tptp2why/whytptp.cmo
 	@cp src/tptp2why/whytptp.cmo $@
 
-
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/plugins
 	cp -f plugins/whytptp.cm* $(LIBDIR)/why3/plugins
 
-
 # depend and clean targets
 
 include .depend.tptp2why
@@ -626,6 +635,7 @@ clean::
 	rm -f .depend.tptp2why
 
 endif
+
 #######
 # tools
 #######
@@ -755,7 +765,9 @@ test-api: src/why.cma
 
 
 ## Examples : Plugins ##
+
 ifeq (@enable_plugins@,yes)
+
 PLUGDIR = examples/plugins/
 PLUG_FILES = genequlin
 
@@ -794,13 +806,18 @@ clean::
 	rm -f $(PLUGDIR)/*.annot $(PLUGDIR)/*~
 	rm -f $(PLUGGENERATED)
 	rm -f .depend.plug
+
 endif
 
 ################
 # documentation
 ################
 
-DOC = doc/manual.pdf
+.PHONY: doc
+
+ifeq (@enable_doc@,yes)
+
+doc: doc/manual.pdf
 # doc/manual.html
 
 BNF = qualid constant operator term type formula theory
@@ -815,16 +832,20 @@ doc/bnf: doc/bnf.mll
 
 doc: $(DOC)
 
-.PHONY:$(DOC)
-
 doc/manual.pdf: $(BNFTEX) doc/apidoc.tex doc/manual.tex doc/version.tex
-	cd doc; rubber -d manual.tex
+	cd doc; $(RUBBER) -d manual.tex
 
 # doc/manual.html: doc/manual.tex doc/version.tex
 # 	$(MAKE) -C doc manual.html
 
 clean::
-	cd doc; rubber -d --clean manual.tex
+	cd doc; $(RUBBER) -d --clean manual.tex
+
+else
+
+doc:
+
+endif
 
 ##########
 # API DOC
@@ -835,7 +856,7 @@ clean::
 MODULESTODOC = util/util util/hashweak \
 	core/ident core/ty core/term core/decl core/theory \
 	core/env core/task \
-	driver/whyconf driver/driver 
+	driver/whyconf driver/driver
 #	transform/introduction \
 #	ide/db
 
@@ -960,7 +981,7 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure .depend.* \
 
 distrib:: $(DISTRIB_TAR)
 
-rmdistrib: 
+rmdistrib:
 	rm -rf $(DISTRIB_DIR)
 
 redistrib: rmdistrib distrib
@@ -972,6 +993,10 @@ $(DISTRIB_TAR): doc/manual.pdf
         fi
 	mkdir -p $(DISTRIB_DIR)
 	mkdir -p $(DISTRIB_DIR)/bin
+	mkdir -p $(DISTRIB_DIR)/share
+	ln -s ../drivers $(DISTRIB_DIR)/share/drivers
+	ln -s ../modules $(DISTRIB_DIR)/share/modules
+	ln -s ../theories $(DISTRIB_DIR)/share/theories
 	cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
 	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
 

configure.in

@@ -51,6 +51,7 @@
 
 # check for one particular file of the sources
 # ADAPT THE FOLLOWING LINE TO YOUR SOURCES!
+
 AC_INIT(src/)
 
 # verbosemake
@@ -62,9 +63,8 @@ AC_ARG_ENABLE(verbose-make,
 # LOCAL_CONF
 
 AC_ARG_ENABLE(local,
-    [  --enable-local            use only WHY3 in the build directory],,
-    ENABLE_LOCAL=no)
-
+    [  --enable-local          use Why3 in the build directory (no installation)],,
+    enable_local=no)
 
 # IDE
 
@@ -72,6 +72,12 @@ AC_ARG_ENABLE(ide,
     [  --enable-ide            enable Why3 IDE],,
     enable_ide=yes)
 
+# Bench
+
+AC_ARG_ENABLE(bench,
+    [  --enable-bench          enable Why3 benchmarking tool],,
+    enable_bench=yes)
+
 # dynlink
 
 AC_ARG_ENABLE(plugins,
@@ -102,11 +108,17 @@ AC_ARG_ENABLE(hypothesis-selection,
     [  --enable-hypothesis-selection    enable hypothesis selection support],,
     enable_hypothesis_selection=yes)
 
+# documentation
+
+AC_ARG_ENABLE(doc,
+    [  --enable-doc            build documentation],,
+    enable_doc=yes)
+
 # profiling
-ENABLE_PROFILING=yes
+
 AC_ARG_ENABLE(profiling,
     [  --enable-profiling      enable profiling],,
-    ENABLE_PROFILING=no)
+    enable_profiling=no)
 
 # Check for arch/OS
 
@@ -250,16 +262,25 @@ if test "$enable_menhirlib" = yes ; then
 AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
 fi
 
+# checking for rubber
+AC_CHECK_PROG(RUBBER,rubber,rubber,no)
+if test "$enable_doc" = yes ; then
+if test "$RUBBER" = no ; then
+    enable_doc=no
+    AC_MSG_WARN(cannot find rubber, documentation building disabled.)
+fi
+fi
+
 # checking for lablgtk2
 if test "$enable_ide" = yes ; then
 AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
 if test "$enable_ide" = no; then
-   AC_MSG_WARN("Lib lablgtk2 not found, IDE disabled.)
+   AC_MSG_WARN(Lib lablgtk2 not found, IDE disabled.)
    reason_ide=" (lablgtk2 not found)"
 else
    AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
    if test "$enable_ide" = no; then
-     AC_MSG_WARN("Lib lablgtksourceview2 not found, IDE disabled.)
+     AC_MSG_WARN(Lib lablgtksourceview2 not found, IDE disabled.)
    reason_ide=" (lablgtksourceview2 not found)"
    fi
 fi
@@ -269,11 +290,18 @@ fi
 if test "$enable_ide" = yes ; then
    AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
    if test "$enable_ide" = no; then
-     AC_MSG_WARN("Lib sqlite3 not found, IDE disabled.)
+     AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
    reason_ide=" (sqlite3 not found)"
    fi
 fi
 
+# checking for sqlite3
+if test "$enable_bench" = yes ; then
+   AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_bench=no)
+   if test "$enable_bench" = no; then
+     AC_MSG_WARN(Lib sqlite3 not found, why3bench disabled.)
+   fi
+fi
 
 dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
 
@@ -328,14 +356,13 @@ reason_coq_support=" (not yet implemented)"
 # hypothesis_selection
 
 if test "$enable_hypothesis_selection" = yes; then
-  AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes,enable_hypothesis_selection=no)
+  AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,,enable_hypothesis_selection=no)
 fi
 
-if test "$ENABLE_LOCAL" = no; then
-   LOCALDIR=None
+if test "$enable_local" = no; then
+   LOCALDIR='None'
 else
    LOCALDIR='Some \"$PWD\"'
-   ENABLE_LOCAL=yes
 fi
 
 #For the META
@@ -380,15 +407,17 @@ AC_SUBST(OCAMLDOC)
 AC_SUBST(OCAMLBEST)
 AC_SUBST(OCAMLVERSION)
 AC_SUBST(OCAMLLIB)
-AC_SUBST(ENABLE_PROFILING)
 dnl AC_SUBST(OCAMLV)
 dnl AC_SUBST(FORPACK)
 dnl AC_SUBST(OCAMLGRAPHLIB)
 dnl AC_SUBST(OCAMLWEB)
 
+AC_SUBST(enable_profiling)
+
 AC_SUBST(CAMLP5O)
 
 AC_SUBST(enable_ide)
+AC_SUBST(enable_bench)
 AC_SUBST(enable_plugins)
 AC_SUBST(DYNLINK)
 AC_SUBST(META_DYNLINK)
@@ -406,8 +435,11 @@ AC_SUBST(enable_menhirlib)
 
 AC_SUBST(enable_hypothesis_selection)
 
+AC_SUBST(enable_doc)
+AC_SUBST(RUBBER)
+
+AC_SUBST(enable_local)
 AC_SUBST(LOCALDIR)
-AC_SUBST(ENABLE_LOCAL)
 
 dnl AC_SUBST(PSVIEWER)
 dnl AC_SUBST(PDFVIEWER)
@@ -431,6 +463,8 @@ echo "OCaml version           : $OCAMLVERSION"
 echo "OCaml library path      : $OCAMLLIB"
 echo "Verbose make            : $enable_verbose_make"
 echo "Why IDE                 : $enable_ide $reason_ide"
+echo "Why bench tool          : $enable_bench"
+echo "Why documentation       : $enable_doc"
 echo "Why plugins             : $enable_plugins"
 echo "Coq plugin support      : $enable_coq_support $reason_coq_support"
 if test "$enable_coq_support" = "yes" ; then
@@ -440,5 +474,5 @@ fi
 echo "TPTP parser             : $enable_whytptp"
 echo "Menhir library          : $enable_menhirlib"
 echo "hypothesis selection    : $enable_hypothesis_selection"
-echo "profiling               : $ENABLE_PROFILING"
-echo "localdir                : $ENABLE_LOCAL"
+echo "profiling               : $enable_profiling"
+echo "localdir                : $enable_local"