Merge branch...

Merge branch '865-cannot-compile-frama-c-if-a-why3-version-unwanted-by-wp-is-installed' into 'stable/scandium'

Resolve "Cannot compile Frama-C if a why3 version unwanted by WP is installed."

See merge request frama-c/frama-c!2673

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

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}.

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