diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 459e80d888a46cb31fd9c2fbb05cf238377adce0..d881a2b55cc344f4ab925dd1f21d6251f3e56810 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -199,9 +199,18 @@ on the configuration of new libraries. This is done by calling a
predefined macro called
\texttt{configure\_library}\scodeidxdef{configure.in}{configure\_library}\scodeidxdef{configure.in}{configure\_tools}\footnote{For
tools, there is a macro \texttt{configure\_tool} which works in the
- same way as \texttt{configure\_library}.}.
+ same way as \texttt{configure\_library}.}, or its more specialized version
+\texttt{configure\_pkg}\scodeidxdef{configure.in}{configure\_pkg}.
+
+\texttt{configure\_pkg} is meant to be used for checking the presence of
+OCaml libraries that are managed as
+\texttt{findlib}\footnote{\url{http://projects.camlcity.org/projects/findlib.html}}
+packages, which is the case for most modern OCaml libraries nowadays.
+It takes two arguments, the name of the package (as known by \texttt{findlib}),
+and a message that will be displayed if the package is not found.
+
The \texttt{configure\_library} macro takes three arguments. The first one is
-the (uppercase) name of the library, the second one is a filename
+the name of the library, the second one is a filename
which is used by the script to check the availability of the library.
In case there are multiple locations possible for the library, this
argument can be a list of filenames. In this case, the argument must
@@ -213,8 +222,19 @@ argument is a warning message to display if a configuration problem
appears (usually because the library does not exist). Using these
arguments, the script checks the availability of the library.
-Results of this macro are available through two variables which are
-substituted in the files generated by \texttt{configure}.
+Results of these macros are available through variables which are
+substituted in the files generated by \texttt{configure}, where
+\texttt{$library$} stands for the \emph{uppercased}
+version of the library name.
+\begin{itemize}
+\item For \texttt{configure\_pkg}:
+\begin{itemize}
+\item \texttt{HAS\_OCAML\_$library$}
+\scodeidxdef{configure.in}{HAS\_OCAML\_$library$}
+is set to \texttt{yes} or \texttt{no} depending on the availability
+of the library
+\end{itemize}
+\item For \texttt{configure\_library}:
\begin{itemize}
\item \texttt{HAS\_$library$}\scodeidxdef{configure.in}{HAS\_$library$}
is set to \texttt{yes} or \texttt{no} depending on the availability
@@ -222,8 +242,10 @@ substituted in the files generated by \texttt{configure}.
\item \texttt{SELECTED\_$library$}\scodeidxdef{configure.in}{SELECTED\_$library$}
contains the name of the version selected as described above.
\end{itemize}
+\end{itemize}
-When checking for \ocaml{} libraries and object files, remember that
+If checking for \ocaml{} libraries and object files without
+\texttt{configure\_pkg}, remember that
they come in two flavors: bytecode and native
code, which have distinct suffixes. Therefore, you should use the
variables \texttt{LIB\_SUFFIX}\scodeidx{configure.in}{LIB\_SUFFIX}
@@ -253,7 +275,22 @@ configure_library(
\subsection{Addition of Library/Tool Dependencies}\label{conf:dep-lib}
\index{Library!Dependency}\index{Tool!Dependency}
-Dependencies upon external tools and libraries are governed by two macros:
+Dependencies upon OCaml packages (checked by \texttt{configure\_pkg}) are
+governed by two macros:
+
+\begin{itemize}
+\item \texttt{plugin\_require\_pkg($plugin$,$library$)}%
+\scodeidxdef{configure.in}{plugin\_require\_pkg} indicates that
+$plugin$ requires $library$ in order to be compiled.
+\item \texttt{plugin\_use\_pkg($plugin$,$library$)}%
+\scodeidxdef{configure.in}{plugin\_use\_pkg} indicates that
+$plugin$ uses $library$, but can nevertheless be compiled if $library$
+is not installed (potentially offering reduced functionality).
+\end{itemize}
+
+Dependencies upon external tools and libraries (checked by
+\texttt{configure\_library} or \texttt{configure\_tool})
+are governed by two macros:
\begin{itemize}
\item \texttt{plugin\_require\_external($plugin$,$library$)}%
\scodeidxdef{configure.in}{plugin\_require\_external} indicates that
@@ -363,6 +400,13 @@ are met. This is done with the following macro:\scodeidxdef{configure.in}{check\
\begin{configurecode}
check_plugin_dependencies
\end{configurecode}
+It is only after this point that the variables
+\texttt{HAS\_$library$}, \texttt{SELECTED\_$library$}, and
+\texttt{ENABLE\_$plugin$} get their final value. If parts of the
+\texttt{configure} script depends on these variables,
+they should appear after the call to
+\texttt{check\_plugin\_dependencies}.
+
An external plug-in can
have dependencies upon previously installed plug-ins.
However two separately installed plug-ins can not be
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index ba27c451541a528ed4f92ed3065cc70aa2008872..8abcd5df6a1cd67926d25c5ce1f67f9767945b43 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,6 +5,12 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
+\section*{21.0 Scandium}
+\begin{itemize}
+\item \textbf{Configure}: Documentation of \texttt{configure\_pkg},
+\texttt{plugin\_require\_pkg} and \texttt{plugin\_use\_pkg} macros.
+\end{itemize}
+
\section*{20.0 Calcium}
\begin{itemize}
\item \textbf{Ptests}: Documentation of the new directive \texttt{MODULE}.
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 52a414ab8e8a89cf4f304e6afed337ab6268bef9..0c3828b35ff2f37b6daf675d0e6670ce9639c3fc 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -48,40 +48,35 @@ plugin_use(wp,gui)
# Why3 API dependency
######################
-# REQUIRE_LIBRARY: library *must* be present in order to build plugins
-# USE_LIBRARY: better for plugins if library is present, but not required
-# HAS_LIBRARY: is the library available?
-REQUIRE_WHY3=
-USE_WHY3=
-HAS_WHY3=
+configure_pkg(why3,[package why3 not found])
-AC_MSG_CHECKING(for why3 (>= 1.3.1))
+plugin_require_pkg(wp,why3)
+
+check_plugin_dependencies
+
+if test "$HAS_OCAML_WHY3" = "yes"; then
+AC_MSG_CHECKING(why3 version)
WHY3VERSION=`ocamlfind query -format %v why3 | tr -d '\\r\\n'`
case $WHY3VERSION in
+ "")
+ AC_MSG_RESULT([not found!])
+ plugin_disable(wp,[why3 not found])
+ ;;
0.* | 1.[[012]].* | 1.3.0)
- AC_MSG_ERROR(found why3 $WHY3VERSION: requires 1.3.1 or higher.);;
+ AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.1+])
+ plugin_disable(wp,[non-supported why3 $WHY3VERSION])
+ ;;
+ 1.3.*)
+ AC_MSG_RESULT([found $WHY3VERSION: ok])
+ ;;
*)
- AC_MSG_RESULT(found $WHY3VERSION: should work);;
+ AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.1+)])
+ ;;
esac
+fi
-WHY3_PATH=`ocamlfind query why3 | tr -d '\\r\\n'`
-WHY3PATH_FOR_CONFIGURE=$WHY3_PATH
-
-configure_library([WHY3],
- [$WHY3PATH_FOR_CONFIGURE/why3.$LIB_SUFFIX],
- [$WHY3PATH_FOR_CONFIGURE/why3.$LIB_SUFFIX not found.],
- no)
-
-
-plugin_require_external(wp,why3)
-
-AC_SUBST(HAS_WHY3)
-
-
-check_plugin_dependencies
-
-# NB: this would deserve to use plugin_requires mechanism
+# Nb: this would deserve to use plugin_requires mechanism
if test "$ENABLE_WP" != "no"; then
## Configuring for WP-COQ