Merge branch 'feature/distrib/improve-distrib-creation' into 'master'

Improve Frama-C distribution creation

Closes #984

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

.gitignore

@@ -34,6 +34,7 @@ autom4te.cache
 /config.log
 /config.status
 /frama-c-*.tar.gz
+/distributed
 /.log.autoconf
 /.Makefile.user
 /ocamlgraph/

doc/build-manuals.sh

@@ -39,14 +39,20 @@ fi
 build () {
 
     echo "##### Building $1"
-    make -C $(dirname $1) $(basename $1) || \
-         (echo "######### $1 failed" ; exit 1)
-    echo "##### $1 done"
+    set +e
+    make -C $(dirname $1) $(basename $1)
+    ret=$?
+    if [ $ret -eq 0 ]; then
+        echo "##### $1 done"
+    else
+        echo "######### $1 failed"
+        exit 1
+    fi
     # extract extension, add suffix, re-append extension
     MANUAL=${2%.*}-$3.${2##*.}
     cp -f $1 manuals/$MANUAL
     echo "##### $MANUAL copied"
-    ln -srf manuals/$MANUAL manuals/$2
+    
 }
 
 EACSL_DOC=../src/plugins/e-acsl/doc

doc/release/branch.tex

@@ -21,6 +21,9 @@ $\rightarrow$ Repository $\rightarrow$ Protected Branches.
 
 \section{Creating the branch}
 
+Note that you must be member of the GitLab groups "frama-c", "dev" and have
+access to each plugin of continuous integration.
+
 Create the branch \texttt{stable/release}, where \texttt{release} is the
 element name, using the \texttt{frama-ci} tool:
 \begin{enumerate}
@@ -64,7 +67,7 @@ the issues should be tagged with the current release, or with the next one.
 
 Create headers in the Changelog(s). This is to avoid some merge conflicts,
 but also so that merge requests add information in the proper part of
-the Changelog.   
+the Changelog.
 
 \begin{itemize}
 \item Add the following in the Changelog, in \texttt{stable/element}
@@ -86,7 +89,7 @@ This should go directly below
 
 From now on, Changelog items corresponding to MR merged into \texttt{master}
 must be placed between these two banners. This should minimize conflicts when
-merging back \texttt{stable/element} into \texttt{master}
+merging back \texttt{stable/element} into \texttt{master}.
 
 \todo{Do the same thing in the manuals that contain a Changelog?}
 

doc/release/build.tex

@@ -7,9 +7,11 @@ The procedure for creating the source distribution.
 \begin{itemize}
 \item All tools needed to compile Frama-C (that you should have anyways)
 \item \texttt{bash} v4.0 or higher
+\item \texttt{rgrep}
 \item \texttt{git-lfs}
 \item GNU \texttt{parallel}
 \item a \TeX distribution
+\item (recommended) \texttt{texfot}
 \end{itemize}
 
 \section{Final checks}
@@ -33,7 +35,7 @@ The procedure for creating the source distribution.
     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+ptests.opt -config qualif src/plugins/wp/tests+.
+    \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}
@@ -235,16 +237,60 @@ website git.
 
 \expertise{release manager} Use the script
 \texttt{build-src-distrib.sh} for this purpose (\texttt{bash version
-  4} required) after cloning the following repositories
+  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 \texttt{pub-frama-c} (\texttt{git@git.frama-c.com:pub/frama-c}),
-\item \texttt{frama-c.wiki} (\texttt{git@git.frama-c.com:pub/frama-c.wiki}), and
-\item \texttt{website} (\texttt{git@git.frama-c.com:frama-c/website})
+  \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 the root directory of Frama-C. The last one is only needed when creating a
-final release. Release candidates are pushed as a branch \texttt{stable/<codename>}
-and added to the \texttt{pub/frama-c} wiki.
-For \texttt{website}, a new branch should be created over \texttt{online}.
+
+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.
@@ -254,17 +300,21 @@ Now, run the script:
 ./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 Inspect the contents of the \texttt{tar.gz}:
-  \begin{enumerate}
-  \item Extract it to a new directory.
-  \item run \texttt{<path-to-frama-c-git-clone>/doc/release/checktar.sh}
-    (CWD must be where the tar was extracted). Fix issues and/or update
-    the script if needed.
-  \end{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.
@@ -272,8 +322,8 @@ Please check that the distribution (sources and API) is OK:
   (or check e.g. \texttt{./configure --prefix=\$PWD/build \&\& make -j \&\& make install});
 \item test the installed binaries (especially the GUI). (On Linux, OCI tests
   everything but the GUI);
-\item redo the two steps above on Windows/WSL \expertise{André/Allan}, macOS
-  \expertise{André/Loïc/Thibaud};
+\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"+

doc/release/checktar.sh

-#!/bin/bash -eu
+#!/usr/bin/env bash
 
-echo "To check: "
+if [[ "$1" == "" ]]; then
+    DIR="."
+else
+    DIR=${1%/}
+fi
 
-find . -name '*NE_PAS_LIVRER*'
-find . -name '*nonfree*' -o -name '*non_free*' -o -name '*non-free*'
+ERROR_CODE=0
+
+RESULT=$(find $DIR -name '*NE_PAS_LIVRER*')
+if [[ "$RESULT" != "" ]]; then
+    echo "### ERROR: The following files should not be distributed:"
+    echo $RESULT
+    ERROR_CODE=1
+fi
+
+RESULT=$(find $DIR -name '*nonfree*' -o -name '*non_free*' -o -name '*non-free*')
+if [[ "$RESULT" != "" ]]; then
+    echo "### ERROR: The following files should not be distributed:"
+    echo $RESULT
+    ERROR_CODE=1
+fi
 
 PLUGINS=( genassigns mthread volatile acsl-importer caveat-importer cfp security pathcrawler a3export )
 
 for A in ${PLUGINS[@]}
 do
-    if [ -e src/plugins/$A ]; then
-        echo "!!! Error: trying to release $A"
+    if [ -e $DIR/src/plugins/$A ]; then
+        echo "### ERROR: Trying to release plugin: $A"
+        ERROR_CODE=1
     fi
 done
+
+RESULT=$(rgrep $HOME $DIR)
+
+if [[ "$RESULT" != "" ]]; then
+    echo "### ERROR: Found some $HOME occurrences in the distribution"
+    echo $RESULT
+    ERROR_CODE=1
+fi
+
+exit $ERROR_CODE

doc/release/website.tex

-\chapter{The Website Stage}
+\chapter{The Web Stage}
 
 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
@@ -8,131 +8,75 @@ be the release manager.
 
 \section{Requirements}
 
-You need the following applications:
-\begin{itemize}
-\item \texttt{pandoc}>=2.0; if your distribution has an older
-  version, you can find installation instructions at
-  \url{https://github.com/jgm/pandoc/blob/master/INSTALL.md}
-\item \texttt{tidy}
-\item \texttt{linkchecker}
-\end{itemize}
-
-\section{Authoring the Pages}
-
-The website sources are in \texttt{src}. Go to this directory.
-
-\subsection{Editing Web Pages}
+The website \texttt{README.md} provides a quick guide to locally setup
+the website.
 
-You should consult and/or improve the \texttt{README} for style
-instructions, and edit \texttt{*.prehtml} files.
+\section{Generate website}
 
-Compile the web pages with:
-\begin{shell}[gobble=2]
-  \$ make local
-\end{shell}
+Before pushing the branch to the website, it can be deployed locally but
+this is not absolutely necessary.
 
-This way, you get a snapshot of the web-site in \texttt{src},
-without any downloadable resources. You can start browsing at
-\texttt{index.html}. Note that the new news and download pages still
-need to be manually updated.
+Push the branch generated by the release script on the website repository.
 
-\subsection{Adding News}
-The news are defined in the \texttt{news.def} page. All the news
-are published in the \textsf{RSS} of \FramaC. Only the first news are
-published on the home page of the web site. The limit is marked with:
-\begin{shell}
-  <#def end-of-html-news></#def>
-\end{shell}
+You can have a look at the generated pages on \texttt{pub.frama-c.com}.
+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).
 
-Move it upward in order to keep only few interesting news on the
-\FramaC home page.
+Check the following pages:
 
-\section{Adding the new Release}
-
-From the build stage, the files to distributed are available in the
-\texttt{website} repository and already ready to commit (look at
-\texttt{git status}). The release manager should update the web pages
-of the \emph{download} and \emph{support} sections to make the new
-release and documentation available.
-
-The current (\emph{awkward}) procedure is as follows:
-\begin{enumerate}
-\item In case a new release of ACSL is done together with Frama-C's release;
-  \begin{itemize}
-  \item copy the ACSL manual using the ``numeric'' version
-    (\texttt{www/download/acsl\_x.y.pdf}) and add it via \texttt{git add}
-    (\texttt{git lfs} should automatically handle it, since it's a .pdf);
-  \item check that \texttt{www/download/acsl.pdf} was updated by the build script;
-%  \item update \texttt{src/download.def} (can't find where???);
-  \item update \texttt{src/acsl.prehtml}: add a new entry for the new version of ACSL
- \end{itemize}
-\item Copy the file \texttt{INSTALL.md} from Frama-C to
-  \texttt{INSTALL-NAME.md} where \texttt{NAME} is the version name of the
-  distribution.
-\item Update the \texttt{Makefile} in \texttt{src}:
+\begin{itemize}
+  \item \texttt{index.html} must display:
   \begin{itemize}
-  \item Add to variable \texttt{PAGES} the new files to export (at least
-    install-<version>.html, following the pattern already present). This will
-    create a target that will generate it from the previous .md file.
-  \item Add the previous latest version to the \texttt{DOWNLOAD\_PAGES}
-    variable for adding a specific downloading page related to that
-    previous release.
+    \item the new event,
+    \item a link to the (beta) release at the bottom.
   \end{itemize}
-\item Update also some macros of \texttt{download.def} file:
-  \begin{enumerate}
-  \item Add an entry after the \texttt{selector-previous-versions} macro.
-  \item Update macros \texttt{latest-No-Version}, \texttt{previous-version} and
-    \texttt{previous-No-Version}.
-  \item Move the definition of \texttt{download-last-version} macro
-  to a new macro \texttt{download\_NAME}, where \texttt{NAME}
-  is the version name added to \texttt{DOWNLOAD\_PAGES} variable of the
-  \texttt{Makefile}.
-  \item Update the definition of \texttt{download-last-version} macro.
-  \item Add a new \texttt{selector-download\_NAME} macro.
-  \item Add a link back to that downloading page into the \texttt{selector-download\_PREVIOUS\_NAME} macro.
-  \item Check the occurrences of references to the previous release
-  resources, and update them. A good practice is to \texttt{grep}
-  \texttt{*.prehtml} \texttt{*.def} against the name of the release.
-  You should at least update the links to reference documentation from the
-  \texttt{support.prehtml} page.
-  \end{enumerate}
-\item Build the web site:
-  \begin{shell}[gobble=4]
-    \$ make local
-    \$ make distrib
-  \end{shell}
-  You get a snapshot of the repository in the \texttt{www} directory.
-  Before going there, check for compliance with \textsf{W3C} and link
-  consistency by running:
-  \begin{shell}
-    \$ make check_link
-  \end{shell}
-  Run it and check the result, fixing broken links if necessary.
-  Go to \texttt{../www}, then open \texttt{index.html} and test the website
-  carefully, especially:
+  \item \texttt{/fc-versions/<version\_name>.html}:
   \begin{itemize}
-  \item the new Downloads page;
-  \item the previous Downloads page;
-  \item Compilation instructions;
-  \item Changelog (check parsing, for all plug-ins).
+    \item check Changelog link,
+    \item check manual links (reminder: the links are dead at this moment), it must contain \texttt{NN.N-Version}
+    \item check ACSL version.
   \end{itemize}
+  \item \texttt{/html/changelog.html\#Version-NN.N}
+  \item \texttt{/html/installations/titanium.html}
+  \item \texttt{/html/acsl.html}: check ACSL versions list
+  \item \texttt{rss.xml}: check last event
+\end{itemize}
 
-\item Commit the web site:
-  \begin{shell}
-    \$ cd ..
-    \$ # manually check that only wanted new files are present
-    \$ git add .
-    \$ git checkout -b \$RELEASE
-    \$ git commit -m "updating distrib website"
-  \end{shell}
-\end{enumerate}
+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:
 
-\section{Publishing}
+\begin{itemize}
+  \item \texttt{acsl-X.XX.pdf}
+  \item \texttt{acsl-implementation-NN.N-CODENAME.pdf}
+  \item \texttt{plugin-development-guide-NN.N-CODENAME.pdf}
+  \item \texttt{user-manual-NN.N-CODENAME.pdf}
+  \item \texttt{<plugin>-manual-NN.N-CODENAME.pdf}\\
+        for Aorai, EVA, Metrics, RTE and WP
+  \item \texttt{e-acsl/e-acsl-X.XX.pdf}
+  \item \texttt{e-acsl/e-acsl-implementation-NN.N-CODENAME.pdf}
+  \item \texttt{e-acsl/e-acsl-manual-NN.N-CODENAME.pdf}
+  \item \texttt{aorai-example-NN.N-CODENAME.tgz}
+  \item \texttt{frama-c-NN.N-CODENAME.tar.gz}
+  \item \texttt{frama-c-api-NN.N-CODENAME.tar.gz}
+  \item \texttt{hello-NN.N-CODENAME.tar.gz}
+\end{itemize}
 
-You have to create a merge request on the website repository that will be published when Florent
-accepts it on the online branch.
+For final release \textbf{ONLY}, the following files must appear as \textbf{modified} in \texttt{download}:
 
-\textbf{Note:} the following steps are done only after the release is live on the website.
+\begin{itemize}
+  \item \texttt{acsl.pdf}
+  \item \texttt{frama-c-acsl-implementation.pdf}
+  \item \texttt{frama-c-plugin-development-guide.pdf}
+  \item \texttt{frama-c-user-manual.pdf}
+  \item \texttt{frama-c-<plugin>-manual.pdf}\\
+        for Aorai, EVA, Metrics, RTE, \textbf{Value Analysis} and WP
+  \item \texttt{e-acsl/e-acsl.pdf}
+  \item \texttt{e-acsl/e-acsl-implementation.pdf}
+  \item \texttt{e-acsl/e-acsl-manual.pdf}
+  \item \texttt{frama-c-aorai-example.tgz}
+  \item \texttt{hello.tar.gz}
+\end{itemize}
 
 \section{Announcements}
 
@@ -152,20 +96,10 @@ You'll need a GitHub account to create a pull request on the official opam repos
 \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{opam/opam} from the release
- to the opam repository clone in: \\
+  \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 Compute the MD5sum of the .tar.gz file and update the \texttt{opam} file
-with the following entry:
-\begin{verbatim}
-url {
-  src: "https://frama-c.com/download/frama-c-<version>-<version-name>.tar.gz"
-  checksum: "md5=<xxxxxx>"
-}
-\end{verbatim}
-You can provide \verb|sha256| and/or \verb|sha512| checksums as well if
-you wish.
+\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>
@@ -203,6 +137,16 @@ commit to it.
 ({\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.
+
 \section{Updating the BTS}
 
 \expertise{Usually Julien performs this step. Soon to be obsoleted.}
@@ -218,11 +162,6 @@ already done).
 Finally have a look at each still opened task in order to see what should be
 resolved in the next release.
 
-%% \section{Update the Wiki}
-
-%% Update references of the Wiki, especially pointers to manuals of this page:
-%% \url{http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications}
-
 \section{Other repositories to update}
 
 Check if other Frama-C (and related) repositories need to be updated:
@@ -240,6 +179,48 @@ 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.
 
+\section{Docker image preparation}
+
+\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be able to upload the image.
+
+Make sure:
+\begin{itemize}
+  \item \texttt{devel\_tools/docker/frama-c.dev/Dockerfile}
+  \item \texttt{devel\_tools/docker/frama-c.custom/Dockerfile}
+\end{itemize}
+are up-to-date; to do so, you can do the following:
+
+\begin{lstlisting}
+cd devel_tools/docker/frama-c.custom
+<edit Dockerfile to change the base image, from debian:sid (unstable) to the
+ latest stable release>
+<copy release .tar.gz to this directory, extract and rename the directory
+ `frama-c`>
+docker build . -t fc-with-test --build-arg=with_source=yes\
+  --build-arg=with_test=yes
+\end{lstlisting}
+
+This should copy the contents of \texttt{frama-c} into the Docker image and try
+to compile Frama-C with it, then run the tests.
+
+If the local tests do not work, check that the OCaml version and package
+dependencies are all up-to-date. Remember that there are several differences
+between Debian unstable (`sid`) and stable, which may require changes to the
+\texttt{Dockerfile}.
+
+If the local tests work, then re-run Docker \textit{without} the source/tests,
+to make the image leaner:
+
+\begin{lstlisting}
+docker build . -t framac/frama-c:<VERSION>
+\end{lstlisting}
+
+Replacing \texttt{<VERSION>} with the release number, e.g. \texttt{23.0}.
+
+After building the image, upload it with \texttt{docker push framac/frama-c:<VERSION>}.
+You will need to have setup your \texttt{framac} Docker Hub account for this to work.
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "release"