validation.tex

\chapter{Validation stage}
\label{chap:validation}

Final validation before running the release pipeline.

\section{Prerequisites on dependencies}

Install all dependencies of Frama-C, including recommended ones.

Check coherence between:
\begin{itemize}
  \item \texttt{opam} \todo{Should always be up to date}
  \item \texttt{reference-configuration.md} \todo{Should always be up to date}
\end{itemize}

Run the command:
\begin{itemize}
  \item \texttt{dune build @frama-c-configure}
\end{itemize}
all plugins should be enabled. Check dependencies in case they have changed.
If you don't know them, ask plug-in developers to verify them.

\section{Prerequisites on installation}

\begin{itemize}
  \item Check the contents of \texttt{INSTALL.md} \todo{Should always be up to date}
  \item Check the contents of \texttt{README.md} \todo{Should always be up to date}
\end{itemize}

\section{Fix version}
\label{sec:validation:version}

The tasks listed in this section are performed by the Release Manager.

\subsection{Versions in documentation files}

Change version and codename in the following files:
\begin{itemize}
  \item \texttt{ALL\_VERSIONS} (non-beta only)
  \item \texttt{VERSION} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
  \item \texttt{opam}
  \begin{itemize}
     \item change version (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
     \item change doc link: \texttt{…/download/user-manual-<version>-<codename>.pdf}
           (with \texttt{-beta} in version for beta releases, not \texttt{\textasciitilde{}beta})
  \end{itemize}
\end{itemize}

\subsection{Versions in source: API documentation}

Check that no \verb|+dev| suffix remains inside comments:

\begin{shell}
git grep +dev src
\end{shell}

Test by recompiling Frama-C and rebuilding the API documentation:
\begin{shell}
dune build @install
dune build @doc
\end{shell}

You can also check that the elements referred to in the index of the
development guide are marked as such in the API doc and vice-versa
by issuing \texttt{make check-devguide}\todo{Fix this}.

\subsection{Manuals}

Manuals are built by the continuous integration. However, the Release Manager
should check whether a new version of ACSL or E-ACSL must be released.