Commit 167477b6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean configuration a bit.

parent 669eda84
......@@ -1190,8 +1190,7 @@ test-runstrat: test-runstrat.$(OCAMLBEST)
ifeq (@enable_doc@,yes)
doc: doc/manual.pdf
# doc/manual.html
doc: doc/manual.pdf doc/html/index.html
BNF = qualid label constant operator term type formula theory theory2 \
why_file spec expr expr2 module whyml_file
......@@ -1212,6 +1211,8 @@ DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
cd doc; $(RUBBER) --warn all --pdf manual.tex
ifeq (@enable_html_doc@,yes)
# the dependency on the pdf ensures the bbl was built
doc/html/manual.html: doc/manual.pdf doc/fix.hva
cd doc; rm -rf html; mkdir -p html
......@@ -1221,6 +1222,12 @@ doc/html/manual.html: doc/manual.pdf doc/fix.hva
doc/html/index.html: doc/html/manual.html
cd doc; $(HACHA) -tocbis -o html/index.html html/manual.html
else
doc/html/manual.html:
endif
clean::
cd doc; rm -rf html; $(RUBBER) --pdf --clean manual.tex
......
......@@ -109,6 +109,10 @@ AC_ARG_ENABLE(doc,
[ --enable-doc build documentation],,
enable_doc=yes)
AC_ARG_ENABLE(html-doc,
[ --enable-html-doc build HTML documentation],,
enable_html_doc=yes)
# profiling
AC_ARG_ENABLE(profiling,
......@@ -276,19 +280,37 @@ if test "$USEOCAMLFIND" = yes; then
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
AC_CHECK_PROG(RUBBER,rubber,rubber,no)
if test "$RUBBER" = no ; then
enable_doc=no
enable_html_doc=no
reason_doc=" (rubber not found)"
AC_MSG_WARN([Cannot find rubber, documentation disabled.])
fi
else
enable_html_doc=no
fi
# checking for hevea
AC_CHECK_PROG(HEVEA,hevea,hevea,no)
if test "$enable_html_doc" = yes ; then
AC_CHECK_PROG(HEVEA,hevea,hevea,no)
if test "$HEVEA" = no ; then
enable_html_doc=no
reason_html_doc=" (hevea not found)"
AC_MSG_WARN([Cannot find hevea, HTML documentation disabled.])
fi
fi
# checking for hacha
AC_CHECK_PROG(HACHA,hacha,hacha,no)
if test "$enable_html_doc" = yes ; then
AC_CHECK_PROG(HACHA,hacha,hacha,no)
if test "$HACHA" = no ; then
enable_html_doc=no
reason_html_doc=" (hacha not found)"
AC_MSG_WARN([Cannot find hacha, HTML documentation disabled.])
fi
fi
# checking for lablgtk2
if test "$enable_ide" = yes ; then
......@@ -487,7 +509,7 @@ fi
if test "$enable_pvs_libs" = yes; then
AC_MSG_CHECKING([for NASA libraries])
enable_pvs_nasa_libs=no
reason_pvs_nasa_libs="(not in PVS_LIBRARY_PATH)"
reason_pvs_nasa_libs=" (not in PVS_LIBRARY_PATH)"
for dir in ${PVS_LIBRARY_PATH//:/ }; do
if test -f $dir/nasalib-version; then
enable_pvs_nasa_libs=yes
......@@ -589,7 +611,11 @@ AC_SUBST(PVSVERSION)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
AC_SUBST(enable_html_doc)
AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)
AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)
......@@ -619,33 +645,43 @@ AC_OUTPUT
echo
echo " Summary"
echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "Compile in native code : $enable_native_code"
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 "Coq support : $enable_coq_support $reason_coq_support"
if test "$enable_coq_support" = "yes" ; then
echo "OCaml compiler : yes"
echo " Version : $OCAMLVERSION"
echo " Library path : $OCAMLLIB"
echo " Native compilation : $enable_native_code"
echo " Profiling : $enable_profiling"
echo "IDE : $enable_ide$reason_ide"
echo "Bench tool : $enable_bench"
echo "Documentation : $enable_doc"
if test "$enable_doc" = yes ; then
echo " HTML : $enable_html_doc"
fi
echo "Coq support : $enable_coq_support$reason_coq_support"
if test "$enable_coq_support" = yes ; then
echo " Version : $COQVERSION"
echo " Lib : $COQLIB"
echo " \"why3\" tactic : $enable_coq_tactic $reason_coq_tactic"
echo " Realization support : $enable_coq_libs $reason_coq_libs"
if test "$enable_coq_libs" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
echo " Library path : $COQLIB"
echo " \"why3\" tactic : $enable_coq_tactic$reason_coq_tactic"
echo " Realization support : $enable_coq_libs$reason_coq_libs"
if test "$enable_coq_libs" = yes ; then
echo " FP arithmetic : $enable_coq_fp_libs$reason_coq_fp_libs"
fi
fi
echo "PVS support : $enable_pvs_support $reason_pvs_support"
if test "$enable_pvs_support" = "yes" ; then
echo "PVS support : $enable_pvs_support$reason_pvs_support"
if test "$enable_pvs_support" = yes ; then
echo " Version : $PVSVERSION"
echo " Lib : $PVSLIB"
echo " Realization support : $enable_pvs_libs $reason_pvs_libs"
if test "$enable_pvs_libs" = "yes" ; then
echo " NASA libraries : $enable_pvs_nasa_libs $reason_pvs_nasa_libs"
echo " Library path : $PVSLIB"
echo " Realization support : $enable_pvs_libs$reason_pvs_libs"
if test "$enable_pvs_libs" = yes ; then
echo " NASA libraries : $enable_pvs_nasa_libs$reason_pvs_nasa_libs"
fi
fi
echo "hypothesis selection : $enable_hypothesis_selection"
echo "profiling : $enable_profiling"
echo "relocatable install : $enable_relocation"
echo "localdir : $enable_local"
echo "Hypothesis selection : $enable_hypothesis_selection"
if test "$enable_local" = yes ; then
echo "Installable : no"
else
echo "Installable : yes"
echo " Binary path : $bindir"
echo " Data path : $datarootdir/why3"
echo " Relocatable : $enable_relocation"
fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment