diff --git a/ALL_VERSIONS b/ALL_VERSIONS
deleted file mode 100644
index b1b8812d34378cbf5905a0aadc8c1ed3459cedfe..0000000000000000000000000000000000000000
--- a/ALL_VERSIONS
+++ /dev/null
@@ -1,66 +0,0 @@
-Version number Date of release Notes
-============== =============== =====
-29.0 (Copper) 2024, June 6
-28.1 (Nickel) 2024, March 24 Bugs fixed
-28.0 (Nickel) 2023, November 29
-27.1 (Cobalt) 2023, July 18
-27.0 (Cobalt) 2023, June 15
-26.1 (Iron) 2023, February 15
-26.0 (Iron) 2022, November 23
-25.0 (Manganese) 2022, June 22
-24.0 (Chromium) 2021, November 30
-23.1 (Vanadium) 2021, July 20
-23.0 (Vanadium) 2021, July 7
-22.0 (Titanium) 2020, November 17
-21.1 (Scandium) 2020, June 25 Bugs fixed
-21.0 (Scandium) 2020, June 11
-20.0 (Calcium) 2019, December 4
-19.1 (Potassium) 2019, September 18 OCaml 4.08 compatibility
-19.0 (Potassium) 2019, June 21
-18.0 (Argon) 2018, November 29
-Chlorine-20180502 2018, July 06 Bug fixed
-Chlorine-20180501 2018, June 01
-Sulfur-20171101 2017, November 28
-Phosphorus-20170501 2017, May 29
-
-Silicon-20161101 2016, December 2
-
-Aluminium-20160502 2016, May 31
-Aluminium-20160501 2016, May 30 Removed
-Aluminium-rc1 2016, May 13 Not publicly released
-
-Magnesium-20151002 2016, January 15
-Magnesium-20151001 2015, October 27 Not publicly released
-
-Sodium-20150201 2015, March 9
-
-Neon-20140301 2014, May 7
-
-Fluorine-20130601 2013, June 11 Bug fixed
-Fluorine-20130501 2013, May 23 Bug fixed
-Fluorine-20130401 2013, April 17
-
-Oxygen-20120901 2012, September 19
-
-Nitrogen-20111001 2011, October 10
-
-Carbon-20110201 2011, February 7
-Carbon-20101202-beta2 2010, December 17 Source only
-Carbon-20101201-beta1 2010, December 14 Source only
-
-Boron-20100401 2010, April 12
-
-Beryllium-20090902 2009, September 23
-Beryllium-20090901 2009, September 01
-Beryllium-20090601-beta1 2009, June 23 Source only
-
-Lithium-20081201 2008, Decembre 16
-Lithium-20081002+beta1 2008, October 28
-Lithium-20081001+alpha0 2008, October 03 Source only
-
-Helium-20080701 2008, July 11
-
-Hydrogen-20080502 2008, May 26 No cvs tag
-Hydrogen-20080501 2008, May 05 Source only, No cvs tag
-Hydrogen-20080302 2008, March 27 Binary only
-Hydrogen-20080301 (Hydrogen) 2008, March 03 Source only
diff --git a/dev/set-version.sh b/dev/set-version.sh
index e1c23b1f1488b08d1e5b266b07b03f0dca371746..9ac93e3b5833553cd6d48c5636bd12fa3d292581 100755
--- a/dev/set-version.sh
+++ b/dev/set-version.sh
@@ -87,6 +87,9 @@ else
echo "$NEXT" >VERSION
echo "$NEXT_CODENAME" >VERSION_CODENAME
+ # Ivette
+ $SED -i "s/^ \"version\": .*/ \"version\": \"$CURRENT_MAJOR.$CURRENT_MINOR.0\",/g" ivette/package.json
+
# Opam files
$SED -i "s/^version: .*/version: \"$NEXT\"/g" opam
$SED -i "s/\(.*\)$CURRENT_MAJOR.$CURRENT_MINOR-$CURRENT_CODENAME\(.*\)/\1$NEXT_MAJOR.$NEXT_MINOR-$NEXT_CODENAME\2/g" opam
@@ -124,6 +127,8 @@ else
doc/aorai/main.tex
$SED -i "s/\(^\\\\section\*{E-ACSL \\\\eacslpluginversion \\\\eacslplugincodename}\)/%\1\n\n\\\\section\*{E-ACSL $NEXT_MAJOR.$NEXT_MINOR $NEXT_CODENAME}/g" \
src/plugins/e-acsl/doc/userman/changes.tex
+ $SED -i "s/\(^\\\\subsection\*{Version Frama-C+dev}\)/%\1\n\n\\\\subsection\*{Version $NEXT_CODENAME-$NEXT_MAJOR}/g" \
+ src/plugins/e-acsl/doc/refman/changes_modern.tex
# Reference configuration
$SED -i "s/Frama-C [1-9][0-9]\.[0-9]/Frama-C $NEXT_MAJOR.$NEXT_MINOR/gI" \
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index 8efc99d39565177b3258f8983c1433f46590bb83..e5fe3d875915652e7fde9806a7f7dc07ed758138 100644
--- a/doc/release/branch.tex
+++ b/doc/release/branch.tex
@@ -14,12 +14,11 @@ be integrated into the upcoming release.
When the ``freeze'' period arrives (usually a few weeks before the beta
release), the release manager may decide to prevent direct merges to the
-\texttt{master} branch, until the \texttt{stable} branch is created.
-If so, then the branch should be protected such that Developers can no
-longer push and merge to it, without asking for a Master to do it.
-
-In Gitlab, this is done via: Frama-C project $\rightarrow$ Settings
-$\rightarrow$ Repository $\rightarrow$ Protected Branches.
+\texttt{master} branch, until the \texttt{stable} branch is created. If so, then
+the branch should be protected such that Developers can no longer push and merge
+to it, without asking for a Maintainer to do it. In Gitlab, this is done via:
+Frama-C project $\rightarrow$ Settings $\rightarrow$ Repository $\rightarrow$
+Protected Branches.\\
\textbf{The \texttt{master} branch must be protected \emph{at all times}.
Parameters
@@ -29,7 +28,7 @@ $\rightarrow$ Repository $\rightarrow$ Protected Branches.
\section{Creating the branch}
-Note that you must be member of the GitLab groups "frama-c", "dev" and have
+\textbf{Note:} 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
@@ -55,6 +54,9 @@ and go through Merge-requests. Everything else should go in \texttt{master},
which can then be reset to standard-level protection (Developers + Maintainers
allowed to push/merge).
+\textbf{Note:} If there are still merge requests tagged for this release, make
+sure to set their targeted branch to \texttt{stable/release}.
+
\section{GitLab issues}
{\em This is currently done periodically in specific Frama-C meetings, so only
@@ -73,8 +75,11 @@ one.
On the new \texttt{stable} branch, execute the script:
\begin{verbatim}
-./dev/set-version.sh NN.M # to be replaced with actual major/minor version
+# to be replaced with actual major/minor version
+# Add suffix ~beta for beta releases only
+./dev/set-version.sh NN.M
\end{verbatim}
+
This will:
\begin{itemize}
\item update the \texttt{Changelog}s
@@ -86,6 +91,10 @@ This will:
\item update the reference configuration
\end{itemize}
+For beta releases, update manually the doc link in opam file to add
+\texttt{-beta} (not \texttt{\textasciitilde{}beta}) :
+\texttt{http://frama-c.com/download/user-manual-<NN.M>-beta-<Codename>.pdf}\\
+
Merge the \texttt{stable} branch in the \texttt{master} branch.
On the \texttt{master} branch, execute the script:
@@ -100,6 +109,28 @@ This will:
Commit this change and push.
+\section{External plugins}
+
+List of external plugins repo names:
+\begin{itemize}
+ \item ACSL-importer
+ \item Caveat-importer
+ \item Cfp
+ \item frama-clang
+ \item GenAssigns
+ \item Meta
+ \item Minimal
+ \item Mthread
+ \item PathCrawler
+ \item Security
+ \item Volatile
+\end{itemize}
+For each one of them, check that versions in the \texttt{dune-project} files are
+coherent with \FramaC's new release. If not, update them and run \verb+make+ to
+generate the new opam file. Create a new branch, commit and push. Create a merge
+request targetting \texttt{stable/copper} on each plugin and assign your co-rm.
+This changes will need to be merged on master's branches later.
+
\section{Copyright}
Check that the date in copyright headers is correct. If not then:
@@ -108,8 +139,6 @@ Check that the date in copyright headers is correct. If not then:
\begin{itemize}
\item \texttt{headers/closed-source/*}
\item \texttt{headers/open-source/*}
- \item \texttt{ivette/headers/closed-source/*}
- \item \texttt{ivette/headers/open-source/*}
\item \texttt{src/plugins/e-acsl/headers/closed-source/*}
\item \texttt{src/plugins/e-acsl/headers/open-source/*}
\end{itemize}
diff --git a/doc/release/deploy.tex b/doc/release/deploy.tex
index 9509289dd29dd93c7004509b3d5003c2b7a2d465..e0592f1698d5e4003f9159a6fa9248c827753817 100644
--- a/doc/release/deploy.tex
+++ b/doc/release/deploy.tex
@@ -32,6 +32,13 @@ following:
on \texttt{pub} (it must be started manually and requires the branch).
\end{description}
+After running \texttt{release-branch} and \texttt{release-create}, either the
+tag indicates a beta release and then this tag is pushed on the public GitLab
+repository (\url{https://git.frama-c.com/pub/frama-c/-/tags}), or it is a final
+release and 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{Check the website}
Once the pipeline for the website has run, open \texttt{https://pub.frama-c.com}.
@@ -48,41 +55,41 @@ Once the pipeline for the website has run, open \texttt{https://pub.frama-c.com}
\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\#Codename-NN.N}
+ \item \texttt{/html/changelog.html\#<codename>-<NN.M>}
\item \texttt{/html/acsl.html}: check ACSL versions list
\item \texttt{rss.xml}: check last event
\end{itemize}
For a beta version, the installation pages for:
\begin{itemize}
-\item \texttt{/html/installations/beta\_codename.html} should indicate the beta status
-\item \texttt{/html/installations/current\_codename.html} should not indicate anything
-\item \texttt{/html/installations/previous\_codename.html} should indicate older version
+\item \texttt{/html/installations/<beta\_codename>.html} should indicate the beta status
+\item \texttt{/html/installations/<current\_codename>.html} should not indicate anything
+\item \texttt{/html/installations/<previous\_codename>.html} should indicate older version
\end{itemize}
For a final version, the installation pages for:
\begin{itemize}
-\item \texttt{/html/installations/codename.html} should not indicate anything
-\item \texttt{/html/installations/previous\_codename.html} should indicate older version
+\item \texttt{/html/installations/<codename>.html} should not indicate anything
+\item \texttt{/html/installations/<previous\_codename>.html} should indicate older version
\end{itemize}
On GitLab, in the website repository, in the merge request assigned to you, 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}
- \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}\\
+ \item \texttt{acsl-<X.YY>.pdf}
+ \item \texttt{acsl-implementation-<NN.M>-<Codename>.pdf}
+ \item \texttt{plugin-development-guide-<NN.M>-<Codename>.pdf}
+ \item \texttt{user-manual-<NN.M>-<Codename>.pdf}
+ \item \texttt{<plugin>-manual-<NN.M>-<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.tar.gz}
- \item \texttt{frama-c-NN.N-CODENAME.tar.gz}
- \item \texttt{frama-c-NN.N-CODENAME-api.tar.gz}
- \item \texttt{frama-c-server-NN.N-CODENAME-api.tar.gz}
- \item \texttt{hello-NN.N-CODENAME.tar.gz}
+ \item \texttt{e-acsl/e-acsl-<X.YY>.pdf}
+ \item \texttt{e-acsl/e-acsl-implementation-<NN.M>-<Codename>.pdf}
+ \item \texttt{e-acsl/e-acsl-manual-<NN.M>-<Codename>.pdf}
+ \item \texttt{aorai-example-<NN.M>-<Codename>.tar.gz}
+ \item \texttt{frama-c-<NN.M>-<Codename>.tar.gz}
+ \item \texttt{frama-c-<NN.M>-<Codename>-api.tar.gz}
+ \item \texttt{frama-c-server-<NN.M>-<Codename>-api.tar.gz}
+ \item \texttt{hello-<NN.M>-<Codename>.tar.gz}
\end{itemize}
For a final release \textbf{ONLY}, the following files must appear as \textbf{modified} in \texttt{download}:
@@ -101,7 +108,7 @@ For a final release \textbf{ONLY}, the following files must appear as \textbf{mo
\item \texttt{e-acsl/e-acsl-implementation.pdf}
\item \texttt{e-acsl/e-acsl-manual.pdf}
\item \texttt{frama-c-aorai-example.tar.gz}
- \item \texttt{hello.tar.gz}
+ \item \texttt{frama-c-hello.tar.gz}
\end{itemize}
If everything is fine, merge the website and ask a website maintainer to put it
@@ -114,16 +121,6 @@ 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, run the job \texttt{release - release-create}. After this, either the
-tag indicates a beta release and then this tag is pushed on the public GitLab
-repository (\url{https://git.frama-c.com/pub/frama-c/-/tags}), or it is a final
-release and 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}
@@ -155,6 +152,8 @@ Check if other \FramaC (and related) repositories need to be updated:
\section{Docker image preparation}
+This section only applies to non-beta releases.
+
\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be
able to upload the image.
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
index b09995dbf48d1b4d68c13b988a927fa8af4fe4bb..758a75b3fc38f5e091d62b3a00251daadfbba299 100644
--- a/doc/release/validation.tex
+++ b/doc/release/validation.tex
@@ -28,21 +28,21 @@ If you don't know them, ask plug-in developers to verify them.
\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:
+For final release only, remove \texttt{\textasciitilde{}beta} and
+\texttt{-beta} mentions 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{VERSION}
\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}
+ \begin{itemize}
+ \item in version field
+ \item in the doc link
+ \end{itemize}
\end{itemize}
\subsection{Versions in source: API documentation}
@@ -99,7 +99,9 @@ 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})
+
+\textbf{Note:} This requires to install the package \texttt{parallel}. Source
+for the command: \url{https://gist.github.com/amitchhajer/4461043}.
\subsection{Commit}
@@ -110,7 +112,7 @@ Commit any change that you have done during these checks \textbf{and push}.
In the last continuous integration pipeline of the release branch, force the
run of the following targets:
\begin{itemize}
- \item manuals
+ \item manuals-artifacts
\item opam-pin
\item opam-pin-minimal
\end{itemize}
@@ -121,7 +123,7 @@ They shall succeed. Collect the artifacts of the following targets:
\item manuals
\end{itemize}
-Check that these artifacts are as expected. In particular:
+\noindent Check that these artifacts are as expected. In particular:
\begin{itemize}
\item API documentatation:
\begin{itemize}
@@ -132,7 +134,9 @@ Check that these artifacts are as expected. In particular:
\item Check versions in manuals
\item Tarball
\begin{itemize}
- \item Check that no non-free components are distributed
+ \item Check that no non-free components are distributed (note: unless
+ someone inadvertently added non-free code, \FramaC does not contain any,
+ this check is obsolete).
\item Check that no \texttt{/home/user} path can be found in the distribution,
\item Build and test
\begin{itemize}
@@ -147,7 +151,7 @@ Check that these artifacts are as expected. In particular:
\end{itemize}
\end{itemize}
-Alternatively, you can use \texttt{docker} to compile the archive against a
+\noindent 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+
@@ -156,11 +160,20 @@ precise configuration:
\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: in order to be able to launch
-\verb+x11docker framac/frama-c:dev frama-c-gui+,
+For the GUI: in order to be able to launch \verb+x11docker framac/frama-c:dev frama-c-gui+,
you might want to install the
\href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script.
+\noindent \FramaC's GUI can be tested with :
+\begin{itemize}
+ \item \texttt{bin/frama-c-gui} for the old GUI.
+ \item \texttt{bin/ivette} for the new GUI.
+\end{itemize}
+\Eva can be tested with \texttt{<gui> -eva tests/idtc/*.c} and \Wp with
+\texttt{<gui> -wp -wp-rte src/plugins/wp/tests/wp\_gallery/find.i}. Try to
+navigate in the code, check some values with \Eva, check that \Wp prove some
+annotations, this should be enough.
+
\section{Validate release}
Create the main changes file in the directory \texttt{releases}. This file must
@@ -182,8 +195,12 @@ expected format is:
# ...
\end{lstlisting}
-It should only list main changes, that will be displayed on the event section
-of the website and the wiki page.
+It should only list main changes, that will be displayed on the event section of
+the website and the wiki page.
+
+\textbf{Note:} Make sure to use markdown code formating \verb+``+ if the texte
+contains things that could be affected by markdown formatting (for example
+\verb+\word1_word2+ will be displayed as \verb+word2+ without code formatting.
Create the version commit, tag it using \texttt{git tag \$(cat VERSION | sed -e "s/\textasciitilde /-/")}
and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/\textasciitilde/-/")}).