diff --git a/bin/update_api_doc.sh b/dev/update_api_doc.sh
similarity index 100%
rename from bin/update_api_doc.sh
rename to dev/update_api_doc.sh
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index d91442d48cbb027e748ecdc55fa4054294a7af88..7313f46e5b9f437eb76841a23cb2e767432b599d 100644
--- a/doc/release/branch.tex
+++ b/doc/release/branch.tex
@@ -1,4 +1,5 @@
-\chapter{The Branch Stage}
+\chapter{Branch stage}
+\label{chap:branch}
That is the procedure for forking the release from \texttt{master}.
@@ -54,9 +55,11 @@ in the Frama-C group
\expertise{François, Julien}.
-\section{BTS}
+\section{GitLab issues}
-Check public issue tracker at \url{https://git.frama-c.com/pub/frama-c/issues/} All issues should have been at least acknowledged: at least they should be assigned to someone, preferably tagged appropriately.
+Check public issue tracker at \url{https://git.frama-c.com/pub/frama-c/issues/}.
+All issues should have been at least acknowledged: at least they should be
+assigned to someone, preferably tagged appropriately.
Send a message to the Frama-C channel on LSL's Mattermost.
Each developer should have a
@@ -98,7 +101,6 @@ This should go directly below
\begin{verbatim}
\section*{\framacversion}
\end{verbatim}
-
and this line should be commented out.
\begin{itemize}
@@ -119,11 +121,9 @@ merging back \texttt{stable/element} into \texttt{master}.
\section{Copyright}
-Check that the date in copyright headers is correct. If not then the script
-\texttt{headers/updates-headers.sh} can be used to update them.
-
+Check that the date in copyright headers is correct. If not then:
\begin{itemize}
- \item Update the dates in the license files in:
+ \item update the dates in the license files in:
\begin{itemize}
\item \texttt{headers/close-source/*}
\item \texttt{headers/open-source/*}
@@ -132,13 +132,11 @@ Check that the date in copyright headers is correct. If not then the script
\item \texttt{src/plugins/e-acsl/headers/close-source/*}
\item \texttt{src/plugins/e-acsl/headers/open-source/*}
\end{itemize}
- \item Update the headers with the following commands:
+ \item update the headers with the following command:
\begin{itemize}
- \item \texttt{./headers/updates-headers.sh headers/header\_spec.txt headers/open-source}
- \item \texttt{./headers/updates-headers.sh ivette/headers/header\_spec.txt headers/open-source ivette}
- \item \texttt{./headers/updates-headers.sh src/plugins/e-acsl/headers/header\_spec.txt src/plugins/e-acsl/headers/open-source src/plugins/e-acsl}
+ \item \texttt{make headers}
\end{itemize}
- \item Check if some copyright are left to update by \texttt{grep}-ing the date in the sources: \texttt{grep -r -e "-yyyy" .}
+ \item Check if some copyrights are left to update by \texttt{grep}-ing the date in the sources: \texttt{grep -r -e "-yyyy" .}
\end{itemize}
%%%Local Variables:
diff --git a/doc/release/build.tex b/doc/release/build.tex
deleted file mode 100644
index 898561b60232bc8b40dad66a74f1453b5d9fc62f..0000000000000000000000000000000000000000
--- a/doc/release/build.tex
+++ /dev/null
@@ -1,360 +0,0 @@
-\chapter{The Build Stage}
-
-The procedure for creating the source distribution.
-
-\section{Prerequisites}
-
-\begin{itemize}
-\item All tools needed to compile Frama-C (that you should have anyways)
-\item \texttt{bash} v4.0 or higher
-\item \texttt{git-lfs}
-\item GNU \texttt{parallel}
-\item a \TeX distribution (e.g. \TeX{}live),
-including notably the following utilities:
-\begin{itemize}
-\item \texttt{latexmk}
-\item (recommended) \texttt{texfot}
-\end{itemize}
-\end{itemize}
-
-\section{Final checks}
-
-\begin{itemize}
-
-\item Check plug-in dependencies in all \texttt{configure.*}, in case they have
- changed: if you don't know them, ask plug-in developers to verify them.
-
-\todo{should be done when the plugin is modified}
-
-\item Check the headers and corresponding licenses files for new files
- \todo{should be done when the plugin is modified}
-
-% (\texttt{make check-headers} is your friend, but it is done by CI anyway).
-
-
-\item Check the contents of \texttt{INSTALL.md} \todo{Should always be up to date}
- \begin{itemize}
- \item Update the Frama-C version number in the `Reference configuration` section
- \item In particular, check and update a full known good configuration for
- opam packages, including alt-ergo, why3, coq, etc.
- Use \verb+bin/check-reference-configuration.sh+ to help check if the
- configuration is ok. You can also try running
- \verb+make wp-qualif+.
- \end{itemize}
-\item Check the contents of \texttt{README.md} \todo{Should always be up to date}
-\item Check the contents of \texttt{Changelog}
- \todo{Should always be up to date}
-\item Carefully read the output of the configure to be sure that there are no
- buggy messages. Make sure you have required OPAM packages installed in your machine,
- e.g. alt-ergo.
-\end{itemize}
-
-\section{Update the Sources}\label{sec:update-sources}
-
-There are many administrative steps, coordinated by the release manager.
-\begin{enumerate}
-\item [{\em Non-beta only}] If a new version of the ACSL manual is to be released, make sure you also
- have a clone of the \texttt{acsl} manual Github repository
- (\url{git@github.com:acsl-language/acsl.git}) in the \texttt{doc}
- directory
-\item Update files \texttt{VERSION} and \texttt{VERSION\_CODENAME}
- (for beta releases, add suffix \texttt{\textasciitilde{}beta})
-\item [{\em Non-beta only}] Update file \texttt{ALL\_VERSIONS}. \todo{This section must be put somewhere else in the release manual}
-\item Update files
- \texttt{src/plugins/wp/Changelog} and
- \texttt{src/plugins/e-acsl/doc/Changelog},
- to add the header corresponding to the
- new version. % For the final release, use the script
- % \texttt{doc/changelog/generate} to check that the HTML page can be built,
- % and check its contents.
-\item Update the Frama-C's authors list in files
- \texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}.
- Traditionally, an author is added if they have contributed 100+ LoC in
- the release, as counted by:
- \begin{verbatim}
- git ls-files -z | \
- parallel -0 -n1 git blame --line-porcelain | \
- sed -n 's/^author //p' | sort -f | uniq -ic | sort -nr
- \end{verbatim}
- (source for the command: \url{https://gist.github.com/amitchhajer/4461043})
-\item Recompile and test to check that all is fine.
-\item Check the documentation as per Section~\ref{update_doc}
-\item update the \texttt{opam} directory: update the version name and
- version number in the fields \texttt{version}, \texttt{doc} and
- \texttt{depends} in \texttt{opam/opam}. \textbf{NB:} for a beta version, be sure
- to use a tilde \textasciitilde{} between the version number and \texttt{beta},
- and not a dash \texttt{-}.
-\item Create the last commit
-\item Create the tag using \texttt{git tag \$(cat VERSION | sed -e "s/~/-/")} and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/~/-/")})
-\end{enumerate}
-
-\section{Update the Documentation}\label{update_doc}
-
-\subsection{Manuals}
-
-Most manuals depend on the \texttt{VERSION} file, so make sure to regenerate
-them when this file changes.
-Also, most of the manuals include an appendix with the list of
-changes that have happened, divided by version of Frama-C. Make sure that the
-first section has the correct release name.
-
-\todo{Mention the other things that change from one release to the
- other, such as the ACSL version number}
-
-\todo{The release manager should create fresh Changes sections in \texttt{master}. But When?: at fork time, or when the release is ready?}
-
-
-The official \FramaC documents relative to the kernel and ACSL to be released
-must be recompiled in order to take into account the \texttt{VERSION}
-file:
-
-\begin{center}
- \begin{tabular}{lll}
- \hline
- \textsf{User Manual} &
- \texttt{doc/userman} &
- \expertise{Julien} \\
- \textsf{Developer Manual} &
- \texttt{doc/developer} &
- \expertise{Julien} \\
- \textsf{ACSL Implementation} &
- \texttt{doc/acsl} (from Github) &
- \expertise{Virgile} \\
- % \textsf{man page} &
- % \texttt{man/frama-c.1} &
- % \expertise{Virgile} \\
- \hline
- \end{tabular}
-\end{center}
-
-Documents relative to the plug-ins can be found at the same place. This list
-isn't exhaustive:
-
-\begin{center}
- \begin{tabular}{lll}
- \hline
- \textsf{RTE} &
- \texttt{doc/rte} &
- \expertise{Julien} \\
- \textsf{Aoraï} &
- \texttt{doc/aorai} &
- \expertise{Virgile} \\
- \textsf{Metrics} &
- \texttt{doc/metrics} &
- \expertise{André} \\
- \textsf{Eva} &
- \texttt{doc/eva} &
- \expertise{David} \\
- \textsf{WP} &
- \texttt{src/plugins/wp/doc/manual/} &
- \expertise{Loïc} \\
- \end{tabular}
-\end{center}
-
-Clone the \texttt{acsl} manual
-(\url{git@github.com:acsl-language/acsl.git}) in
-\texttt{doc/acsl} in order to generate the ACSL reference and implementation
-manuals.
-
-% manuals (which uses git-annex) are now deprecated in favor of using the
-% Github wiki
-%Clone the \texttt{manuals} repository
-%(\url{git@git.frama-c.com:frama-c/manuals.git}) in
-%\texttt{doc/manuals} in order to update the manuals (required by the
-%\texttt{install} target below).
-
-In the \texttt{doc} directory, just run \texttt{make all} to compile
-and install all manuals, together with some final coherence checks with
-respect to the current Frama-C implementation (notably
-for the developer manual and ACSL implementation manual).
-
-% No longer use git annex (as recommended by VP)
-%\paragraph{Getting the manuals on the web (ultimately)}
-%
-% In \texttt{doc/manuals} after installing all the manuals:
-%\begin{shell}
-%git annex add .
-%git annex copy . --to origin
-%git commit -am "manuals for release ...."
-%git push
-%\end{shell}
-
-\subsection{API documentation}
-
-To update the \textsf{API} documentation, you must update the
-\texttt{@since} tags. This involves the following script (\texttt{sed -i} must
-work for this purpose):
-\begin{shell}
-./bin/update_api_doc.sh <NEXT>
-\end{shell}
-\verb+<NEXT>+ is the long name of the final release, i.e.
-\verb+`cat VERSION`-`VERSION_CODENAME`+
-(without the \verb+beta+ suffix, if any).
-
-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}
-make -j byte gui-byte
-make doc # or just doc-kernel
-\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}.
-
-\section{Build the Source Distribution}
-\label{sec:build-source-distr}
-
-This steps creates the tarball of Frama-C, the tarball of the API and
-copy them to the website. It also copies the manuals.
-
-\textbf{Note}: all standard plugins must be enabled to ensure they are distributed
-in the \verb+.tar.gz+. Some plug-ins require optional dependencies
-(e.g. markdown-report and \verb+ppx_deriving+), so you must ensure that,
-when running \verb+./configure+, no plugins that should be distributed are missing.
-Some of the checks are performed by the release build script, but not all of them.
-Also, some plug-ins may have components depending on optional packages
-(e.g. Server and \verb+zmq+), which are not always thoroughly tested. If such
-plug-ins are only partially enabled, check that the non-compiled sources are
-distributed in any case, or report it as a bug to their developers.
-
-If you have never run \verb+make src-distrib+, you can try a standalone build
-of the \verb+.tar.gz+ itself, before doing the rest (don't forget to use
-\verb+OPEN_SOURCE=yes+).
-Refer to Appendix \ref{chap:make-src-distrib} if you have problems when
-doing so. In any case, the archive will be recreated by a script, so you can
-skip this step.
-
-You need to have installed \texttt{git-lfs}, otherwise the build
-script will not correctly use lfs when putting large files in the
-website git.
-
-\expertise{release manager} Use the script
-\texttt{build-src-distrib.sh} for this purpose (\texttt{bash version
- 4} required).
-
-The script will search for the following repositories:
-
-\begin{itemize}
- \item \texttt{./doc/acsl} (\texttt{git@github.com:acsl-language/acsl.git})
- \item \texttt{./frama-c.wiki} (\texttt{git@git.frama-c.com:pub/frama-c.wiki.git})
- \item \texttt{./website} (\texttt{git@git.frama-c.com:pub/pub.frama-c.com.git})
-\end{itemize}
-
-If they are not available, they can be cloned by the script.
-
-The following steps will be performed by the script:
-
-\begin{itemize}
- \item compile manuals
- \item build source distribution
- \item build the API bundle
- \item build the documentation companions
- \item update locally the wiki pages
- \item create a new branch for the website
- \item run some sanity checks on the source distribution
- \item generate the \texttt{opam} file
-\end{itemize}
-
-In order to create "ready to deploy" wiki and website pages, a file \texttt{main\_changes.md}
-must be provided. The expected format is:
-
-\begin{lstlisting}
-# Kernel
-
-- item
-- ...
-
-# <Plugin-Name> (Prefer alphabetic order)
-
-- item
-- ...
-
-# ...
-
-\end{lstlisting}
-
-The performed sanity checks are:
-
-\begin{itemize}
- \item verification that no non-free files are distributed,
- \item verification that no non-free plugins are distributed,
- \item no \texttt{/home/user} path can be found in the distribution,
- \item the source code can be compiled and tests succeed.
-\end{itemize}
-
-Note that there are some interactive steps in the script, that ask for user
-approval before going further.
-
-Finally, ensure that locale \verb+en_US.UTF-8+ is available on your system,
-as it is used by the script to ensure a proper encoding of the generated files.
-
-Now, run the script:
-\begin{shell}
-./bin/build-src-distrib.sh
-\end{shell}
-
-The generated files are available in the \texttt{./distributed} repository.
-After testing more extensively the distribution, the following actions should
-be performed:
-
-\begin{itemize}
- \item push stable branch on the public repository
- \item push stable tag on the public repository
- \item push the local Frama-C wiki branch to the public repository
- \item push the generated website branch
-\end{itemize}
-
-\section{Testing the Distribution}
-
-Please check that the distribution (sources and API) is OK:
-\begin{enumerate}
-\item check for possible path/environment leaks in the \texttt{tar.gz}:
- grep for the path where your Frama-C git directory is, e.g.
- \texttt{/home/user/git/frama-c}. It should appear nowhere in the archive.
-\item check that \texttt{./configure \&\& make -j \&\& sudo make install} works fine
- (or check e.g. \texttt{./configure --prefix=\$PWD/build \&\& make -j \&\& make install});
-\item Alternatively, you can use \texttt{docker} to compile the archive against a
- precise configuration:
- \begin{itemize}
- \item \verb+cp distributed/frama-c-<VERSION>.tar.gz developer_tools/docker+
- \item \verb+cd developer_tools/docker+
- \item \verb+make Dockerfile.dev+
- \item \verb+docker build . -t framac/frama-c:dev --target frama-c-gui-slim \+\\
- \verb+ -f Dockerfile.dev --build-arg=from_archive=frama-c-<VERSION>.tar.gz+
- \end{itemize}
-\item test the installed binaries (especially the GUI). (On Linux, OCI tests
- everything but the GUI); If you've taken the \texttt{docker} route, you might
- want to install the \href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script,
- in order to be able to launch
- \verb+x11docker framac/frama-c:dev frama-c-gui+
-\item redo the two steps above on Windows/WSL \expertise{André}\expertise{Allan},
- macOS \expertise{André}\expertise{Loïc}\\\expertise{Thibaud};
- \begin{itemize}
- \item For instance, you can compile and test as follows:
- \item \verb+./configure --prefix="$PWD/build"+
- \item \verb+make+;
- \item \verb+make install+;
- \item \verb+rm -f ~/.why3.conf; why3 config detect+;
- \item \verb+build/bin/frama-c tests/idct/*.c -eva -wp -wp-rte+
- \item If you have a GUI, replace \verb+frama-c+ above with \verb+frama-c-gui+
- and click around, see if things work (e.g. no segmentation faults).
- \end{itemize}
-\item have a look at the documentation of the API (untar, open
- \texttt{index.html} in a browser, click on a few links, etc).
- If there are minor bugs/typos, note them for later, but it's not
- worth delaying the release to fix them.
-\item consider decompressing both the current and the previous release archives
- in different directories, then using \texttt{meld} to compare them. This
- allows spotting if some files were unexpectedly added, for instance.
-\end{enumerate}
-
-
-%%%Local Variables:
-%%%TeX-master: "release"
-%%%End:
diff --git a/doc/release/website.tex b/doc/release/deploy.tex
similarity index 58%
rename from doc/release/website.tex
rename to doc/release/deploy.tex
index 8ebbbb7f7e9972aeafef7f1fd83487f96d5bab4d..3527628644e025447500f58afe9ed185da3565e1 100644
--- a/doc/release/website.tex
+++ b/doc/release/deploy.tex
@@ -1,30 +1,40 @@
-\chapter{The Web Stage}
+\chapter{Deployment stage}
+\label{chap:deploy}
-Where all our efforts goes on the web. There are two very different
-tasks for \FramaC to go online. Authoring the web site pages is the
-responsibility of the developers and the release manager. Publishing
-the web site can only be performed by authorized people, who may not
-be the release manager.
+The validation stage (Chapter~\ref{chap:validation}) must be complete before
+starting this stage. The tasks listed in this section are mostly performed by
+the Release Manager.
-\section{Requirements}
+\section{Release pipeline}
-The website \texttt{README.md} provides a quick guide to locally setup
-the website.
-
-\section{Generate website}
-
-Before pushing the branch to the website, it can be deployed locally but
-this is not absolutely necessary.
-
-Push the branch generated by the release script on the website repository.
-
-You can have a look at the generated pages on \texttt{pub.frama-c.com} (after
-the \texttt{deploy} target of the website's continuous integration has successfully run.
-This can take a few minutes if the server is loaded).
-Note however that the download links won't work as they are available only
-once the branch is merged (\texttt{download} links are handled by Git-LFS).
+Go to the CI/CD section of GitLab. Start the release pipeline:
+\begin{itemize}
+ \item click ``Run Pipeline''
+ \item select the stable branch
+ \item add the variable \texttt{RELEASE} with value \texttt{yes}
+ \item run the pipeline.
+\end{itemize}
-Check the following pages:
+All tests will be run, as well as the \texttt{opam-pin} target and the job that
+create the release artifacts. The most important for the remaining tasks are the
+following:
+\begin{description}
+\item[\texttt{release-content}] has all generated artifacts
+\item[\texttt{release-website}] creates a merge-request assigned to
+ you on the website repository,
+\item[\texttt{release-wiki}] creates a wiki page on the public
+ Frama-C repository (you can see a link in the Activity section),
+\item[\texttt{release-opam}] creates the branch on the opam-repository
+ of the Frama-C organization on GitHub for Opam release,
+\item[\texttt{release-branch}] is ready to push the stable branch on
+ the public repo (it must be started manually)
+\item[\texttt{release-create}] is ready to create the GitLab release
+ on \texttt{pub} (it must be started manually and requires the branch).
+\end{description}
+
+\section{Check the website}
+
+Once the pipeline for the website has run, open \texttt{https://pub.frama-c.com}.
\begin{itemize}
\item \texttt{index.html} must display:
@@ -56,10 +66,7 @@ For a final version, the installation pages for:
\item \texttt{/html/installations/previous\_version\_name.html} should indicate older version
\end{itemize}
-On GitLab, the following files must appear as \textbf{new} in \texttt{download}.
-Note that for beta versions, if you have not included all manuals, not all of
-them will appear:
-
+On GitLab, the following files must appear as \textbf{new} in \texttt{download}:
\begin{itemize}
\item \texttt{acsl-X.XX.pdf}
\item \texttt{acsl-implementation-NN.N-CODENAME.pdf}
@@ -92,6 +99,25 @@ For final release \textbf{ONLY}, the following files must appear as \textbf{modi
\item \texttt{hello.tar.gz}
\end{itemize}
+If everything is fine, merge the website and ask a website maintainer to put it
+online (\expertise{Allan, Augustin}).
+
+\section{Public GitLab}
+
+Open the generated wiki page (visible in the public website activity). Check the
+links (files are available only once the website has been put online). If
+everything is fine, edit the main wiki page and the sidebar with a link to the
+page (\url{https://git.frama-c.com/pub/frama-c/-/wikis/home}).
+
+In the release pipeline, run the job \texttt{release - release-branch}. It will
+push the stable branch on the public repository.
+
+Then, either the release is beta, or not. If the release is a beta, just push
+the tag of the release on the public GitLab. Else, run the job
+\texttt{release - release-create}. After this, the release should
+be available in \url{https://git.frama-c.com/pub/frama-c/-/releases}. As well
+as the tag of the version in \url{https://git.frama-c.com/pub/frama-c/-/tags}.
+
\section{Announcements}
\begin{itemize}
@@ -104,62 +130,10 @@ For final release \textbf{ONLY}, the following files must appear as \textbf{modi
\section{Opam package}
You'll need a GitHub account to create a pull request on the official opam repository,
-\texttt{ocaml/opam-repository.git}.
-
-\begin{itemize}
-\item Clone \texttt{opam-repository}: \texttt{git clone git@github.com:ocaml/opam-repository.git}
-\item Make sure you are on \texttt{master} and your branch is up-to-date
-\item Create a new directory: \\
- \texttt{packages/frama-c/frama-c.<version>}
-\item Copy the file \texttt{./distributed/opam} to the opam repository clone in: \\
- \texttt{packages/frama-c/frama-c.<version>/opam}
-\item You can provide \verb|sha256| and/or \verb|sha512| checksums at the end of this file if ou wish.
-\item (optional) Check locally that everything is fine:
-\begin{verbatim}
-opam switch create local <some-ocaml-compiler-version>
-opam repository add local <path-to-repository-clone>
-opam repository set-repos local
-opam install frama-c
-\end{verbatim}
-(of course, if you already create a local switch before and it uses your
-local version of the repository, you just have to switch to it).
-
-\textbf{Note:} uncommitted changes are ignored by \texttt{opam repository};
-you have to locally commit them before \texttt{opam update} will take them into
-account.
-
-\item Create a branch with any name you want (e.g. frama-c.<version>) and push it to your remote Github
-\item Create a pull request to opam-repository. If all tests pass,
- someone from opam should merge it for you.
- \textbf{Note:} some opam tests may fail due to external circumstances; if the
- error log makes no sense to you, wait to see if someone will contact you
- about it, or ask directly on the merge request.
-\end{itemize}
-
-\section{Updating pub/frama-c}
-
-You'll need to be member of the \texttt{pub/frama-c} project to be able to
-commit to it.
-
-\begin{itemize}
-\item add the \texttt{pub/frama-c} remote to your Git clone;
-\item make sure the last commit is tagged (either a release candidate, or a
- final release);
-\item push the stable/\texttt{<codename>} branch to the \texttt{pub} remote.
-\end{itemize}
-
-({\em Non-beta only}) After pushing the tag to Gitlab, go to the Releases page
-and create a release for the tag.
-
-You should also push the wiki changes. Note that all files listed as \textbf{new}
-in the website section should appear in the wiki but:
-
-\begin{itemize}
- \item \texttt{frama-c-api-NN.N-CODENAME.tar.gz}
- \item \texttt{hello-NN.N-CODENAME.tar.gz}
-\end{itemize}
-
-and E-ACSL files are not in a sub-folder \texttt{e-acsl} on the wiki.
+\texttt{ocaml/opam-repository.git}. Go to the Frama-C GitHub organization opam
+repository (\url{https://github.com/Frama-C/opam-repository}). Find the branch
+corresponding to the release and create the pull-request on the official opam
+repository.
\section{Other repositories to update}
@@ -174,13 +148,12 @@ Check if other Frama-C (and related) repositories need to be updated:
\section{Preparing the Next Release}
-Just update the \texttt{VERSION} file in \texttt{master}, by adding
-\texttt{"+dev"}. Do not add any newline at the end of the
-\texttt{VERSION} file.
+Just update the \texttt{VERSION} file in \texttt{master}, by adding \texttt{"+dev"}.
\section{Docker image preparation}
-\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be able to upload the image.
+\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be
+able to upload the image.
Make sure that \texttt{devel\_tools/docker/Makefile} is up-to-date:
diff --git a/doc/release/intro.tex b/doc/release/intro.tex
index 3c37a442b6952117321a42789d46f157bd005503..7a0434bb42c4edf95410699141d9898e27f4883e 100644
--- a/doc/release/intro.tex
+++ b/doc/release/intro.tex
@@ -20,7 +20,7 @@ roles, and we must distinguish between:
%% \item[Binary Builders:] they are responsible for creating a binary distribution
%% of the release for a specific architecture \expertise{none currently}.
\item[Web Site Maintainers:] they are responsible for updating the web site,
- during the release and for possible later updates \expertise{Florent ? Thibaud ?}.
+ during the release and for possible later updates \expertise{Allan, Augustin}.
\item[Release Manager:] they are responsible for the organisation of the
release process
\end{description}
@@ -30,24 +30,23 @@ roles, and we must distinguish between:
A \FramaC release consists of the following main steps:
\begin{enumerate}
-\item \textbf{The branch stage.} A branch is created, in which the release
- will be prepared. It will ultimately become the released version.
- The development of unstable features may continue in master, while the
- branch is dedicated to the ongoing release.
-
-\item \textbf{The build stage.} The source files are setup by the
- developers, and the bug tracking system is updated to reflect the
- distribution state. A source distribution is created and registered,
- with its updated documentation.
-
-\item \textbf{The web stage.} A snap-shot of the complete web site is
- created, by merging the new release files with the old,
- already distributed ones. %% Some old data might be dropped away if
- %% necessary, although they are still committed somewhere in the
- %% repository.
-
-\item \textbf{The go-online stage}. The web-site snapshot is put on
- the web. Time to notify the world!
+\item \textbf{The branch stage (Chapter~\ref{chap:branch}).} A branch is
+ created, in which the release will be prepared. It will ultimately become the
+ released version. The development of unstable features may continue in master,
+ while the branch is dedicated to the ongoing release.
+
+\item \textbf{The validation stage (Chapter~\ref{chap:validation}).} When we
+ estimate that \FramaC is ready to be released, the bug tracking system is
+ updated to reflect the distribution state. All artifacts that must be
+ distributed are generated in the continuous integration and validated by the
+ Release Manager. The version commit is created and tagged.
+
+\item \textbf{The deployment stage (Chapter~\ref{chap:deploy}).} The Release
+ Manager starts the release pipeline in the continuous integration. The last
+ stage releases the branch, the GitLab release, the website, the wiki and
+ creates an opam repository branch on the Frama-C organisation on GitHub. Time
+ to send an email on the Frama-C discuss mailing list, tweet and spread the
+ world!
\end{enumerate}
diff --git a/doc/release/release.tex b/doc/release/release.tex
index c55488d82ec4a05115a7cf51d188cbec6c0f55f6..08d23cef1011d33c4b193dd4ff969ef19052efbe 100644
--- a/doc/release/release.tex
+++ b/doc/release/release.tex
@@ -17,8 +17,8 @@
\input{intro}
\input{branch}
-\input{build}
-\input{website}
+\input{validation}
+\input{deploy}
\input{standalone-src}
\end{document}
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5a73843cb085290b46dfe7605d806ce4e11580e7
--- /dev/null
+++ b/doc/release/validation.tex
@@ -0,0 +1,201 @@
+\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/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}
+
+The tasks listed in this section are performed by the Release Manager.
+
+\subsection{Versions in documentation files}
+
+Check 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{VERSION\_CODENAME}
+ \item \texttt{Changelog}
+ \item \texttt{src/plugins/wp/Changelog}
+ \item \texttt{src/plugins/e-acsl/doc/Changelog}
+ \item \texttt{INSTALL.md} ("Reference configuration")
+ \item \texttt{opam/opam} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
+\end{itemize}
+
+\subsection{Versions in source: API documentation}
+
+To update the \textsf{API} documentation, you must update the \texttt{@since}
+tags. This involves the following script (\texttt{sed -i} must work for this
+purpose):
+\begin{shell}
+./dev/update_api_doc.sh <NEXT>
+\end{shell}
+\verb+<NEXT>+ is the long name of the final release, i.e.
+\verb+`cat VERSION`-`VERSION_CODENAME`+
+(without the \verb+beta+ suffix, if any).
+
+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.
+
+Also, most of the manuals include an appendix with the list of changes that have
+happened, divided by version of Frama-C. Make sure that the first section has
+the correct release name.
+
+Manuals experts:
+\begin{center}
+ \begin{tabular}{lll}
+ \hline
+ \textsf{User Manual} & \texttt{doc/userman} & \expertise{Julien} \\
+ \textsf{Developer Guide} & \texttt{doc/developer} & \expertise{Julien} \\
+ \textsf{ACSL} & (from Github) & \expertise{Virgile} \\
+ \textsf{Aoraï} & \texttt{doc/aorai} & \expertise{Virgile} \\
+ \textsf{E-ACSL} & \texttt{src/plugins/e-acsl/doc/*} & \expertise{Julien} \\
+ \textsf{Eva} & \texttt{doc/eva} & \expertise{David} \\
+ \textsf{Metrics} & \texttt{doc/metrics} & \expertise{André} \\
+ \textsf{RTE} & \texttt{doc/rte} & \expertise{Julien} \\
+ \textsf{WP} & \texttt{src/plugins/wp/doc/manual/} & \expertise{Loïc} \\
+ \end{tabular}
+\end{center}
+
+\subsection{Contributors}
+
+Update the Frama-C's authors list in files
+\texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}. Traditionally,
+an author is added if they have contributed 100+ LoC in the release, as counted
+by:
+\begin{verbatim}
+git ls-files -z | \
+parallel -0 -n1 git blame --line-porcelain | \
+sed -n 's/^author //p' | sort -f | uniq -ic | sort -nr
+\end{verbatim}
+(source for the command: \url{https://gist.github.com/amitchhajer/4461043})
+
+\subsection{Commit}
+
+Commit any change that you have done during these checks \textbf{and push}.
+
+\section{Last pipeline artifacts validation}
+
+In the last continuous integration pipeline of the release branch, force the
+run of the following targets:
+\begin{itemize}
+ \item manuals
+ \item opam-pin
+\end{itemize}
+Both should succeed. Collect the artifacts of the following targets:
+\begin{itemize}
+ \item api-doc
+ \item build-distrib-tarball
+ \item manuals
+\end{itemize}
+
+Check that these artifacts are as expected. In particular:
+\begin{itemize}
+ \item API documentatation:
+ \begin{itemize}
+ \item check that you can browse the API documentation
+ \item if there are minor bugs/typos, note them for later, but it's not
+ worth delaying the release to fix them.
+ \end{itemize}
+ \item Check versions in manuals
+ \item Tarball
+ \begin{itemize}
+ \item Check that no non-free components are distributed
+ \item Check that no \texttt{/home/user} path can be found in the distribution,
+ \item Build and test
+ \begin{itemize}
+ \item on Linux (the CI has already done it, but the GUI is not tested)
+ \item on MacOS \expertise{André, Loïc}
+ \item on Windows (WSL) \expertise{Allan, André}
+ \end{itemize}
+ \item consider decompressing both the current and the previous release
+ archives in different directories, then using \texttt{meld} to compare
+ them. This allows spotting if some files were unexpectedly added, for
+ instance.
+ \end{itemize}
+\end{itemize}
+
+Alternatively, you can use \texttt{docker} to compile the archive against a
+precise configuration:
+\begin{itemize}
+ \item \verb+cp distributed/frama-c-<VERSION>.tar.gz developer_tools/docker+
+ \item \verb+cd developer_tools/docker+
+ \item \verb+make Dockerfile.dev+
+ \item \verb+docker build . -t framac/frama-c:dev --target frama-c-gui-slim \+\\
+ \verb+ -f Dockerfile.dev --build-arg=from_archive=frama-c-<VERSION>.tar.gz+
+\end{itemize}
+For the GUI: you might want to install the
+\href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script, in
+order to be able to launch \verb+x11docker framac/frama-c:dev frama-c-gui+
+
+\section{Validate release}
+
+Create the main changes file in the directory \texttt{releases}. This file must
+be named <VERSION without ext>.md (e.g. \texttt{25.0}: \texttt{25.0.md},
+\texttt{25.0~beta}: \texttt{25.0.md}, \texttt{25.1}: \texttt{25.1.md}). The
+expected format is:
+
+\begin{lstlisting}
+ # Kernel
+
+ - item
+ - ...
+
+ # <Plugin-Name> (Prefer alphabetic order)
+
+ - item
+ - ...
+
+ # ...
+\end{lstlisting}
+
+It should only list main changes, that will be displayed on the event section
+of the website and the wiki page.
+
+Create the version commit, tag it using \texttt{git tag \$(cat VERSION | sed -e "s/~/-/")}
+and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/~/-/")}).
+
+%%%Local Variables:
+%%%TeX-master: "release"
+%%%End: