diff --git a/.gitignore b/.gitignore
index de43450eff5ee7cb09c766ebbf36124e1680d579..007ef76046f16522120663ea798724d4f4a9b4dc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,6 +34,7 @@ autom4te.cache
/config.log
/config.status
/frama-c-*.tar.gz
+/distributed
/.log.autoconf
/.Makefile.user
/ocamlgraph/
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index 1bfb095e9c7ede6d469630aa0896568f7c4e48cd..003db5f0f80ba222d5681d98f80449198de48830 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -2,6 +2,14 @@
set -u
+# Search "BEGIN SCRIPT" to skip functions
+
+# Set it to "no" in order to really execute the commands.
+# Otherwise, they are only printed.
+DEBUG=no
+
+# Set variable VERBOSE_MAKE_DOC to see all latex messages during manuals build
+
# Executing this script requires bash 4.0 or higher
# (special use of the 'case' construct)
if test `echo $BASH_VERSION | sed "s/\([0-9]\).*/\1/" ` -lt 4; then
@@ -15,9 +23,531 @@ if ! command -v git-lfs >/dev/null 2>/dev/null; then
exit 99
fi
-# Set it to "no" in order to really execute the commands.
-# Otherwise, they are only printed.
-DEBUG=no
+# rgrep needs to be installed
+if ! command -v rgrep --version >/dev/null 2>/dev/null; then
+ echo "rgrep is required"
+ exit 99
+fi
+
+function run {
+ cmd=$1
+ echo "$cmd"
+ if test "$DEBUG" == "no"; then
+ sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
+ fi
+}
+
+function step {
+ STEP=$1
+ echo
+ echo "Step $1: $2"
+}
+
+# find_repository_DIRECTORY_BRANCH path url
+# - path: path to the directory
+# - url: URL of the repository
+# Checks:
+# - master branch
+# Sets:
+# DIRECTORY: path to the directory
+function find_repository_DIRECTORY_BRANCH {
+ name=$1
+ url=$2
+ if test \! -d $name/.git ; then
+ echo "### WARNING: $name/.git directory not found; do you want to clone it? (y/n)"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ run "git clone $url $name"
+ ;;
+ *)
+ echo "The $url repository must be linked at $name (clone or symbolic link)"
+ exit 1
+ ;&
+ esac
+ fi
+ DIRECTORY=$name
+ BRANCH=`git --git-dir=$name/.git rev-parse --abbrev-ref HEAD`
+ if [ "$BRANCH" != "master" ]; then
+ echo "### WARNING: $name repository is on branch $BRANCH"
+ proceed_anyway "Reset the branch to 'master', then run the script again."
+ fi
+}
+
+# proceed_anyway message
+# - message: text to display if we have to stop
+# Ask if the user wants to continue and display the message if not (then exit)
+function proceed_anyway {
+ message=$1
+ echo "Proceed anyway? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ ;;
+ *)
+ echo "$message"
+ exit 1
+ esac
+}
+
+function look_for_uncommited_changes {
+ run "git update-index --refresh"
+ if ! git diff-index HEAD --; then
+ echo ""
+ echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
+ proceed_anyway "Stash or commit local changes, then run the script again."
+ fi
+}
+
+function look_for_frama_c_dev {
+ rgrep -i "frama-c+dev" src &> /dev/null
+ if [ "$?" == "0" ]; then
+ echo "### WARNING: Remaining frama-c+dev occurrences in 'src'"
+ proceed_anyway "Update API, then run the script again"
+ fi
+}
+
+function assert_build_dir {
+ if test \! -d "$BUILD_DIR" ; then
+ echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
+ exit 1
+ fi
+}
+
+function assert_out_dir {
+ if test \! -d "$OUT_DIR" ; then
+ echo "ERROR: $OUT_DIR does not exist, possibly removed by another step"
+ exit 1
+ fi
+}
+
+# diff_validation repository file
+# - repository: target repository
+# - file: target file
+# Ask for user validation before staging changes in [file] on the [repository].
+# Stops the script if the user refuses the changes
+function diff_validation {
+ repo=$1
+ file=$2
+ run "git -C $repo diff $file"
+ echo
+ echo "Is the above diff correct for $file? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ ;;
+ *)
+ echo "Something went wrong, you may want to clean $repo"
+ exit 1
+ esac
+ run "git -C $repo add $file"
+}
+
+# Manuals choice
+
+function get_MANUAL_NAME {
+ case "$1" in
+ "user") MANUAL_NAME="Frama-C user manual" ;;
+ "plugin-dev") MANUAL_NAME="Frama-C plug-in development guide" ;;
+ "api") MANUAL_NAME="Frama-C API bundle" ;;
+ "acsl-1") MANUAL_NAME="ACSL manual" ;;
+ "acsl-impl") MANUAL_NAME="ACSL implementation" ;;
+ "aorai") MANUAL_NAME="Aorai manual" ;;
+ "e-acsl-1") MANUAL_NAME="E-ACSL reference" ;;
+ "e-acsl-impl") MANUAL_NAME="E-ACSL implementation" ;;
+ "e-acsl-man") MANUAL_NAME="E-ACSL manual" ;;
+ "eva") MANUAL_NAME="EVA manual" ;;
+ "metrics") MANUAL_NAME="Metrics manual" ;;
+ "rte") MANUAL_NAME="RTE manual" ;;
+ "wp") MANUAL_NAME="WP manual" ;;
+ *) MANUAL_NAME="Not a manual identifier: $1" ;;
+ esac
+}
+
+function check_manual {
+ value=$1
+ if [[ ! " ${AVAILABLE_MANUALS[@]} " =~ " ${value} " ]]; then
+ echo "### ERROR: in $INCLUDED_MANUALS_CONFIG: $value is not a valid manual identifier"
+ exit 1
+ fi
+}
+
+function show_generated_manuals {
+ echo
+ echo "The following manuals will be included."
+ for i in ${INCLUDED_MANUALS[@]}; do
+ get_MANUAL_NAME $i
+ echo "- $MANUAL_NAME"
+ done
+ echo
+}
+
+function create_manuals_config {
+ echo -n > $INCLUDED_MANUALS_CONFIG
+ for i in ${AVAILABLE_MANUALS[@]}; do
+ get_MANUAL_NAME $i
+ echo "Include $MANUAL_NAME? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ echo $i >> $INCLUDED_MANUALS_CONFIG ;;
+ *) ;;
+ esac
+ done
+}
+
+function check_manual_path_MUST_ADD {
+ MUST_ADD="no"
+ for i in ${INCLUDED_MANUALS[@]}; do
+ if [[ $1 == "$i"* ]]; then
+ MUST_ADD="yes"
+ fi
+ done
+}
+
+# WIKI generation
+
+function fill_wiki {
+ PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
+ WIKI_PAGE=$WIKI_DIR/$PAGE_NAME
+ run "mkdir -p $WIKI_DIR/manuals"
+ run "sed -i -e '/<!-- LAST RELEASE -->/a \
+- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $WIKI_DIR/Home.md"
+ if test "$FINAL_RELEASE" = "yes"; then
+ release_type="FINAL"
+ else
+ release_type="BETA"
+ fi
+ run "sed -i -e '/<!-- LAST ${release_type} RELEASE -->/a \
+- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $WIKI_DIR/_sidebar.md"
+ echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
+ echo "## Sources" >> $WIKI_PAGE
+ run "cp $OUT_DIR/$TARGZ_FILENAME $WIKI_DIR/downloads"
+ run "git -C $WIKI_DIR add downloads/$TARGZ_FILENAME"
+ echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
+ echo "" >> $WIKI_PAGE
+ echo "## Manuals" >> $WIKI_PAGE
+ for fpath in $OUT_DIR/manuals/* ; do
+ f=$(basename $fpath)
+ check_manual_path_MUST_ADD $f
+ if [[ $MUST_ADD == "yes" ]]; then
+ f_no_ext=${f%.*}
+ f_no_pdf_ext="${f%.pdf}"
+ echo "- [${f_no_pdf_ext%-${FRAMAC_VERSION_AND_CODENAME}}](manuals/$f)" >> $WIKI_PAGE
+ run "cp $fpath $WIKI_DIR/manuals/"
+ run "git -C $WIKI_DIR add manuals/$f"
+ fi
+ done
+ echo "" >> $WIKI_PAGE
+ echo "## Main changes" >> $WIKI_PAGE
+ sed 's/\(\#.*\)/##\1/' $CHANGES >> $WIKI_PAGE
+ run "git -C $WIKI_DIR add $PAGE_NAME"
+ diff_validation $WIKI_DIR "Home.md"
+ diff_validation $WIKI_DIR "_sidebar.md"
+}
+
+# WEBSITE pages generation
+
+function add_install_page {
+ INSTALL_WEBPAGE=html/installations/$FRAMAC_VERSION_CODENAME_LOWER.md
+ INSTALL_WEBPAGE_PATH=$WEBSITE_DIR/$INSTALL_WEBPAGE
+ echo "---" > $INSTALL_WEBPAGE_PATH
+ echo "layout: doc_page" >> $INSTALL_WEBPAGE_PATH
+ echo "title: Installation instructions for $FRAMAC_VERSION_CODENAME" >> $INSTALL_WEBPAGE_PATH
+ echo "---" >> $INSTALL_WEBPAGE_PATH
+ echo >> $INSTALL_WEBPAGE_PATH
+ cat ./INSTALL.md >> $INSTALL_WEBPAGE_PATH
+
+ run "git -C $WEBSITE_DIR add $INSTALL_WEBPAGE"
+}
+
+function add_event_page {
+ EVENT_WEBPAGE=_events/framac-$FRAMAC_VERSION.md
+ EVENT_WEBPAGE_PATH=$WEBSITE_DIR/$EVENT_WEBPAGE
+
+ if [ "$VERSION_MINOR" != 0 ]; then
+ PREVIOUS=$VERSION_MAJOR
+ else
+ PREVIOUS=$(( $VERSION_MAJOR-1 ))
+ fi
+ PREVIOUS_NAME=$(git show $PREVIOUS.0:VERSION_CODENAME)
+
+ TEXTUAL_VERSION="Frama-C $FRAMAC_VERSION ($FRAMAC_VERSION_CODENAME)"
+ TEXTUAL_PREVIOUS="Frama-C $PREVIOUS ($PREVIOUS_NAME)"
+
+ echo "---" > $EVENT_WEBPAGE_PATH
+ echo "layout: default" >> $EVENT_WEBPAGE_PATH
+ echo "date: $(date +\"%d-%m-%Y\")" >> $EVENT_WEBPAGE_PATH
+ echo "event: $TEXTUAL_VERSION" >> $EVENT_WEBPAGE_PATH
+ echo -n "title: " >> $EVENT_WEBPAGE_PATH
+ if [ "$FINAL_RELEASE" = "no" ]; then
+ echo -n "Beta release " >> $EVENT_WEBPAGE_PATH
+ else
+ echo -n "Release " >> $EVENT_WEBPAGE_PATH
+ fi
+ echo "of $TEXTUAL_VERSION" >> $EVENT_WEBPAGE_PATH
+ VERSION_PAGE="/fc-versions/$FRAMAC_VERSION_CODENAME_LOWER.html"
+ echo "link: $VERSION_PAGE" >> $EVENT_WEBPAGE_PATH
+ echo "---" >> $EVENT_WEBPAGE_PATH
+ echo >> $EVENT_WEBPAGE_PATH
+ echo "$TEXTUAL_VERSION is out. Download it [here]($VERSION_PAGE)." >> $EVENT_WEBPAGE_PATH
+ echo >> $EVENT_WEBPAGE_PATH
+ echo "Main changes with respect to $TEXTUAL_PREVIOUS include:" >> $EVENT_WEBPAGE_PATH
+ echo >> $EVENT_WEBPAGE_PATH
+ sed 's/\(\#.*\)/###\1/' $CHANGES >> $EVENT_WEBPAGE_PATH
+
+ run "git -C $WEBSITE_DIR add $EVENT_WEBPAGE"
+}
+
+function add_version_page {
+ VERSION_WEBPAGE="_fc-versions/$FRAMAC_VERSION_CODENAME_LOWER.md"
+ VERSION_WEBPAGE_PATH=$WEBSITE_DIR/$VERSION_WEBPAGE
+ ACSL_VERSION=$(ls $OUT_DIR/manuals | sed -n 's/^acsl-1.\([0-9][0-9]\).pdf/\1/p')
+ echo "---" > $VERSION_WEBPAGE_PATH
+ echo "layout: version" >> $VERSION_WEBPAGE_PATH
+ echo "number: $VERSION_MAJOR" >> $VERSION_WEBPAGE_PATH
+ echo "name: $FRAMAC_VERSION_CODENAME" >> $VERSION_WEBPAGE_PATH
+ if [ "$FINAL_RELEASE" = "no" ]; then
+ echo "beta: true" >> $VERSION_WEBPAGE_PATH
+ else
+ echo "acsl: $ACSL_VERSION" >> $VERSION_WEBPAGE_PATH
+ fi
+ echo "releases:" >> $VERSION_WEBPAGE_PATH
+ echo " - number: $VERSION_MINOR" >> $VERSION_WEBPAGE_PATH
+ echo " categories:" >> $VERSION_WEBPAGE_PATH
+ echo " - name: Frama-C v$FRAMAC_VERSION $FRAMAC_VERSION_CODENAME" >> $VERSION_WEBPAGE_PATH
+ echo " files:" >> $VERSION_WEBPAGE_PATH
+ echo " - name: Source distribution" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/$TARGZ_FILENAME" >> $VERSION_WEBPAGE_PATH
+ echo " help: Compilation instructions" >> $VERSION_WEBPAGE_PATH
+ echo " help_link: /html/installations/$FRAMAC_VERSION_CODENAME_LOWER.html" >> $VERSION_WEBPAGE_PATH
+ check_manual_path_MUST_ADD "user"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: User manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/user-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "plugin-dev"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: Plug-in development guide" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/plugin-development-guide-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ echo " help: Hello plug-in tutorial archive" >> $VERSION_WEBPAGE_PATH
+ echo " help_link: /download/hello-$FRAMAC_VERSION_AND_CODENAME.tar.gz" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "api"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: API Documentation" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/frama-c-$FRAMAC_VERSION_AND_CODENAME-api.tar.gz" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "acsl-impl"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: ACSL 1.$ACSL_VERSION ($FRAMAC_VERSION_CODENAME implementation)" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/acsl-implementation-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ echo " - name: Plug-in Manuals" >> $VERSION_WEBPAGE_PATH
+ echo " sort: true" >> $VERSION_WEBPAGE_PATH
+ echo " files:" >> $VERSION_WEBPAGE_PATH
+ check_manual_path_MUST_ADD "aorai"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: Aoraï manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/aorai-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ echo " help: Aoraï example" >> $VERSION_WEBPAGE_PATH
+ echo " help_link: /download/aorai-example-$FRAMAC_VERSION_AND_CODENAME.tgz" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "metrics"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: Metrics manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/metrics-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "rte"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: Rte manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/rte-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "eva"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: Eva manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/eva-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "wp"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: WP manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/wp-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ check_manual_path_MUST_ADD "e-acsl-man"
+ if [[ $MUST_ADD == "yes" ]]; then
+ echo " - name: E-ACSL manual" >> $VERSION_WEBPAGE_PATH
+ echo " link: /download/e-acsl/e-acsl-manual-$FRAMAC_VERSION_AND_CODENAME.pdf" >> $VERSION_WEBPAGE_PATH
+ fi
+ echo "---" >> $VERSION_WEBPAGE_PATH
+
+ run "git -C $WEBSITE_DIR add $VERSION_WEBPAGE"
+}
+
+function add_downloads {
+ DOWNLOAD_DIR="$WEBSITE_DIR/download"
+ DOWNLOAD_PATH="download"
+ for fpath in $OUT_DIR/manuals/* ; do
+ f=$(basename $fpath)
+ f_no_ext=${f%.*}
+
+ check_manual_path_MUST_ADD $f
+ if [[ $MUST_ADD == "yes" ]]; then
+ if [[ $f_no_ext =~ ^e-acsl.*$ ]]; then
+ BASE="e-acsl/$f"
+ else
+ BASE="$f"
+ fi
+
+ if [[ $f_no_ext =~ ^(e-)?acsl-[0-9].[0-9][0-9]$ ]]; then
+ REPL=$(echo $BASE | sed -e "s/-[0-9].[0-9][0-9]//")
+ elif [[ $f_no_ext =~ ^e-acsl-* ]]; then
+ REPL=$(echo $BASE | sed -e "s/-$FRAMAC_VERSION_AND_CODENAME//")
+ else
+ REPL=$(echo $BASE | sed -e "s/\(.*\)-$FRAMAC_VERSION_AND_CODENAME/frama-c-\1/")
+ fi
+
+ run "cp $fpath $DOWNLOAD_DIR/$BASE"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$BASE"
+
+ # we change generic files ONLY for FINAL release
+ if test "$FINAL_RELEASE" = "yes"; then
+ run "cp $fpath $DOWNLOAD_DIR/$REPL"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$REPL"
+ fi
+ fi
+ done
+
+ # Particular case for the value analysis manual:
+ EVA_FILE="$OUT_DIR/manuals/eva-manual-$FRAMAC_VERSION_AND_CODENAME.pdf"
+ VALUE_PATH="$DOWNLOAD_DIR/frama-c-value-analysis.pdf"
+ VALUE_GIT_PATH="$DOWNLOAD_PATH/frama-c-value-analysis.pdf"
+ # we change generic files ONLY for FINAL release
+ if test "$FINAL_RELEASE" = "yes"; then
+ run "cp $EVA_FILE $VALUE_PATH"
+ run "git -C $WEBSITE_DIR add $VALUE_GIT_PATH"
+ fi
+
+ # Examples:
+ HELLO="hello-$FRAMAC_VERSION_AND_CODENAME.tar.gz"
+ check_manual_path_MUST_ADD "plugin-dev"
+ if [[ $MUST_ADD == "yes" ]]; then
+ run "cp $OUT_DIR/$HELLO $DOWNLOAD_DIR"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$HELLO"
+ # we change generic files ONLY for FINAL release
+ if test "$FINAL_RELEASE" = "yes"; then
+ run "cp $OUT_DIR/$HELLO $DOWNLOAD_DIR"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/hello.tar.gz"
+ fi
+ fi
+
+ # Source distribution:
+ run "cp $OUT_DIR/$TARGZ_FILENAME $DOWNLOAD_DIR"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/$TARGZ_FILENAME"
+
+ # API
+ run "cp $OUT_DIR/frama-c-api.tar.gz $DOWNLOAD_DIR/frama-c-api-$FRAMAC_VERSION_AND_CODENAME.tar.gz"
+ run "git -C $WEBSITE_DIR add $DOWNLOAD_PATH/frama-c-api-$FRAMAC_VERSION_AND_CODENAME.tar.gz"
+}
+
+function fill_website {
+ add_install_page
+ add_event_page
+ add_version_page
+ add_downloads
+}
+
+# Commit changes
+
+function create_website_branch {
+ if test "$FINAL_RELEASE" = "yes"; then
+ BRANCH_NAME="release/stable-$FRAMAC_VERSION-$FRAMAC_VERSION_CODENAME_LOWER"
+ else
+ BRANCH_NAME="release/beta-$FRAMAC_VERSION-$FRAMAC_VERSION_CODENAME_LOWER"
+ fi
+ # Chech whether release/<release> exists on the website
+ git -C $WEBSITE_DIR show-ref --verify --quiet refs/heads/$BRANCH_NAME
+ if [[ "$?" == "0" ]]; then
+ echo "### Warning: branch $BRANCH_NAME already exists in $WEBSITE_DIR"
+ echo "The script will ERASE this branch"
+ proceed_anyway "Rename or erase the branch, then run the script again."
+ run "git -C $WEBSITE_DIR branch -D $BRANCH_NAME"
+ fi
+
+ # Set release/<release> and displays changes to be committed
+ run "git -C $WEBSITE_DIR checkout --quiet -b $BRANCH_NAME"
+ run "git -C $WEBSITE_DIR status"
+
+ echo "Commit locally the previous changes on $WEBSITE_DIR:$BRANCH_NAME? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ ;;
+ *)
+ echo "Abort website branch creation, reset to master."
+ run "git -C $WEBSITE_DIR checkout master"
+ exit 1
+ esac
+ run "git -C $WEBSITE_DIR commit -m \"Prepare pages for the release of Frama-C $FRAMAC_VERSION\""
+}
+
+function commit_wiki {
+ run "git -C $WIKI_DIR status"
+
+ echo "Commit locally the previous changes on $WIKI_DIR? [y/N]"
+ read CHOICE
+ case "${CHOICE}" in
+ "Y"|"y")
+ ;;
+ *)
+ echo "Abort wiki update."
+ exit 1
+ esac
+ run "git -C $WIKI_DIR commit -m \"Prepare pages for the release of Frama-C $FRAMAC_VERSION\""
+}
+
+
+function propagate_changes {
+ create_website_branch
+ commit_wiki
+}
+
+function last_step_validation {
+ # if test "$FRAMAC_VERSION" != "$FRAMAC_TAG"; then
+ # echo "To go further, the last commit must be tagged with the right version"
+ # exit 1
+ # fi
+ echo "
+ This step will:
+
+ - ask for a validation of the changes to website
+ - create a NEW branch on for the website
+
+ - ask for a validation of the changes to wiki
+ - commit changes to the wiki MASTER branch
+
+ If you want to perform some additional checks it is probably time to stop.
+
+ Generated files are available in: $OUT_DIR.
+ "
+ echo -n "If you are ready to continue, type exactly \"RELEASE\": "
+ read CHOICE
+ case "${CHOICE}" in
+ "RELEASE")
+ ;;
+ *)
+ echo "Aborting"
+ exit 1
+ esac
+}
+
+
+# BEGIN SCRIPT
+GITLAB_FRAMA_C_PUBLIC="git@git.frama-c.com:pub"
+GITLAB_WIKI="$GITLAB_FRAMA_C_PUBLIC/frama-c.wiki.git"
+GITLAB_WEBSITE="$GITLAB_FRAMA_C_PUBLIC/pub.frama-c.com.git"
+GITLAB_ACSL="git@github.com:acsl-language/acsl.git"
+GITLAB_FRAMA_C_PRIVATE="git@git.frama-c.com:frama-c/frama-c.git"
+
if test \! -e .git ; then
echo "ERROR: .git directory not found"
echo "This script must be run at the root of a Frama-C repository"
@@ -30,9 +560,11 @@ if test \! -f VERSION ; then
echo "This script must be run at the root of a Frama-C repository"
exit 1
fi
+
FRAMAC_VERSION=$(cat VERSION)
FRAMAC_TAG=$(git describe --tag)
FRAMAC_VERSION_CODENAME=$(cat VERSION_CODENAME)
+FRAMAC_VERSION_CODENAME_LOWER=$(echo "$FRAMAC_VERSION_CODENAME" | tr '[:upper:]' '[:lower:]')
FRAMAC_VERSION_AND_CODENAME="${FRAMAC_VERSION}-${FRAMAC_VERSION_CODENAME}"
TARGZ_FILENAME=frama-c-${FRAMAC_VERSION_AND_CODENAME}.tar.gz
@@ -41,144 +573,129 @@ VERSION_MAJOR=$(cat VERSION | sed -e s/\\\([0-9]*\\\).[0-9]*.*/\\1/)
VERSION_MINOR=$(cat VERSION | sed -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
if test -n "$VERSION_MODIFIER"; then FINAL_RELEASE=no; else FINAL_RELEASE=yes; fi
+if [ "$VERSION_MODIFIER" == "+dev" ]; then
+ echo "### WARNING: The VERSION is a development version"
+ proceed_anyway "Update VERSION and run the script again"
+fi
if test "$FRAMAC_VERSION" != "$FRAMAC_TAG"; then
- echo "WARNING: The current commit is not tagged with the current version:"
+ echo "### WARNING: The current commit is not tagged with the current version:"
echo "Frama-C Version: $FRAMAC_VERSION"
echo "Frama-C Tag : $FRAMAC_TAG"
fi
-run () {
- cmd=$1
- echo "$cmd"
- if test "$DEBUG" == "no"; then
- sh -c "$cmd" || { echo "Aborting step ${STEP}."; exit "${STEP}"; }
- fi
-}
+# Find specific repositories
-# GITLAB_DIR=./pub-frama-c
-# GITLAB_GIT="git@git.frama-c.com:pub/frama-c.git"
-
-# if test ! -d $GITLAB_DIR/.git; then
-# echo "WARNING: $GITLAB_DIR/.git directory not found; do you want to clone it? (y/n)"
-# read CHOICE
-# case "${CHOICE}" in
-# "Y"|"y")
-# run "git clone $GITLAB_GIT $GITLAB_DIR"
-# ;;
-# *)
-# echo "gitlab's public Frama-C project must be linked at $GITLAB_DIR \
- # (clone or symbolic link)"
-# exit 1
-# ;&
-# esac
-# fi
-# GITLAB_BRANCH=$(git --git-dir=$GITLAB_DIR/.git rev-parse --abbrev-ref HEAD)
-# if test "$FRAMAC_BRANCH" != "$GITLAB_BRANCH"; then
-# echo "WARNING: switching pub-frama-c to current branch $FRAMAC_BRANCH"
-# run "git -C $GITLAB_DIR checkout -b $FRAMAC_BRANCH"
-# fi
-
-GITLAB_WIKI_GIT="git@git.frama-c.com:pub/frama-c.wiki"
-GITLAB_WIKI=./frama-c.wiki
-if test ! -d $GITLAB_WIKI/.git; then
- echo "WARNING: $GITLAB_WIKI/.git directory not found; do you want to clone it? (y/n)"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- run "git clone $GITLAB_WIKI_GIT"
- ;;
- *)
- echo "pub/frama-c wiki must be linked at $GITLAB_WIKI \
- (clone or symbolic link)"
- exit 1
- ;&
- esac
-fi
-GITLAB_WIKI_BRANCH=$(git --git-dir=$GITLAB_WIKI/.git rev-parse --abbrev-ref HEAD)
+find_repository_DIRECTORY_BRANCH "./frama-c.wiki" $GITLAB_WIKI
+WIKI_DIR=$DIRECTORY
+WIKI_BRANCH=$BRANCH
-if test "$GITLAB_WIKI_BRANCH" != "master"; then
- echo "WARNING: pub/frama-c's wiki is not on the master branch";
-fi
+find_repository_DIRECTORY_BRANCH "./website" $GITLAB_WEBSITE
+WEBSITE_DIR=$DIRECTORY
+WEBSITE_BRANCH=$BRANCH
-ACSL_GIT="git@gitlab.com:acsl-language/acsl.git"
-ACSL_DIR="./doc/acsl"
-if test \! -d $ACSL_DIR/.git ; then
- echo "WARNING: $ACSL_DIR/.git directory not found; do you want to clone it? (y/n)"
+find_repository_DIRECTORY_BRANCH "./doc/acsl" $GITLAB_ACSL
+ACSL_DIR=$DIRECTORY
+
+CHANGES="./main_changes.md"
+if test \! -f $CHANGES ; then
+ echo "### WARNING: The $CHANGES file is missing"
+ echo "Do you want to create an empty one? [y/N]"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
- pushd "./doc"
- run "git clone $ACSL_GIT"
- popd
- ;;
+ touch $CHANGES;;
*)
- echo "The Github ACSL repository must be linked at $ACSL_DIR (clone or symbolic link)"
+ echo "Create a changes file and run the script again"
exit 1
- ;&
esac
fi
+AVAILABLE_MANUALS=("user" "api" "plugin-dev" "acsl-1" "acsl-impl" "aorai" "e-acsl-1" "e-acsl-man" "e-acsl-impl" "eva" "metrics" "rte" "wp")
+INCLUDED_MANUALS_CONFIG="./included_manuals"
+INCLUDED_MANUALS=()
-
-MANUALS_DIR="./doc/manuals"
-
-# push on frama-c.com only for final releases
-WEBSITE_GIT="git@git.frama-c.com:pub/pub.frama-c.com.git"
if test "$FINAL_RELEASE" = "yes"; then
- WEBSITE_DIR="./website"
- if test \! -d $WEBSITE_DIR/.git ; then
- echo "ERROR: $WEBSITE_DIR/.git directory not found; do you want to clone it? (y/n)"
+ # In final release mode, all manuals must be distributed
+ for i in ${AVAILABLE_MANUALS[@]}; do
+ INCLUDED_MANUALS+=($i)
+ done
+else
+ if test \! -f $INCLUDED_MANUALS_CONFIG ; then
+ echo "### WARNING: The $INCLUDED_MANUALS_CONFIG file is missing"
+ echo "Do you want to create one? [y/N]"
read CHOICE
case "${CHOICE}" in
"Y"|"y")
- run "git clone $WEBSITE_GIT website"
+ create_manuals_config
+ for i in $(cat $INCLUDED_MANUALS_CONFIG); do
+ check_manual $i
+ INCLUDED_MANUALS+=($i)
+ done
;;
*)
- echo "The Github Website repository must be linked at $WEBSITE_DIR (clone or symbolic link)"
- exit 1
- ;&
+ echo "NO manuals will be included"
+ ;;
esac
+ else
+ for i in $(cat $INCLUDED_MANUALS_CONFIG); do
+ check_manual $i
+ INCLUDED_MANUALS+=($i)
+ done
fi
- WEBSITE_BRANCH=`git --git-dir=$WEBSITE_DIR/.git rev-parse --abbrev-ref HEAD`
-fi # FINAL_RELEASE == yes
+fi
+
+MANUALS_DIR="./doc/manuals"
+
+FILTER=""
+if [ -z ${VERBOSE_MAKE_DOC+x} ]; then
+ if command -v texfot --version >/dev/null 2>/dev/null; then
+ FILTER="texfot --ignore '(Warning|Overfull|Underfull|Version)'"
+ fi
+fi
BUILD_DIR_ROOT="/tmp/release"
BUILD_DIR="$BUILD_DIR_ROOT/frama-c"
-echo "Frama-C Version : $FRAMAC_VERSION"
-echo "Frama-C Branch : $FRAMAC_BRANCH"
-echo "Final release : $FINAL_RELEASE"
-# echo "pub/frama-c dir : $GITLAB_DIR"
-# echo "pub/frama-c branch : $GITLAB_BRANCH"
-echo "pub/frama-c wiki : $GITLAB_WIKI"
-echo "Manuals Dir : $MANUALS_DIR"
-if test "$FINAL_RELEASE" = "yes"; then
- echo "Website Dir : $WEBSITE_DIR"
- echo "Website Branch : $WEBSITE_BRANCH"
-else
- echo "Intermediate release: website not updated"
-fi
-echo "Build Dir : $BUILD_DIR"
+OUT_DIR="./distributed"
-DOWNLOAD_DIR="download"
+echo "############################# Frama-C Info ##############################"
+echo ""
+echo "Frama-C Version : $FRAMAC_VERSION"
+echo "Final release : $FINAL_RELEASE"
+echo "Frama-C Branch : $FRAMAC_BRANCH"
+echo "Frama-C Wiki Dir : $WIKI_DIR"
+echo "Website Dir : $WEBSITE_DIR"
+echo "Changes file : $CHANGES"
+echo "Build Dir : $BUILD_DIR"
+echo "Output Dir : $OUT_DIR"
+echo ""
+echo "############################# Manuals ##############################"
+echo ""
+echo "Manuals Dir : $MANUALS_DIR"
+echo "ACSL Dir : $ACSL_DIR"
+show_generated_manuals
-step () {
- STEP=$1
- echo
- echo "Step $1: $2"
-}
+echo "#########################################################################"
export LC_CTYPE=en_US.UTF-8
-echo -n "Steps are:
+echo -n "
+Steps are:
+
N) previous information is wrong, STOP the script
- 0) compile PDF manuals (will ERASE $MANUALS_DIR!)
- 1) reset local copy of target repositories
+ 0) ERASE $OUT_DIR
+ 1) compile PDF manuals (will ERASE $MANUALS_DIR!)
2) build the source distribution
3) build API bundle
4) build documentation companions
- 5) copy and stage locally the distributed manuals
+ 5) clean $BUILD_DIR
+ 6) prepare wiki (will RESET HARD $WIKI_DIR:$WIKI_BRANCH)
+ 7) prepare website (will RESET HARD $WEBSITE_DIR:$WEBSITE_BRANCH)
+ 8) check generated distribution
+ 9) generate opam file
+ 10) commit changes
+
Start at which step? (default is N, which cancels everything)
- If this is the first time running this script, start at 0
- Otherwise, start at the latest step before failure
@@ -191,36 +708,24 @@ case "${STEP}" in
exit 0;
;&
0)
- step 0 "COMPILING PDF MANUALS"
- run "rm -rf $MANUALS_DIR"
- run "mkdir -p $MANUALS_DIR"
- run "doc/build-manuals.sh"
+ step 0 "PREPARE DISTRIBUTION DIRECTORY"
+ run "rm -rf $OUT_DIR"
+ run "mkdir -p $OUT_DIR"
;&
+
1)
- # run "git -C $GITLAB_DIR reset --hard"
- run "git -C $GITLAB_WIKI reset --hard"
- if test "$FINAL_RELEASE" = "yes"; then
- run "git -C $WEBSITE_DIR reset --hard"
- fi
+ step 1 "COMPILING PDF MANUALS"
+ run "rm -rf $MANUALS_DIR"
+ run "mkdir -p $MANUALS_DIR"
+ run "$FILTER doc/build-manuals.sh"
+ run "rm -rf $OUT_DIR/manuals"
+ run "mkdir -p $OUT_DIR/manuals"
+ run "cp $MANUALS_DIR/* $OUT_DIR/manuals"
;&
2)
step 2 "BUILDING THE SOURCE DISTRIBUTION"
- # WARNING! MUST RUN git update-index BEFORE git diff-index!
- # See: https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status
- run "git update-index --refresh"
- if ! git diff-index HEAD --; then
- echo ""
- echo "### WARNING: uncommitted git changes will be discarded when creating archive!"
- echo "Proceed anyway? [y/N]"
- read CHOICE
- case "${CHOICE}" in
- "Y"|"y")
- ;;
- *)
- echo "Stash or commit local changes, then run the script again."
- exit 1
- esac
- fi
+ look_for_uncommited_changes
+ look_for_frama_c_dev
run "mkdir -p $BUILD_DIR_ROOT"
run "rm -rf $BUILD_DIR"
run "git worktree add -f --detach $BUILD_DIR $FRAMAC_BRANCH"
@@ -229,112 +734,63 @@ case "${STEP}" in
run "cd $BUILD_DIR; make -j OPEN_SOURCE=yes src-distrib"
# sanity check: markdown-report must be distributed
run "tar tf $BUILD_DIR/$TARGZ_FILENAME | grep -q src/plugins/markdown-report"
- # populate release assets in wiki
- run "mkdir -p $GITLAB_WIKI/downloads"
- run "cp $BUILD_DIR/$TARGZ_FILENAME $GITLAB_WIKI/downloads/"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/$TARGZ_FILENAME"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE"
- run "cp $BUILD_DIR/$TARGZ_FILENAME $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- fi
+ run "cp $BUILD_DIR/$TARGZ_FILENAME $OUT_DIR"
;&
3)
- #note: this step may fail if step 4 was performed,
- # because it will erase BUILD_DIR
step 3 "BUILDING THE API BUNDLE"
- if test \! -d "$BUILD_DIR" ; then
- echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
- exit 1
- fi
+ assert_build_dir
run "cd $BUILD_DIR; make -j doc-distrib"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/frama-c-${FRAMAC_VERSION_AND_CODENAME}-api.tar.gz"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE"
- run "cp $BUILD_DIR/frama-c-api.tar.gz $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- fi
+ run "cp $BUILD_DIR/frama-c-api.tar.gz $OUT_DIR"
;&
4)
step 4 "BUILDING THE DOCUMENTATION COMPANIONS"
- if test \! -d "$BUILD_DIR" ; then
- echo "ERROR: $BUILD_DIR does not exist, possibly removed by another step"
- exit 1
- fi
+ assert_build_dir
run "cd $BUILD_DIR; make -j doc-companions"
- if test "$FINAL_RELEASE" = "yes"; then
- SPEC_FILE="$DOWNLOAD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz"
- RELE_FILE="$DOWNLOAD_DIR/hello.tar.gz"
- run "rm -f $WEBSITE_DIR/$SPEC_FILE $WEBSITE_DIR/$RELE_FILE"
- run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$SPEC_FILE"
- run "git -C $WEBSITE_DIR add $SPEC_FILE"
- run "ln -s hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $WEBSITE_DIR/$RELE_FILE";
- run "git -C $WEBSITE_DIR add $RELE_FILE"
- run "rm -rf $BUILD_DIR"
- run "git worktree prune"
- fi
+ run "cp $BUILD_DIR/hello-${FRAMAC_VERSION_AND_CODENAME}.tar.gz $OUT_DIR"
;&
5)
- step 5 "COPYING AND STAGING THE DISTRIBUTED MANUALS"
- PAGE_NAME=Frama-C-${FRAMAC_VERSION_AND_CODENAME}.md
- WIKI_PAGE=$GITLAB_WIKI/$PAGE_NAME
- run "mkdir -p $GITLAB_WIKI/manuals"
- run "sed -i -e '/<!-- LAST RELEASE -->/a \
-- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/Home.md"
- if test "$FINAL_RELEASE" = "yes"; then
- release_type="FINAL"
- else
- release_type="BETA"
- fi
- run "sed -i -e '/<!-- LAST ${release_type} RELEASE -->/a \
-- [${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})](Frama-C-${FRAMAC_VERSION_AND_CODENAME})' $GITLAB_WIKI/_sidebar.md"
- echo "# Frama-C release ${FRAMAC_VERSION} (${FRAMAC_VERSION_CODENAME})" > $WIKI_PAGE
- echo "## Sources" >> $WIKI_PAGE
- echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
- echo "" >> $WIKI_PAGE
- echo "## Manuals" >> $WIKI_PAGE
- for fpath in $MANUALS_DIR/*; do
- f=$(basename $fpath)
- f_no_ext=${f%.*}
- # E-ACSL-related files are stored in subdirectory e-acsl
- if [[ $f_no_ext =~ ^e-acsl.*$ ]]; then
- destdir="$WEBSITE_DIR/$DOWNLOAD_DIR/e-acsl"
- else
- destdir="$WEBSITE_DIR/$DOWNLOAD_DIR"
- fi
- if [[ -L $fpath ]]; then
- # symbolic links are copied to the website and prepended with 'frama-c-'
- # (except for acsl.pdf, which is copied as is)
- if [[ $f_no_ext =~ ^(e-)?acsl$ ]]; then
- ln="$f"
- else
- ln="frama-c-$f"
- fi
- run "rm -f $destdir/$ln"
- run "cp -P $fpath $destdir/$ln"
- run "git -C $destdir add $ln"
- else
- # non-symbolic links are copied as-is to the website, and also to
- # the Gitlab wiki, where they are also added as links
- f_no_pdf_ext="${f%.pdf}"
- echo "- [${f_no_pdf_ext%-${FRAMAC_VERSION_AND_CODENAME}}](manuals/$f)" >> $WIKI_PAGE
- run "cp $fpath $GITLAB_WIKI/manuals/"
- run "git -C $GITLAB_WIKI add manuals/$f"
- run "cp $fpath $destdir/$f"
- run "git -C $destdir add $f"
- fi
- done
-
- INSTALL_WEBPAGE=html/installations/$(echo "$FRAMAC_VERSION_CODENAME" | tr '[:upper:]' '[:lower:]').md
- INSTALL_WEBPAGE_PATH=$WEBSITE_DIR/$INSTALL_WEBPAGE
- echo "----" > $INSTALL_WEBPAGE_PATH
- echo "layout: doc_page" >> $INSTALL_WEBPAGE_PATH
- echo "title: Installation instructions for $FRAMAC_VERSION_CODENAME" >> $INSTALL_WEBPAGE_PATH
- echo "----" >> $INSTALL_WEBPAGE_PATH
- cat ./INSTALL.md >> $INSTALL_WEBPAGE_PATH
- run "git -C $WEBSITE_DIR add $INSTALL_WEBPAGE"
-
- run "git -C $GITLAB_WIKI add $PAGE_NAME"
+ step 5 "CLEAN $BUILD_DIR"
+ run "rm -rf $BUILD_DIR"
+ run "git worktree prune"
+ ;&
+ 6)
+ step 6 "PREPARE WIKI"
+ assert_out_dir
+ run "git -C $WIKI_DIR reset --hard"
+ fill_wiki
+ ;&
+ 7)
+ step 7 "PREPARE WEBSITE"
+ assert_out_dir
+ run "git -C $WEBSITE_DIR reset --hard"
+ fill_website
+ ;&
+ 8)
+ step 8 "CHECK GENERATED DISTRIBUTION"
+ assert_out_dir
+ TEST_DIR="$BUILD_DIR_ROOT/frama-c-$FRAMAC_VERSION-$FRAMAC_VERSION_CODENAME"
+ run "mkdir -p $BUILD_DIR_ROOT"
+ run "rm -rf $TEST_DIR"
+ run "cp $OUT_DIR/$TARGZ_FILENAME $BUILD_DIR_ROOT"
+ run "cd $BUILD_DIR_ROOT ; tar xzf $TARGZ_FILENAME"
+ run "./doc/release/checktar.sh $TEST_DIR"
+ run "cd $TEST_DIR ; ./configure && make -j && make tests PTESTS_OPTS=\"-error-code\""
+ run "rm -rf $TEST_DIR"
+ ;&
+ 9)
+ step 9 "GENERATE OPAM FILE"
+ assert_out_dir
+ run "cp opam/opam $OUT_DIR/opam"
+ echo >> "$OUT_DIR/opam"
+ echo "url {" >> "$OUT_DIR/opam"
+ echo " src: \"https://git.frama-c.com/pub/frama-c/-/wikis/downloads/$TARGZ_FILENAME\"" >> "$OUT_DIR/opam"
+ echo " checksum: \"md5=$(md5sum $OUT_DIR/$TARGZ_FILENAME | cut -d" " -f1)\"" >> "$OUT_DIR/opam"
+ echo "}" >> "$OUT_DIR/opam"
+ ;&
+ 10)
+ step 10 "COMMIT CHANGES"
+ last_step_validation
+ propagate_changes
;;
*)
echo "Bad entry: ${STEP}"
diff --git a/doc/build-manuals.sh b/doc/build-manuals.sh
index 725ae1c670b36d9f33b091d199cb851cfd55c332..353f2a43d2922800c2c49054163491b92f712242 100755
--- a/doc/build-manuals.sh
+++ b/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
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index 5ee6c9b56ce577b22486f3ea5b426fbb0366e0c0..ca2cb8d1c8e44672d4243488ab1b6d6a2cb23e8c 100644
--- a/doc/release/branch.tex
+++ b/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?}
diff --git a/doc/release/build.tex b/doc/release/build.tex
index 7d2cfc524726c384cdf7279618022a4ed25b2298..e3c9386b25c4516fd10187fffbc1b047d526c18a 100644
--- a/doc/release/build.tex
+++ b/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"+
diff --git a/doc/release/checktar.sh b/doc/release/checktar.sh
index db08047a27a1cea62a982859f3260d682f296463..66a852c693bcc02af7e3a92ea51fd9bbdef5c5e1 100755
--- a/doc/release/checktar.sh
+++ b/doc/release/checktar.sh
@@ -1,15 +1,43 @@
-#!/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
diff --git a/doc/release/website.tex b/doc/release/website.tex
index b10cda813a798083bb2264a7e72001f29493b445..6e6b79dc3aec6550a8aebbb00c3a994bc2333011 100644
--- a/doc/release/website.tex
+++ b/doc/release/website.tex
@@ -1,4 +1,4 @@
-\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"