diff --git a/.gitignore b/.gitignore
index f0eff975f0ed1f0788644d01adb9cc7da866566f..7b6e963424996402da1ae8c6ba24d04f5d3c5633 100644
--- a/.gitignore
+++ b/.gitignore
@@ -86,9 +86,9 @@ _build
/doc/acsl/
-/doc/aorai/aorai-example.tgz
+/doc/aorai/aorai-example.tar.gz
/doc/aorai/aorai-example/
-/doc/aorai/frama-c-aorai-example.tgz
+/doc/aorai/frama-c-aorai-example.tar.gz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
/doc/aorai/ya_file.tex
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b7ee6c797ec4ed7311b188adac5b92e68fbd120c..3ff7baef0bfc584690eecd152b3c1fe5212c9b5e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -7,6 +7,7 @@ stages:
- tests
- distrib
- compatibility
+ - release
- publish
################################################################################
@@ -23,6 +24,7 @@ variables:
DEFAULT: "master"
OCAML: "4.11"
PUBLISH: "no"
+ RELEASE: "no"
################################################################################
### PREPARE
@@ -52,6 +54,28 @@ do-not-stop-pipeline:
variables:
- $DEFAULT == $CI_COMMIT_BRANCH
+check-publish:
+ stage: prepare
+ script: >
+ [[ "$RELEASE" == "no" ]] &&
+ [[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
+ [[ "$DEFAULT" == "master" ]]
+ only:
+ variables:
+ - $PUBLISH == "yes"
+
+check-release:
+ stage: prepare
+ script: >
+ [[ "$PUBLISH" == "no" ]] &&
+ [[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
+ [[ "$DEFAULT" == "stable/$(cat VERSION_CODENAME | tr '[:upper:]' '[:lower:]')" ]] &&
+ [[ "$(git describe --tag)" == "$(cat VERSION | sed 's/~/-/')" ]]
+ [[ "$(cat VERSION)" == "$(cat opam/opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')" ]]
+ only:
+ variables:
+ - $RELEASE == "yes"
+
################################################################################
### BUILD
@@ -156,33 +180,16 @@ external-plugins:
# API documentation
-.build_template: &api_doc_template
+api-doc: # Note: the Nix store avoids rebuilding
stage: distrib
variables:
OUT: "api"
script:
- ./nix/build-proxy.sh api-doc
-
-api-doc-default: # Check that we successfully build but no artifact
- <<: *api_doc_template
-
-api-doc-artifact: # Note: the Nix store avoids rebuilding
- <<: *api_doc_template
artifacts:
paths:
- api/frama-c-api.tar.gz
expire_in: 7 days
- when: manual
-
-api-doc-scheduled: # Keep artifact for published branch each night
- <<: *api_doc_template
- artifacts:
- paths:
- - api/frama-c-api.tar.gz
- expire_in: 7 days # Note: the LAST artifact of the ref is always kept
- only:
- variables:
- - $PUBLISH == "yes"
# Build distribution tarball
@@ -225,15 +232,43 @@ lint:
OUT: "manuals"
script:
- ./nix/build-proxy.sh manuals
+ artifacts:
+ paths:
+ - manuals/*.pdf
+ - manuals/*.tar.gz
+ - manuals/*.txt
+ expire_in: 7 days # Note: the LAST artifact of the ref is always kept
manuals:
<<: *manuals_template
+ except:
+ variables:
+ - $RELEASE == "yes"
when: manual
+
+manuals-for-release:
+ <<: *manuals_template
+ only:
+ variables:
+ - $RELEASE == "yes"
+
+release-content:
+ stage: distrib
+ script:
+ - ./nix/shell-checkers.sh "./dev/build-release.sh"
+ needs:
+ - api-doc
+ - build-distrib-tarball
+ - manuals-for-release
artifacts:
paths:
- - manuals/*.pdf
- - manuals/*.tgz
- expire_in: 7 days # Note: the LAST artifact of the ref is always kept
+ - website
+ - wiki
+ - opam-repository
+ - release-data.json
+ only:
+ variables:
+ - $RELEASE == "yes"
################################################################################
### COMPATIBILITY
@@ -283,7 +318,7 @@ ocaml-versions-nightly:
# Opam pin
-.build_template: &opam_template
+.build_template: &opam_pin_template
stage: compatibility
image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
script:
@@ -295,15 +330,21 @@ ocaml-versions-nightly:
- docker
opam-pin:
- <<: *opam_template
- when: manual
+ <<: *opam_pin_template
except:
- - schedules
+ refs:
+ - schedules
+ variables:
+ - $RELEASE == "yes"
+ when: manual
-opam-pin-nightly:
- <<: *opam_template
+opam-pin-automatic:
+ <<: *opam_pin_template
only:
- - schedules
+ refs:
+ - schedules
+ variables:
+ - $RELEASE == "yes"
# TODO: Enable this rule later:
#
@@ -337,14 +378,84 @@ opam-pin-nightly:
src-distrib-tests:
<<: *src_distrib_tests_template
except:
- - schedules
+ refs:
+ - schedules
+ variables:
+ - $RELEASE == "yes"
-src-distrib-tests-nightly:
+src-distrib-tests-long:
<<: *src_distrib_tests_template
# The Opam target may affect this job
timeout: 2h
only:
- - schedules
+ refs:
+ - schedules
+ variables:
+ - $RELEASE == "yes"
+
+################################################################################
+### RELEASE
+
+.build_template: &prepare_ssh_template
+ before_script:
+ - export GIT_SSH=$PWD/nix/frama-c-public/ssh.sh
+ - echo "$FRAMA_CI_BOT_SSH_PRIVATE" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
+ - nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
+
+release-branch:
+ stage: release
+ <<: *prepare_ssh_template
+ script:
+ - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/$CI_COMMIT_BRANCH)
+ - nix run -f channel:nixos-19.03 openssh --command git push git@git.frama-c.com:pub/frama-c.git origin/$CI_COMMIT_BRANCH:refs/heads/$CI_COMMIT_BRANCH
+ only:
+ variables:
+ - $RELEASE == "yes"
+ when: manual
+ interruptible: false
+
+release-create:
+ stage: release
+ script:
+ - nix-shell -p curl --run './nix/frama-c-public/publish-release.sh'
+ needs:
+ - release-branch
+ - release-content
+ only:
+ variables:
+ - $RELEASE == "yes"
+ when: manual
+ interruptible: false
+
+release-opam:
+ stage: release
+ <<: *prepare_ssh_template
+ script:
+ - nix-shell -p openssh --run './nix/frama-c-public/publish-opam.sh'
+ only:
+ variables:
+ - $RELEASE == "yes"
+ interruptible: false
+
+release-website:
+ stage: release
+ <<: *prepare_ssh_template
+ script:
+ - nix-shell -p openssh --run './nix/frama-c-public/publish-website.sh'
+ only:
+ variables:
+ - $RELEASE == "yes"
+ interruptible: false
+
+release-wiki:
+ stage: release
+ <<: *prepare_ssh_template
+ script:
+ - nix-shell -p openssh --run './nix/frama-c-public/publish-wiki.sh'
+ only:
+ variables:
+ - $RELEASE == "yes"
+ interruptible: false
################################################################################
### PUBLISH
@@ -365,35 +476,32 @@ src-distrib-tests-nightly:
publish-frama-c:
stage: publish
+ <<: *prepare_ssh_template
script:
- (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/master)
- - echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- - nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- - GIT_SSH=nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git push git@git.frama-c.com:pub/frama-c.git origin/master:refs/heads/master
+ - nix run -f channel:nixos-19.03 openssh --command git push git@git.frama-c.com:pub/frama-c.git origin/master:refs/heads/master
only:
variables:
- $PUBLISH == "yes"
interruptible: false
-publish-meta:
+publish-fclang:
stage: publish
+ <<: *prepare_ssh_template
script:
- - echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- - nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- - GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/meta.git nix/frama-c-public/meta
- - GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/meta push git@git.frama-c.com:pub/meta origin/master:refs/heads/master
+ - nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/frama-clang.git nix/frama-c-public/frama-clang
+ - nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/frama-clang push git@git.frama-c.com:pub/frama-clang origin/master:refs/heads/master
only:
variables:
- $PUBLISH == "yes"
interruptible: false
-publish-fclang:
+publish-meta:
stage: publish
+ <<: *prepare_ssh_template
script:
- - echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- - nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- - GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/frama-clang.git nix/frama-c-public/frama-clang
- - GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/frama-clang push git@git.frama-c.com:pub/frama-clang origin/master:refs/heads/master
+ - nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/meta.git nix/frama-c-public/meta
+ - nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/meta push git@git.frama-c.com:pub/meta origin/master:refs/heads/master
only:
variables:
- $PUBLISH == "yes"
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index bb1682475f5153d6f94ce3bc27e397080fe732ce..fbc41f1c1abada51e201b289c1bcfd270f89f036 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -377,7 +377,7 @@ function add_version_page {
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
+ echo " help_link: /download/aorai-example-$FRAMAC_VERSION_AND_CODENAME.tar.gz" >> $VERSION_WEBPAGE_PATH
fi
check_manual_path_MUST_ADD "metrics"
if [[ $MUST_ADD == "yes" ]]; then
diff --git a/dev/build-release.sh b/dev/build-release.sh
new file mode 100755
index 0000000000000000000000000000000000000000..22a708b2a41736c6726fa09df3658890a720e90b
--- /dev/null
+++ b/dev/build-release.sh
@@ -0,0 +1,471 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Note:
+#
+# While this script can be run locally, it is meant to run in the Frama-C CI.
+# Thus, it expects to be run from the root of the Frama-C directory and that
+# some CI artifacts are available. Namely:
+# - 'frama-c.tar.gz'
+# - 'api' directory (with api archive inside)
+# - 'manuals' directory (with all manuals incl. acsl + version text files)
+# Availability of the files is checked when the script starts. The script also
+# checks that:
+# - the version is stable (VERSION file does not contain '+dev')
+# - the commit is tagged with the version (if it contains ~, replaced by -)
+# - releases/<VERSION_MAJOR>.<VERSION_MINOR>.md exists
+# The script generates the following directories:
+# - wiki (for the public Frama-C instance)
+# - website
+# - opam-repository
+# - release-data.json
+# with the correct tree for generated files.
+
+##########################################################################
+# Check binaries
+
+function echo_red {
+ echo -e "\e[31m$1\e[0m"
+}
+function echo_green {
+ echo -e "\e[32m$1\e[0m"
+}
+
+function show_step {
+ echo ""
+ echo "### $1"
+ echo ""
+}
+
+show_step "Checking binaries availability"
+
+if ! command -v git-lfs >/dev/null 2>/dev/null; then
+ echo_red "git-lfs is required"
+ exit 127
+fi
+
+# grep needs to be installed
+if ! command -v grep --version >/dev/null 2>/dev/null; then
+ echo_red "grep is required"
+ exit 127
+fi
+
+MANUALS_DIR="./manuals"
+API_DIR="./api"
+
+FRAMAC_COM_DOWNLOAD="https://www.frama-c.com/download"
+
+##########################################################################
+# Check stable or beta and build names
+
+show_step "Checking version"
+
+VERSION="$(cat VERSION)"
+VERSION_SAFE="${VERSION/~/-}"
+VERSION_MODIFIER=$(sed VERSION -e s/[0-9.]*\\\(.*\\\)/\\1/)
+VERSION_MAJOR=$(sed VERSION -e s/\\\([0-9]*\\\).[0-9]*.*/\\1/)
+VERSION_MINOR=$(sed VERSION -e s/[0-9]*.\\\([0-9]*\\\).*/\\1/)
+TAG="$(git describe --tag)"
+CODENAME="$(cat VERSION_CODENAME)"
+LOWER_CODENAME="$(echo "$CODENAME" | tr '[:upper:]' '[:lower:]')"
+VERSION_AND_CODENAME="${VERSION_SAFE}-${CODENAME}"
+
+if [ "$VERSION_MINOR" != 0 ]; then
+ PREVIOUS="$VERSION_MAJOR.$((VERSION_MINOR - 1))"
+else
+ PREVIOUS="$((VERSION_MAJOR - 1)).0"
+fi
+PREVIOUS_NAME=$(git show $PREVIOUS:VERSION_CODENAME)
+
+if [ "$VERSION_MODIFIER" == "+dev" ]; then
+ echo "Development version ($VERSION)"
+ echo_red "Aborting"
+ exit 2
+fi
+
+if [ "$VERSION_SAFE" != "$TAG" ]; then
+ echo "The current commit is not tagged with the current version:"
+ echo "Frama-C Version: $VERSION"
+ echo "Frama-C Tag : $TAG"
+ echo_red "Aborting"
+ exit 2
+fi
+
+if test -n "$VERSION_MODIFIER"; then
+ FINAL=no
+else
+ FINAL=yes
+fi
+
+echo "Ready to build release: Frama-C $VERSION - $CODENAME"
+echo "MAJOR: $VERSION_MAJOR"
+echo "MINOR: $VERSION_MINOR"
+echo "FINAL: $FINAL"
+
+##########################################################################
+# Check input files
+
+function prepare_file {
+ echo -n "Searching for '$1' ... "
+ if [ ! -f "$1" ]; then
+ echo_red "FAILED (aborting)"
+ exit 2
+ fi
+ echo_green "OK"
+ chmod 644 "$1"
+}
+
+show_step "Searching for a Frama-C source archive"
+
+TARGZ_BASE="frama-c.tar.gz"
+TARGZ_GENERIC="frama-c-source-dist.tar.gz"
+TARGZ_VERSION="frama-c-$VERSION_SAFE-$CODENAME.tar.gz"
+prepare_file $TARGZ_BASE
+
+show_step "Searching for a Frama-C API archive"
+
+TARGZ_API="$API_DIR/frama-c-api.tar.gz"
+
+prepare_file $TARGZ_API
+
+show_step "Searching for manuals"
+
+MANUALS=(
+ "acsl"
+ "acsl-implementation"
+ "aorai-manual"
+ "e-acsl"
+ "e-acsl-implementation"
+ "e-acsl-manual"
+ "eva-manual"
+ "metrics-manual"
+ "plugin-development-guide"
+ "rte-manual"
+ "user-manual"
+ "wp-manual"
+)
+
+COMPANIONS=(
+ "aorai-example"
+ "hello"
+)
+
+for manual in "${MANUALS[@]}"; do
+ prepare_file "$MANUALS_DIR/$manual.pdf"
+done
+
+for companion in "${COMPANIONS[@]}"; do
+ prepare_file "$MANUALS_DIR/$companion.tar.gz"
+done
+
+prepare_file "$MANUALS_DIR/acsl-version.txt"
+ACSL_VERSION=$(cat "$MANUALS_DIR/acsl-version.txt")
+prepare_file "$MANUALS_DIR/e-acsl-version.txt"
+EACSL_VERSION=$(cat "$MANUALS_DIR/e-acsl-version.txt")
+
+show_step "Searching for changes"
+
+CHANGES="releases/$VERSION_MAJOR.$VERSION_MINOR.md"
+prepare_file "$CHANGES"
+
+##########################################################################
+# File copy
+
+function generic_name {
+ if [ "$1" == "frama-c" ]; then echo "frama-c-source-dist"
+ elif [ "$1" == "acsl" ]; then echo "acsl"
+ elif [ "$1" == "e-acsl" ]; then echo "e-acsl"
+ elif [[ $1 =~ ^e-acsl.*$ ]]; then echo "$1"
+ else echo "frama-c-$1"
+ fi
+}
+function version_name {
+ if [ "$1" == "acsl" ]; then echo "acsl-$ACSL_VERSION"
+ elif [ "$1" == "e-acsl" ]; then echo "e-acsl-$EACSL_VERSION"
+ else echo "$1-$VERSION_AND_CODENAME"
+ fi
+}
+
+# For the 2 next functions
+# $1 : name
+# $2 : extension
+
+function copy_normal {
+ cp "$MANUALS_DIR/$1.$2" "$MANS_TARGET_DIR/$(generic_name "$1").$2"
+ cp "$MANUALS_DIR/$1.$2" "$MANS_TARGET_DIR/$(version_name "$1").$2"
+}
+
+function copy_e_acsl {
+ EACSL_TARGET_DIR="$MANS_TARGET_DIR/e-acsl"
+ cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(generic_name "$1").$2"
+ cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(version_name "$1").$2"
+}
+
+function copy_files {
+ for manual in "${MANUALS[@]}"; do
+ if [[ $manual =~ ^e-acsl.*$ ]]; then
+ copy_e_acsl "$manual" "pdf"
+ else
+ copy_normal "$manual" "pdf"
+ fi
+ done
+ for companion in "${COMPANIONS[@]}"; do
+ copy_normal "$companion" "tar.gz"
+ done
+
+ # Eva has an old manual name that might be in use:
+ cp "$MANS_TARGET_DIR/frama-c-eva-manual.pdf" "$MANS_TARGET_DIR/frama-c-value-analysis.pdf"
+
+ cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_VERSION"
+ cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_GENERIC"
+
+ cp $TARGZ_API "$MANS_TARGET_DIR/frama-c-$VERSION_AND_CODENAME-api.tar.gz"
+}
+
+##########################################################################
+# Make opam
+
+show_step "Building opam repository file"
+
+OPAM_DIR="opam-repository"
+OPAM_FC_DIR="$OPAM_DIR/packages/frama-c/frama-c.$VERSION"
+
+mkdir -p $OPAM_DIR
+mkdir -p $OPAM_FC_DIR
+
+cat opam/opam | grep -v "^version\:" | grep -v "^name\:" > $OPAM_FC_DIR/opam
+cat >>$OPAM_FC_DIR/opam << EOL
+
+url {
+ src: "$FRAMAC_COM_DOWNLOAD/$TARGZ_VERSION"
+ checksum: "sha256=$(sha256sum $TARGZ_BASE | cut -d" " -f1)"
+}
+EOL
+
+echo "Opam file built"
+
+##########################################################################
+# Make wiki
+
+show_step "Building wiki"
+
+WIKI_DIR="wiki"
+
+mkdir -p $WIKI_DIR
+
+echo "Download directory built"
+
+WIKI_PAGE="$WIKI_DIR/Frama-C-${VERSION_AND_CODENAME}.md"
+
+echo "# Frama-C release $VERSION ($CODENAME)" > $WIKI_PAGE
+echo "## Sources" >> $WIKI_PAGE
+echo "- [$TARGZ_VERSION]($FRAMAC_COM_DOWNLOAD/$TARGZ_VERSION)" >> $WIKI_PAGE
+echo "" >> $WIKI_PAGE
+echo "## Manuals" >> $WIKI_PAGE
+for manual in "${MANUALS[@]}"; do
+ if [[ $manual =~ ^e-acsl.*$ ]]; then
+ DIR="$FRAMAC_COM_DOWNLOAD/e-acsl"
+ else
+ DIR="$FRAMAC_COM_DOWNLOAD"
+ fi
+ NAME=$(version_name $manual)
+ echo "- [$manual]($DIR/$NAME.pdf)" >> $WIKI_PAGE
+done
+echo "" >> $WIKI_PAGE
+echo "## Companion archives" >> $WIKI_PAGE
+for archive in "${COMPANIONS[@]}"; do
+ NAME=$(version_name "$archive")
+ echo "- [$archive]($FRAMAC_COM_DOWNLOAD/$NAME.tar.gz)" >> $WIKI_PAGE
+done
+echo "" >> $WIKI_PAGE
+echo "## Main changes" >> $WIKI_PAGE
+sed 's/\(\#.*\)/##\1/' $CHANGES >> $WIKI_PAGE
+
+echo "Wiki page built"
+
+##########################################################################
+# Make wiki
+
+show_step "Building release json file"
+
+JSON_DATA="release-data.json"
+
+cat >$JSON_DATA <<EOL
+{
+ "name": "Frama-C $VERSION $CODENAME",
+ "tag_name": "$VERSION_SAFE",
+ "ref": "stable/$LOWER_CODENAME",
+ "assets": {
+ "links": [
+ {
+ "name": "API Documentation",
+ "url": "https://frama-c.com/download/frama-c-$VERSION_AND_CODENAME-api.tar.gz",
+ "link_type":"other"
+ },
+ {
+ "name": "Official source archive",
+ "url": "https://frama-c.com/download/$TARGZ_VERSION",
+ "link_type":"other"
+ }
+ ]
+ },
+EOL
+ echo " \"description\": \"# Main changes since $PREVIOUS $PREVIOUS_NAME\n$(sed "$CHANGES" -z 's/\n/\\n/g' | sed 's/\(\#.*\)/#\1/')\"" >> $JSON_DATA
+ echo "}" >> $JSON_DATA
+
+echo "Release data file built"
+
+##########################################################################
+# Make website
+
+show_step "Building website"
+
+WEBSITE_DIR="./website"
+WEBSITE_DL_DIR="$WEBSITE_DIR/download"
+WEBSITE_INST_DIR="$WEBSITE_DIR/html/installations"
+WEBSITE_EVENTS_DIR="$WEBSITE_DIR/_events"
+WEBSITE_VERSIONS_DIR="$WEBSITE_DIR/_fc-versions"
+
+mkdir -p $WEBSITE_DIR
+
+# Downloads
+
+mkdir -p $WEBSITE_DL_DIR
+mkdir -p $WEBSITE_DL_DIR/e-acsl
+
+GZ_TARGET_DIR=$WEBSITE_DL_DIR
+MANS_TARGET_DIR=$WEBSITE_DL_DIR
+
+copy_files
+
+echo "Download directory built"
+
+# Install
+
+mkdir -p $WEBSITE_INST_DIR
+
+INSTALL_WEBPAGE="$WEBSITE_INST_DIR/$LOWER_CODENAME.md"
+EXT="$FRAMAC_VERSION_CODENAME (released on $(date +%Y-%m-%d))"
+
+cat >$INSTALL_WEBPAGE <<EOL
+---
+layout: installation_page
+version: $LOWER_CODENAME
+title: Installation instructions for Frama-C $VERSION ($CODENAME)
+---
+EOL
+sed ./INSTALL.md -e "s/^\(# Installing Frama-C\)$/\1 $EXT/" >>$INSTALL_WEBPAGE
+
+echo "Installation file built"
+
+# Event
+
+mkdir -p $WEBSITE_EVENTS_DIR
+
+TEXTUAL_VERSION="Frama-C $VERSION ($CODENAME)"
+TEXTUAL_PREVIOUS="Frama-C $PREVIOUS ($PREVIOUS_NAME)"
+
+if [ "$FINAL_RELEASE" = "no" ]; then
+ EVENT_TITLE="Beta release of $TEXTUAL_VERSION"
+else
+ EVENT_TITLE="Release of $TEXTUAL_VERSION"
+fi
+VERSION_PAGE="/fc-versions/$LOWER_CODENAME.html"
+
+EVENT_WEBPAGE="$WEBSITE_EVENTS_DIR/framac-$VERSION_SAFE.md"
+
+cat >$EVENT_WEBPAGE <<EOL
+---
+layout: default
+date: $(date +\"%d-%m-%Y\")
+short_title: $TEXTUAL_VERSION
+title: $EVENT_TITLE
+link: /fc-versions/$LOWER_CODENAME.html
+---
+
+$TEXTUAL_VERSION is out. Download it [here]($VERSION_PAGE).
+
+Main changes with respect to $TEXTUAL_PREVIOUS include:
+
+EOL
+sed 's/\(\#.*\)/###\1/' $CHANGES >>$EVENT_WEBPAGE
+
+echo "Event file built"
+
+# Version
+
+mkdir -p $WEBSITE_VERSIONS_DIR
+VERSION_WEBPAGE="$WEBSITE_DIR/_fc-versions/$LOWER_CODENAME.md"
+
+if [ "$FINAL_RELEASE" = "no" ]; then
+ ACSL_OR_BETA="beta: true"
+else
+ ACSL_OR_BETA="acsl: $ACSL_VERSION"
+fi
+
+cat >$VERSION_WEBPAGE <<EOL
+---
+layout: version
+number: $VERSION_MAJOR
+name: $CODENAME
+$ACSL_OR_BETA
+releases:
+- number: $VERSION_MINOR
+ categories:
+ - name: Frama-C v$VERSION $CODENAME
+ files:
+ - name: Source distribution
+ link: /download/$TARGZ_VERSION
+ help: Compilation instructions
+ help_link: /html/installations/$LOWER_CODENAME.html
+ - name: User manual
+ link: /download/user-manual-$VERSION_AND_CODENAME.pdf
+ - name: Plug-in development guide
+ link: /download/plugin-development-guide-$VERSION_AND_CODENAME.pdf
+ help: Hello plug-in tutorial archive
+ help_link: /download/hello-$VERSION_AND_CODENAME.tar.gz
+ - name: API Documentation
+ link: /download/frama-c-$VERSION_AND_CODENAME-api.tar.gz
+ - name: ACSL $ACSL_VERSION ($CODENAME implementation)
+ link: /download/acsl-implementation-$VERSION_AND_CODENAME.pdf
+ - name: Plug-in Manuals
+ sort: true
+ files:
+ - name: Aoraï manual
+ link: /download/aorai-manual-$VERSION_AND_CODENAME.pdf
+ help: Aoraï example
+ help_link: /download/aorai-example-$VERSION_AND_CODENAME.tar.gz
+ - name: Metrics manual"
+ link: /download/metrics-manual-$VERSION_AND_CODENAME.pdf"
+ - name: Rte manual"
+ link: /download/rte-manual-$VERSION_AND_CODENAME.pdf"
+ - name: Eva manual"
+ link: /download/eva-manual-$VERSION_AND_CODENAME.pdf"
+ - name: WP manual"
+ link: /download/wp-manual-$VERSION_AND_CODENAME.pdf"
+ - name: E-ACSL manual"
+ link: /download/e-acsl/e-acsl-manual-$VERSION_AND_CODENAME.pdf"
+---
+EOL
+
+echo "Version file built"
diff --git a/bin/update_api_doc.sh b/dev/update_api_doc.sh
similarity index 100%
rename from bin/update_api_doc.sh
rename to dev/update_api_doc.sh
diff --git a/doc/Makefile b/doc/Makefile
index 584d88aec76d842370af34c38b77519793add281..7449ebf6b505600d5e295747868d015064fcb430 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -85,7 +85,7 @@ endif
clean::
$(RM) manuals/*.pdf
- $(RM) manuals/*.tgz
+ $(RM) manuals/*.tar.gz
$(MAKE) -C userman clean
$(MAKE) -C developer dist-clean
$(MAKE) -C rte clean
@@ -99,7 +99,8 @@ all: \
manuals/plugin-development-guide$(FC_SUFFIX).pdf \
manuals/rte-manual$(FC_SUFFIX).pdf \
manuals/aorai-manual$(FC_SUFFIX).pdf \
- manuals/aorai-example$(FC_SUFFIX).tgz \
+ manuals/aorai-example$(FC_SUFFIX).tar.gz \
+ manuals/hello$(FC_SUFFIX).tar.gz \
manuals/eva-manual$(FC_SUFFIX).pdf \
manuals/metrics-manual$(FC_SUFFIX).pdf \
manuals/wp-manual$(FC_SUFFIX).pdf \
@@ -112,7 +113,7 @@ manuals/%:
$(PRINT) Generating $@
$(MAKE) -C $(@D) $(@F)
-%.tgz:
+%.tar.gz:
$(PRINT) Generating $@
$(MAKE) -C $(@D) $(@F)
@@ -120,7 +121,8 @@ manuals/user-manual$(FC_SUFFIX).pdf: userman/userman.pdf
manuals/plugin-development-guide$(FC_SUFFIX).pdf: developer/developer.pdf
manuals/rte-manual$(FC_SUFFIX).pdf: rte/main.pdf
manuals/aorai-manual$(FC_SUFFIX).pdf: aorai/main.pdf
-manuals/aorai-example$(FC_SUFFIX).tgz: aorai/aorai-example.tgz
+manuals/aorai-example$(FC_SUFFIX).tar.gz: aorai/aorai-example.tar.gz
+manuals/hello$(FC_SUFFIX).tar.gz: developer/hello.tar.gz
manuals/eva-manual$(FC_SUFFIX).pdf: eva/main.pdf
manuals/metrics-manual$(FC_SUFFIX).pdf: metrics/metrics.pdf
manuals/wp-manual$(FC_SUFFIX).pdf: ../src/plugins/wp/doc/manual/wp.pdf
@@ -149,9 +151,13 @@ all: \
manuals/acsl-implementation$(FC_SUFFIX).pdf \
manuals/acsl$(ACSL_SUFFIX).pdf \
+version: manuals/acsl-version.txt
+
manuals/acsl-implementation$(FC_SUFFIX).pdf: acsl/acsl-implementation.pdf
manuals/acsl$(ACSL_SUFFIX).pdf: acsl/acsl.pdf
+manuals/acsl-version.txt:
+ echo ${ACSL_VERSION} > $@
###################
# E-ACSL #
@@ -182,12 +188,17 @@ clean::
all: \
manuals/e-acsl-implementation$(FC_SUFFIX).pdf \
manuals/e-acsl-manual$(FC_SUFFIX).pdf \
- manuals/e-acsl$(EACSL_SUFFIX).pdf \
+ manuals/e-acsl$(EACSL_SUFFIX).pdf
+
+version: manuals/e-acsl-version.txt
manuals/e-acsl-implementation$(FC_SUFFIX).pdf: $(EACSL_DOC)/refman/e-acsl-implementation.pdf
manuals/e-acsl-manual$(FC_SUFFIX).pdf: $(EACSL_DOC)/userman/main.pdf
manuals/e-acsl$(EACSL_SUFFIX).pdf: $(EACSL_DOC)/refman/e-acsl.pdf
+manuals/e-acsl-version.txt:
+ echo ${EACSL_VERSION} > $@
+
endif
# Note: The makefiles of ACSL/E-ACSL are not parallelizable when producing both
diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile
index 750c6c23f14ea14be2145c360c8613e03c85f89c..bb56a790d234ad42f524d822714cae0513757c0a 100644
--- a/doc/aorai/Makefile
+++ b/doc/aorai/Makefile
@@ -35,23 +35,23 @@ EXAMPLES=example.c example.ltl example.ya \
BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf
-all: main.pdf $(ARCHIVENAME).tgz
+all: main.pdf $(ARCHIVENAME).tar.gz
main.pdf: main.tex $(BNF:.bnf=.tex) macros.tex
touch main.aux #work around latexmk bug
latexmk -pdf main.tex
-$(ARCHIVENAME).tgz: $(addprefix example/, $(EXAMPLES))
+$(ARCHIVENAME).tar.gz: $(addprefix example/, $(EXAMPLES))
@rm -fr $(ARCHIVENAME)
@mkdir $(ARCHIVENAME)
@cp $^ $(ARCHIVENAME)
@tar czvf $@ $(ARCHIVENAME)
-install: main.pdf $(ARCHIVENAME).tgz
+install: main.pdf $(ARCHIVENAME).tar.gz
mkdir -p ../manuals
- @echo "copying example.tgz in ${DWNLDDIR}/$(ARCHIVENAME).tgz"
- @rm -f "${DWNLDDIR}/$(ARCHIVENAME).tgz"
- @cp $(ARCHIVENAME).tgz "${DWNLDDIR}/$(ARCHIVENAME).tgz"
+ @echo "copying example.tar.gz in ${DWNLDDIR}/$(ARCHIVENAME).tar.gz"
+ @rm -f "${DWNLDDIR}/$(ARCHIVENAME).tar.gz"
+ @cp $(ARCHIVENAME).tar.gz "${DWNLDDIR}/$(ARCHIVENAME).tar.gz"
@echo "copying main.pdf in $(DWNLDDIR)/$(DOCNAME)"
@rm -f "$(DWNLDDIR)/$(DOCNAME)"
@cp main.pdf "$(DWNLDDIR)/$(DOCNAME)"
@@ -62,7 +62,7 @@ clean:
*.cm? *.idx *.o pp.ml pp *.dvi *.blg *.bbl \
main???.png *.image.tex *.haux *.htoc *.html \
*.backup *.pdf *.backup example/frama_c_journal.ml \
- $(ARCHIVENAME) $(ARCHIVENAME).tgz
+ $(ARCHIVENAME) $(ARCHIVENAME).tar.gz
.SUFFIXES: .tex .bnf .ml .cmo .mll
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index c725a2b14245038604375a5f2e47eebcfcb948d6..8718ee6e1cca36aba202a62c04e5927f5f810949 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -143,20 +143,19 @@ check-viewcfg-v5:
check-viewcfg-v6:
cd tutorial/viewcfg/v2-* && $(duneb) @install
-archives: FILES=$(shell cd tutorial/hello/v7-doc && git ls-files)
+hello.tar.gz: FILES=$(shell cd tutorial/hello/v7-doc && git ls-files)
# - use 'git ls-files' to avoid including extraneous files in archive
# - use several tar options to improve build reproducibility
-archives:
- export VERSION="$(shell cat ../../VERSION)" && \
+hello.tar.gz:
cd tutorial/hello && \
- rm -rf hello-$$VERSION && \
- cp -r v7-doc hello-$$VERSION && \
- tar -cf - $(addprefix hello-$$VERSION/,$(FILES)) \
+ rm -rf hello && \
+ cp -r v7-doc hello && \
+ tar -cf - $(addprefix hello/,$(FILES)) \
--numeric-owner --owner=0 --group=0 --sort=name \
--mtime="$$(date +"%F") Z" --mode='a+rw' | \
- gzip -9 -n > ../../hello-$$VERSION.tar.gz && \
- rm -rf hello-$$VERSION
+ gzip -9 -n > ../../hello.tar.gz && \
+ rm -rf hello
###########
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index d91442d48cbb027e748ecdc55fa4054294a7af88..7313f46e5b9f437eb76841a23cb2e767432b599d 100644
--- a/doc/release/branch.tex
+++ b/doc/release/branch.tex
@@ -1,4 +1,5 @@
-\chapter{The Branch Stage}
+\chapter{Branch stage}
+\label{chap:branch}
That is the procedure for forking the release from \texttt{master}.
@@ -54,9 +55,11 @@ in the Frama-C group
\expertise{François, Julien}.
-\section{BTS}
+\section{GitLab issues}
-Check public issue tracker at \url{https://git.frama-c.com/pub/frama-c/issues/} All issues should have been at least acknowledged: at least they should be assigned to someone, preferably tagged appropriately.
+Check public issue tracker at \url{https://git.frama-c.com/pub/frama-c/issues/}.
+All issues should have been at least acknowledged: at least they should be
+assigned to someone, preferably tagged appropriately.
Send a message to the Frama-C channel on LSL's Mattermost.
Each developer should have a
@@ -98,7 +101,6 @@ This should go directly below
\begin{verbatim}
\section*{\framacversion}
\end{verbatim}
-
and this line should be commented out.
\begin{itemize}
@@ -119,11 +121,9 @@ merging back \texttt{stable/element} into \texttt{master}.
\section{Copyright}
-Check that the date in copyright headers is correct. If not then the script
-\texttt{headers/updates-headers.sh} can be used to update them.
-
+Check that the date in copyright headers is correct. If not then:
\begin{itemize}
- \item Update the dates in the license files in:
+ \item update the dates in the license files in:
\begin{itemize}
\item \texttt{headers/close-source/*}
\item \texttt{headers/open-source/*}
@@ -132,13 +132,11 @@ Check that the date in copyright headers is correct. If not then the script
\item \texttt{src/plugins/e-acsl/headers/close-source/*}
\item \texttt{src/plugins/e-acsl/headers/open-source/*}
\end{itemize}
- \item Update the headers with the following commands:
+ \item update the headers with the following command:
\begin{itemize}
- \item \texttt{./headers/updates-headers.sh headers/header\_spec.txt headers/open-source}
- \item \texttt{./headers/updates-headers.sh ivette/headers/header\_spec.txt headers/open-source ivette}
- \item \texttt{./headers/updates-headers.sh src/plugins/e-acsl/headers/header\_spec.txt src/plugins/e-acsl/headers/open-source src/plugins/e-acsl}
+ \item \texttt{make headers}
\end{itemize}
- \item Check if some copyright are left to update by \texttt{grep}-ing the date in the sources: \texttt{grep -r -e "-yyyy" .}
+ \item Check if some copyrights are left to update by \texttt{grep}-ing the date in the sources: \texttt{grep -r -e "-yyyy" .}
\end{itemize}
%%%Local Variables:
diff --git a/doc/release/build.tex b/doc/release/build.tex
deleted file mode 100644
index 898561b60232bc8b40dad66a74f1453b5d9fc62f..0000000000000000000000000000000000000000
--- a/doc/release/build.tex
+++ /dev/null
@@ -1,360 +0,0 @@
-\chapter{The Build Stage}
-
-The procedure for creating the source distribution.
-
-\section{Prerequisites}
-
-\begin{itemize}
-\item All tools needed to compile Frama-C (that you should have anyways)
-\item \texttt{bash} v4.0 or higher
-\item \texttt{git-lfs}
-\item GNU \texttt{parallel}
-\item a \TeX distribution (e.g. \TeX{}live),
-including notably the following utilities:
-\begin{itemize}
-\item \texttt{latexmk}
-\item (recommended) \texttt{texfot}
-\end{itemize}
-\end{itemize}
-
-\section{Final checks}
-
-\begin{itemize}
-
-\item Check plug-in dependencies in all \texttt{configure.*}, in case they have
- changed: if you don't know them, ask plug-in developers to verify them.
-
-\todo{should be done when the plugin is modified}
-
-\item Check the headers and corresponding licenses files for new files
- \todo{should be done when the plugin is modified}
-
-% (\texttt{make check-headers} is your friend, but it is done by CI anyway).
-
-
-\item Check the contents of \texttt{INSTALL.md} \todo{Should always be up to date}
- \begin{itemize}
- \item Update the Frama-C version number in the `Reference configuration` section
- \item In particular, check and update a full known good configuration for
- opam packages, including alt-ergo, why3, coq, etc.
- Use \verb+bin/check-reference-configuration.sh+ to help check if the
- configuration is ok. You can also try running
- \verb+make wp-qualif+.
- \end{itemize}
-\item Check the contents of \texttt{README.md} \todo{Should always be up to date}
-\item Check the contents of \texttt{Changelog}
- \todo{Should always be up to date}
-\item Carefully read the output of the configure to be sure that there are no
- buggy messages. Make sure you have required OPAM packages installed in your machine,
- e.g. alt-ergo.
-\end{itemize}
-
-\section{Update the Sources}\label{sec:update-sources}
-
-There are many administrative steps, coordinated by the release manager.
-\begin{enumerate}
-\item [{\em Non-beta only}] If a new version of the ACSL manual is to be released, make sure you also
- have a clone of the \texttt{acsl} manual Github repository
- (\url{git@github.com:acsl-language/acsl.git}) in the \texttt{doc}
- directory
-\item Update files \texttt{VERSION} and \texttt{VERSION\_CODENAME}
- (for beta releases, add suffix \texttt{\textasciitilde{}beta})
-\item [{\em Non-beta only}] Update file \texttt{ALL\_VERSIONS}. \todo{This section must be put somewhere else in the release manual}
-\item Update files
- \texttt{src/plugins/wp/Changelog} and
- \texttt{src/plugins/e-acsl/doc/Changelog},
- to add the header corresponding to the
- new version. % For the final release, use the script
- % \texttt{doc/changelog/generate} to check that the HTML page can be built,
- % and check its contents.
-\item Update the Frama-C's authors list in files
- \texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}.
- Traditionally, an author is added if they have contributed 100+ LoC in
- the release, as counted by:
- \begin{verbatim}
- git ls-files -z | \
- parallel -0 -n1 git blame --line-porcelain | \
- sed -n 's/^author //p' | sort -f | uniq -ic | sort -nr
- \end{verbatim}
- (source for the command: \url{https://gist.github.com/amitchhajer/4461043})
-\item Recompile and test to check that all is fine.
-\item Check the documentation as per Section~\ref{update_doc}
-\item update the \texttt{opam} directory: update the version name and
- version number in the fields \texttt{version}, \texttt{doc} and
- \texttt{depends} in \texttt{opam/opam}. \textbf{NB:} for a beta version, be sure
- to use a tilde \textasciitilde{} between the version number and \texttt{beta},
- and not a dash \texttt{-}.
-\item Create the last commit
-\item Create the tag using \texttt{git tag \$(cat VERSION | sed -e "s/~/-/")} and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/~/-/")})
-\end{enumerate}
-
-\section{Update the Documentation}\label{update_doc}
-
-\subsection{Manuals}
-
-Most manuals depend on the \texttt{VERSION} file, so make sure to regenerate
-them when this file changes.
-Also, most of the manuals include an appendix with the list of
-changes that have happened, divided by version of Frama-C. Make sure that the
-first section has the correct release name.
-
-\todo{Mention the other things that change from one release to the
- other, such as the ACSL version number}
-
-\todo{The release manager should create fresh Changes sections in \texttt{master}. But When?: at fork time, or when the release is ready?}
-
-
-The official \FramaC documents relative to the kernel and ACSL to be released
-must be recompiled in order to take into account the \texttt{VERSION}
-file:
-
-\begin{center}
- \begin{tabular}{lll}
- \hline
- \textsf{User Manual} &
- \texttt{doc/userman} &
- \expertise{Julien} \\
- \textsf{Developer Manual} &
- \texttt{doc/developer} &
- \expertise{Julien} \\
- \textsf{ACSL Implementation} &
- \texttt{doc/acsl} (from Github) &
- \expertise{Virgile} \\
- % \textsf{man page} &
- % \texttt{man/frama-c.1} &
- % \expertise{Virgile} \\
- \hline
- \end{tabular}
-\end{center}
-
-Documents relative to the plug-ins can be found at the same place. This list
-isn't exhaustive:
-
-\begin{center}
- \begin{tabular}{lll}
- \hline
- \textsf{RTE} &
- \texttt{doc/rte} &
- \expertise{Julien} \\
- \textsf{Aoraï} &
- \texttt{doc/aorai} &
- \expertise{Virgile} \\
- \textsf{Metrics} &
- \texttt{doc/metrics} &
- \expertise{André} \\
- \textsf{Eva} &
- \texttt{doc/eva} &
- \expertise{David} \\
- \textsf{WP} &
- \texttt{src/plugins/wp/doc/manual/} &
- \expertise{Loïc} \\
- \end{tabular}
-\end{center}
-
-Clone the \texttt{acsl} manual
-(\url{git@github.com:acsl-language/acsl.git}) in
-\texttt{doc/acsl} in order to generate the ACSL reference and implementation
-manuals.
-
-% manuals (which uses git-annex) are now deprecated in favor of using the
-% Github wiki
-%Clone the \texttt{manuals} repository
-%(\url{git@git.frama-c.com:frama-c/manuals.git}) in
-%\texttt{doc/manuals} in order to update the manuals (required by the
-%\texttt{install} target below).
-
-In the \texttt{doc} directory, just run \texttt{make all} to compile
-and install all manuals, together with some final coherence checks with
-respect to the current Frama-C implementation (notably
-for the developer manual and ACSL implementation manual).
-
-% No longer use git annex (as recommended by VP)
-%\paragraph{Getting the manuals on the web (ultimately)}
-%
-% In \texttt{doc/manuals} after installing all the manuals:
-%\begin{shell}
-%git annex add .
-%git annex copy . --to origin
-%git commit -am "manuals for release ...."
-%git push
-%\end{shell}
-
-\subsection{API documentation}
-
-To update the \textsf{API} documentation, you must update the
-\texttt{@since} tags. This involves the following script (\texttt{sed -i} must
-work for this purpose):
-\begin{shell}
-./bin/update_api_doc.sh <NEXT>
-\end{shell}
-\verb+<NEXT>+ is the long name of the final release, i.e.
-\verb+`cat VERSION`-`VERSION_CODENAME`+
-(without the \verb+beta+ suffix, if any).
-
-Check that no \verb|+dev| suffix remains inside comments:
-
-\begin{shell}
-git grep +dev src
-\end{shell}
-
-Test by recompiling Frama-C and rebuilding the API documentation:
-\begin{shell}
-make -j byte gui-byte
-make doc # or just doc-kernel
-\end{shell}
-
-You can also check that the elements referred to in the index of the
-development guide are marked as such in the API doc and vice-versa
-by issuing \texttt{make check-devguide}.
-
-\section{Build the Source Distribution}
-\label{sec:build-source-distr}
-
-This steps creates the tarball of Frama-C, the tarball of the API and
-copy them to the website. It also copies the manuals.
-
-\textbf{Note}: all standard plugins must be enabled to ensure they are distributed
-in the \verb+.tar.gz+. Some plug-ins require optional dependencies
-(e.g. markdown-report and \verb+ppx_deriving+), so you must ensure that,
-when running \verb+./configure+, no plugins that should be distributed are missing.
-Some of the checks are performed by the release build script, but not all of them.
-Also, some plug-ins may have components depending on optional packages
-(e.g. Server and \verb+zmq+), which are not always thoroughly tested. If such
-plug-ins are only partially enabled, check that the non-compiled sources are
-distributed in any case, or report it as a bug to their developers.
-
-If you have never run \verb+make src-distrib+, you can try a standalone build
-of the \verb+.tar.gz+ itself, before doing the rest (don't forget to use
-\verb+OPEN_SOURCE=yes+).
-Refer to Appendix \ref{chap:make-src-distrib} if you have problems when
-doing so. In any case, the archive will be recreated by a script, so you can
-skip this step.
-
-You need to have installed \texttt{git-lfs}, otherwise the build
-script will not correctly use lfs when putting large files in the
-website git.
-
-\expertise{release manager} Use the script
-\texttt{build-src-distrib.sh} for this purpose (\texttt{bash version
- 4} required).
-
-The script will search for the following repositories:
-
-\begin{itemize}
- \item \texttt{./doc/acsl} (\texttt{git@github.com:acsl-language/acsl.git})
- \item \texttt{./frama-c.wiki} (\texttt{git@git.frama-c.com:pub/frama-c.wiki.git})
- \item \texttt{./website} (\texttt{git@git.frama-c.com:pub/pub.frama-c.com.git})
-\end{itemize}
-
-If they are not available, they can be cloned by the script.
-
-The following steps will be performed by the script:
-
-\begin{itemize}
- \item compile manuals
- \item build source distribution
- \item build the API bundle
- \item build the documentation companions
- \item update locally the wiki pages
- \item create a new branch for the website
- \item run some sanity checks on the source distribution
- \item generate the \texttt{opam} file
-\end{itemize}
-
-In order to create "ready to deploy" wiki and website pages, a file \texttt{main\_changes.md}
-must be provided. The expected format is:
-
-\begin{lstlisting}
-# Kernel
-
-- item
-- ...
-
-# <Plugin-Name> (Prefer alphabetic order)
-
-- item
-- ...
-
-# ...
-
-\end{lstlisting}
-
-The performed sanity checks are:
-
-\begin{itemize}
- \item verification that no non-free files are distributed,
- \item verification that no non-free plugins are distributed,
- \item no \texttt{/home/user} path can be found in the distribution,
- \item the source code can be compiled and tests succeed.
-\end{itemize}
-
-Note that there are some interactive steps in the script, that ask for user
-approval before going further.
-
-Finally, ensure that locale \verb+en_US.UTF-8+ is available on your system,
-as it is used by the script to ensure a proper encoding of the generated files.
-
-Now, run the script:
-\begin{shell}
-./bin/build-src-distrib.sh
-\end{shell}
-
-The generated files are available in the \texttt{./distributed} repository.
-After testing more extensively the distribution, the following actions should
-be performed:
-
-\begin{itemize}
- \item push stable branch on the public repository
- \item push stable tag on the public repository
- \item push the local Frama-C wiki branch to the public repository
- \item push the generated website branch
-\end{itemize}
-
-\section{Testing the Distribution}
-
-Please check that the distribution (sources and API) is OK:
-\begin{enumerate}
-\item check for possible path/environment leaks in the \texttt{tar.gz}:
- grep for the path where your Frama-C git directory is, e.g.
- \texttt{/home/user/git/frama-c}. It should appear nowhere in the archive.
-\item check that \texttt{./configure \&\& make -j \&\& sudo make install} works fine
- (or check e.g. \texttt{./configure --prefix=\$PWD/build \&\& make -j \&\& make install});
-\item Alternatively, you can use \texttt{docker} to compile the archive against a
- precise configuration:
- \begin{itemize}
- \item \verb+cp distributed/frama-c-<VERSION>.tar.gz developer_tools/docker+
- \item \verb+cd developer_tools/docker+
- \item \verb+make Dockerfile.dev+
- \item \verb+docker build . -t framac/frama-c:dev --target frama-c-gui-slim \+\\
- \verb+ -f Dockerfile.dev --build-arg=from_archive=frama-c-<VERSION>.tar.gz+
- \end{itemize}
-\item test the installed binaries (especially the GUI). (On Linux, OCI tests
- everything but the GUI); If you've taken the \texttt{docker} route, you might
- want to install the \href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script,
- in order to be able to launch
- \verb+x11docker framac/frama-c:dev frama-c-gui+
-\item redo the two steps above on Windows/WSL \expertise{André}\expertise{Allan},
- macOS \expertise{André}\expertise{Loïc}\\\expertise{Thibaud};
- \begin{itemize}
- \item For instance, you can compile and test as follows:
- \item \verb+./configure --prefix="$PWD/build"+
- \item \verb+make+;
- \item \verb+make install+;
- \item \verb+rm -f ~/.why3.conf; why3 config detect+;
- \item \verb+build/bin/frama-c tests/idct/*.c -eva -wp -wp-rte+
- \item If you have a GUI, replace \verb+frama-c+ above with \verb+frama-c-gui+
- and click around, see if things work (e.g. no segmentation faults).
- \end{itemize}
-\item have a look at the documentation of the API (untar, open
- \texttt{index.html} in a browser, click on a few links, etc).
- If there are minor bugs/typos, note them for later, but it's not
- worth delaying the release to fix them.
-\item consider decompressing both the current and the previous release archives
- in different directories, then using \texttt{meld} to compare them. This
- allows spotting if some files were unexpectedly added, for instance.
-\end{enumerate}
-
-
-%%%Local Variables:
-%%%TeX-master: "release"
-%%%End:
diff --git a/doc/release/website.tex b/doc/release/deploy.tex
similarity index 56%
rename from doc/release/website.tex
rename to doc/release/deploy.tex
index 7ad669583bc3abacb66312895893ef9a2350605b..7218143d80b17fd1d1114a81469b8dc063498e62 100644
--- a/doc/release/website.tex
+++ b/doc/release/deploy.tex
@@ -1,30 +1,40 @@
-\chapter{The Web Stage}
+\chapter{Deployment stage}
+\label{chap:deploy}
-Where all our efforts goes on the web. There are two very different
-tasks for \FramaC to go online. Authoring the web site pages is the
-responsibility of the developers and the release manager. Publishing
-the web site can only be performed by authorized people, who may not
-be the release manager.
+The validation stage (Chapter~\ref{chap:validation}) must be complete before
+starting this stage. The tasks listed in this section are mostly performed by
+the Release Manager.
-\section{Requirements}
+\section{Release pipeline}
-The website \texttt{README.md} provides a quick guide to locally setup
-the website.
-
-\section{Generate website}
-
-Before pushing the branch to the website, it can be deployed locally but
-this is not absolutely necessary.
-
-Push the branch generated by the release script on the website repository.
-
-You can have a look at the generated pages on \texttt{pub.frama-c.com} (after
-the \texttt{deploy} target of the website's continuous integration has successfully run.
-This can take a few minutes if the server is loaded).
-Note however that the download links won't work as they are available only
-once the branch is merged (\texttt{download} links are handled by Git-LFS).
+Go to the CI/CD section of GitLab. Start the release pipeline:
+\begin{itemize}
+ \item click ``Run Pipeline''
+ \item select the stable branch
+ \item add the variable \texttt{RELEASE} with value \texttt{yes}
+ \item run the pipeline.
+\end{itemize}
-Check the following pages:
+All tests will be run, as well as the \texttt{opam-pin} target and the job that
+create the release artifacts. The most important for the remaining tasks are the
+following:
+\begin{description}
+\item[\texttt{release-content}] has all generated artifacts
+\item[\texttt{release-website}] creates a merge-request assigned to
+ you on the website repository,
+\item[\texttt{release-wiki}] creates a wiki page on the public
+ Frama-C repository (you can see a link in the Activity section),
+\item[\texttt{release-opam}] creates the branch on the opam-repository
+ of the Frama-C organization on GitHub for Opam release,
+\item[\texttt{release-branch}] is ready to push the stable branch on
+ the public repo (it must be started manually)
+\item[\texttt{release-create}] is ready to create the GitLab release
+ on \texttt{pub} (it must be started manually and requires the branch).
+\end{description}
+
+\section{Check the website}
+
+Once the pipeline for the website has run, open \texttt{https://pub.frama-c.com}.
\begin{itemize}
\item \texttt{index.html} must display:
@@ -56,10 +66,7 @@ For a final version, the installation pages for:
\item \texttt{/html/installations/previous\_version\_name.html} should indicate older version
\end{itemize}
-On GitLab, the following files must appear as \textbf{new} in \texttt{download}.
-Note that for beta versions, if you have not included all manuals, not all of
-them will appear:
-
+On GitLab, the following files must appear as \textbf{new} in \texttt{download}:
\begin{itemize}
\item \texttt{acsl-X.XX.pdf}
\item \texttt{acsl-implementation-NN.N-CODENAME.pdf}
@@ -70,7 +77,7 @@ them will appear:
\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{aorai-example-NN.N-CODENAME.tar.gz}
\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}
@@ -88,10 +95,30 @@ For final release \textbf{ONLY}, the following files must appear as \textbf{modi
\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{frama-c-aorai-example.tar.gz}
\item \texttt{hello.tar.gz}
\end{itemize}
+If everything is fine, merge the website and ask a website maintainer to put it
+online (\expertise{Allan, Augustin}).
+
+\section{Public GitLab}
+
+Open the generated wiki page (visible in the public website activity). Check the
+links (files are available only once the website has been put online). If
+everything is fine, edit the main wiki page and the sidebar with a link to the
+page (\url{https://git.frama-c.com/pub/frama-c/-/wikis/home}).
+
+In the release pipeline, run the job \texttt{release - release-branch}. It will
+push the stable branch on the public repository.
+
+Then, 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}
@@ -104,62 +131,10 @@ For final release \textbf{ONLY}, the following files must appear as \textbf{modi
\section{Opam package}
You'll need a GitHub account to create a pull request on the official opam repository,
-\texttt{ocaml/opam-repository.git}.
-
-\begin{itemize}
-\item Clone \texttt{opam-repository}: \texttt{git clone git@github.com:ocaml/opam-repository.git}
-\item Make sure you are on \texttt{master} and your branch is up-to-date
-\item Create a new directory: \\
- \texttt{packages/frama-c/frama-c.<version>}
-\item Copy the file \texttt{./distributed/opam} to the opam repository clone in: \\
- \texttt{packages/frama-c/frama-c.<version>/opam}
-\item You can provide \verb|sha256| and/or \verb|sha512| checksums at the end of this file if ou wish.
-\item (optional) Check locally that everything is fine:
-\begin{verbatim}
-opam switch create local <some-ocaml-compiler-version>
-opam repository add local <path-to-repository-clone>
-opam repository set-repos local
-opam install frama-c
-\end{verbatim}
-(of course, if you already create a local switch before and it uses your
-local version of the repository, you just have to switch to it).
-
-\textbf{Note:} uncommitted changes are ignored by \texttt{opam repository};
-you have to locally commit them before \texttt{opam update} will take them into
-account.
-
-\item Create a branch with any name you want (e.g. frama-c.<version>) and push it to your remote Github
-\item Create a pull request to opam-repository. If all tests pass,
- someone from opam should merge it for you.
- \textbf{Note:} some opam tests may fail due to external circumstances; if the
- error log makes no sense to you, wait to see if someone will contact you
- about it, or ask directly on the merge request.
-\end{itemize}
-
-\section{Updating pub/frama-c}
-
-You'll need to be member of the \texttt{pub/frama-c} project to be able to
-commit to it.
-
-\begin{itemize}
-\item add the \texttt{pub/frama-c} remote to your Git clone;
-\item make sure the last commit is tagged (either a release candidate, or a
- final release);
-\item push the stable/\texttt{<codename>} branch to the \texttt{pub} remote.
-\end{itemize}
-
-({\em Non-beta only}) After pushing the tag to Gitlab, go to the Releases page
-and create a release for the tag.
-
-You should also push the wiki changes. Note that all files listed as \textbf{new}
-in the website section should appear in the wiki but:
-
-\begin{itemize}
- \item \texttt{frama-c-api-NN.N-CODENAME.tar.gz}
- \item \texttt{hello-NN.N-CODENAME.tar.gz}
-\end{itemize}
-
-and E-ACSL files are not in a sub-folder \texttt{e-acsl} on the wiki.
+\texttt{ocaml/opam-repository.git}. Go to the Frama-C GitHub organization opam
+repository (\url{https://github.com/Frama-C/opam-repository}). Find the branch
+corresponding to the release and create the pull-request on the official opam
+repository.
\section{Other repositories to update}
@@ -174,13 +149,12 @@ Check if other Frama-C (and related) repositories need to be updated:
\section{Preparing the Next Release}
-Just update the \texttt{VERSION} file in \texttt{master}, by adding
-\texttt{"+dev"}. Do not add any newline at the end of the
-\texttt{VERSION} file.
+Just update the \texttt{VERSION} file in \texttt{master}, by adding \texttt{"+dev"}.
\section{Docker image preparation}
-\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be able to upload the image.
+\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be
+able to upload the image.
Make sure that \texttt{devel\_tools/docker/Makefile} is up-to-date:
diff --git a/doc/release/intro.tex b/doc/release/intro.tex
index 3c37a442b6952117321a42789d46f157bd005503..7a0434bb42c4edf95410699141d9898e27f4883e 100644
--- a/doc/release/intro.tex
+++ b/doc/release/intro.tex
@@ -20,7 +20,7 @@ roles, and we must distinguish between:
%% \item[Binary Builders:] they are responsible for creating a binary distribution
%% of the release for a specific architecture \expertise{none currently}.
\item[Web Site Maintainers:] they are responsible for updating the web site,
- during the release and for possible later updates \expertise{Florent ? Thibaud ?}.
+ during the release and for possible later updates \expertise{Allan, Augustin}.
\item[Release Manager:] they are responsible for the organisation of the
release process
\end{description}
@@ -30,24 +30,23 @@ roles, and we must distinguish between:
A \FramaC release consists of the following main steps:
\begin{enumerate}
-\item \textbf{The branch stage.} A branch is created, in which the release
- will be prepared. It will ultimately become the released version.
- The development of unstable features may continue in master, while the
- branch is dedicated to the ongoing release.
-
-\item \textbf{The build stage.} The source files are setup by the
- developers, and the bug tracking system is updated to reflect the
- distribution state. A source distribution is created and registered,
- with its updated documentation.
-
-\item \textbf{The web stage.} A snap-shot of the complete web site is
- created, by merging the new release files with the old,
- already distributed ones. %% Some old data might be dropped away if
- %% necessary, although they are still committed somewhere in the
- %% repository.
-
-\item \textbf{The go-online stage}. The web-site snapshot is put on
- the web. Time to notify the world!
+\item \textbf{The branch stage (Chapter~\ref{chap:branch}).} A branch is
+ created, in which the release will be prepared. It will ultimately become the
+ released version. The development of unstable features may continue in master,
+ while the branch is dedicated to the ongoing release.
+
+\item \textbf{The validation stage (Chapter~\ref{chap:validation}).} When we
+ estimate that \FramaC is ready to be released, the bug tracking system is
+ updated to reflect the distribution state. All artifacts that must be
+ distributed are generated in the continuous integration and validated by the
+ Release Manager. The version commit is created and tagged.
+
+\item \textbf{The deployment stage (Chapter~\ref{chap:deploy}).} The Release
+ Manager starts the release pipeline in the continuous integration. The last
+ stage releases the branch, the GitLab release, the website, the wiki and
+ creates an opam repository branch on the Frama-C organisation on GitHub. Time
+ to send an email on the Frama-C discuss mailing list, tweet and spread the
+ world!
\end{enumerate}
diff --git a/doc/release/release.tex b/doc/release/release.tex
index c55488d82ec4a05115a7cf51d188cbec6c0f55f6..08d23cef1011d33c4b193dd4ff969ef19052efbe 100644
--- a/doc/release/release.tex
+++ b/doc/release/release.tex
@@ -17,8 +17,8 @@
\input{intro}
\input{branch}
-\input{build}
-\input{website}
+\input{validation}
+\input{deploy}
\input{standalone-src}
\end{document}
diff --git a/doc/release/standalone-src.tex b/doc/release/standalone-src.tex
index 8fd3429af287568bf55759e0da8221e79b8f8e25..e061edd7804d1597e5d3e650da3b37eba772be03 100644
--- a/doc/release/standalone-src.tex
+++ b/doc/release/standalone-src.tex
@@ -4,48 +4,23 @@
\label{chap:make-src-distrib}
Requirements and tips to create a source release of Frama-C
-(i.e. \texttt{make src-distrib}).
+(i.e. \texttt{dev/make-distrib.sh}).
\section{Requirements}
You will need the following programs:
\begin{itemize}
-\item a custom (unreleased) version of \texttt{headache};
\item on Mac OS, binaries \texttt{gtar} and \texttt{gzip}.
\end{itemize}
Details about how to install them are presented below.
-\section{Custom headache}
-
-Clone the following repository (by default, every Frama-C developer has
-access to it):
-
-\texttt{git clone git@git.frama-c.com/dev/headache.git}
-
-Then run:
-
-\verb+./configure && make && make install+
-
-Note that some extra opam packages may be needed, such as \texttt{camomile}.
-
-This version of \texttt{headache} needs to be in your PATH for the next steps.
-
\section{Check your headers}
-Before making a source distribution, make sure your headers are up-to-date,
-by running:
-
-\texttt{make check-headers}
-
-Any plug-ins you are distributing along with Frama-C should have their
-distributed files (all OCaml sources, plus those listed in
-\verb+PLUGIN_DISTRIBUTED_EXTERNAL+) listed in file:
-
-\verb+headers/header_spec.txt+
-
-Their headers will then be checked by the above make target.
+Headers are checked by the script. For external plugins, they must provide a
+\texttt{.gitattributes} file as \texttt{git} is used to find the headers to
+apply.
\textbf{Note:} if you fail to check your headers, the distribution script may
corrupt your files. You were warned.
@@ -75,10 +50,10 @@ or an {\em open-source} distribution.
inside a virtual machine for a paper).
\end{itemize}
-Use Makefile variable \verb+OPEN_SOURCE=yes+ to create an open-source release,
+Use the variable \verb+OPEN_SOURCE=yes+ to create an open-source release,
as in:
-\verb+make src-distrib OPEN_SOURCE=yes+
+\verb+OPEN_SOURCE=yes ./dev/make-distrib.sh+
Otherwise, by default a closed-source archive will be created.
diff --git a/doc/release/validation.tex b/doc/release/validation.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5a73843cb085290b46dfe7605d806ce4e11580e7
--- /dev/null
+++ b/doc/release/validation.tex
@@ -0,0 +1,201 @@
+\chapter{Validation stage}
+\label{chap:validation}
+
+Final validation before running the release pipeline.
+
+\section{Prerequisites on dependencies}
+
+Install all dependencies of Frama-C, including recommended ones.
+
+Check coherence between:
+\begin{itemize}
+ \item \texttt{opam/opam} \todo{Should always be up to date}
+ \item \texttt{reference-configuration.md} \todo{Should always be up to date}
+\end{itemize}
+
+Run the command:
+\begin{itemize}
+ \item \texttt{dune build @frama-c-configure}
+\end{itemize}
+all plugins should be enabled. Check dependencies in case they have changed.
+If you don't know them, ask plug-in developers to verify them.
+
+\section{Prerequisites on installation}
+
+\begin{itemize}
+ \item Check the contents of \texttt{INSTALL.md} \todo{Should always be up to date}
+ \item Check the contents of \texttt{README.md} \todo{Should always be up to date}
+\end{itemize}
+
+\section{Fix version}
+
+The tasks listed in this section are performed by the Release Manager.
+
+\subsection{Versions in documentation files}
+
+Check the following files:
+\begin{itemize}
+ \item \texttt{ALL\_VERSIONS} (non-beta only)
+ \item \texttt{VERSION} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
+ \item \texttt{VERSION\_CODENAME}
+ \item \texttt{Changelog}
+ \item \texttt{src/plugins/wp/Changelog}
+ \item \texttt{src/plugins/e-acsl/doc/Changelog}
+ \item \texttt{INSTALL.md} ("Reference configuration")
+ \item \texttt{opam/opam} (for beta releases, add suffix \texttt{\textasciitilde{}beta}, not \texttt{-beta})
+\end{itemize}
+
+\subsection{Versions in source: API documentation}
+
+To update the \textsf{API} documentation, you must update the \texttt{@since}
+tags. This involves the following script (\texttt{sed -i} must work for this
+purpose):
+\begin{shell}
+./dev/update_api_doc.sh <NEXT>
+\end{shell}
+\verb+<NEXT>+ is the long name of the final release, i.e.
+\verb+`cat VERSION`-`VERSION_CODENAME`+
+(without the \verb+beta+ suffix, if any).
+
+Check that no \verb|+dev| suffix remains inside comments:
+
+\begin{shell}
+git grep +dev src
+\end{shell}
+
+Test by recompiling Frama-C and rebuilding the API documentation:
+\begin{shell}
+dune build @install
+dune build @doc
+\end{shell}
+
+You can also check that the elements referred to in the index of the
+development guide are marked as such in the API doc and vice-versa
+by issuing \texttt{make check-devguide}\todo{Fix this}.
+
+\subsection{Manuals}
+
+Manuals are built by the continuous integration. However, the Release Manager
+should check whether a new version of ACSL or E-ACSL must be released.
+
+Also, most of the manuals include an appendix with the list of changes that have
+happened, divided by version of Frama-C. Make sure that the first section has
+the correct release name.
+
+Manuals experts:
+\begin{center}
+ \begin{tabular}{lll}
+ \hline
+ \textsf{User Manual} & \texttt{doc/userman} & \expertise{Julien} \\
+ \textsf{Developer Guide} & \texttt{doc/developer} & \expertise{Julien} \\
+ \textsf{ACSL} & (from Github) & \expertise{Virgile} \\
+ \textsf{Aoraï} & \texttt{doc/aorai} & \expertise{Virgile} \\
+ \textsf{E-ACSL} & \texttt{src/plugins/e-acsl/doc/*} & \expertise{Julien} \\
+ \textsf{Eva} & \texttt{doc/eva} & \expertise{David} \\
+ \textsf{Metrics} & \texttt{doc/metrics} & \expertise{André} \\
+ \textsf{RTE} & \texttt{doc/rte} & \expertise{Julien} \\
+ \textsf{WP} & \texttt{src/plugins/wp/doc/manual/} & \expertise{Loïc} \\
+ \end{tabular}
+\end{center}
+
+\subsection{Contributors}
+
+Update the Frama-C's authors list in files
+\texttt{src/plugins/gui/help\_manager.ml} and \texttt{opam/opam}. Traditionally,
+an author is added if they have contributed 100+ LoC in the release, as counted
+by:
+\begin{verbatim}
+git ls-files -z | \
+parallel -0 -n1 git blame --line-porcelain | \
+sed -n 's/^author //p' | sort -f | uniq -ic | sort -nr
+\end{verbatim}
+(source for the command: \url{https://gist.github.com/amitchhajer/4461043})
+
+\subsection{Commit}
+
+Commit any change that you have done during these checks \textbf{and push}.
+
+\section{Last pipeline artifacts validation}
+
+In the last continuous integration pipeline of the release branch, force the
+run of the following targets:
+\begin{itemize}
+ \item manuals
+ \item opam-pin
+\end{itemize}
+Both should succeed. Collect the artifacts of the following targets:
+\begin{itemize}
+ \item api-doc
+ \item build-distrib-tarball
+ \item manuals
+\end{itemize}
+
+Check that these artifacts are as expected. In particular:
+\begin{itemize}
+ \item API documentatation:
+ \begin{itemize}
+ \item check that you can browse the API documentation
+ \item if there are minor bugs/typos, note them for later, but it's not
+ worth delaying the release to fix them.
+ \end{itemize}
+ \item Check versions in manuals
+ \item Tarball
+ \begin{itemize}
+ \item Check that no non-free components are distributed
+ \item Check that no \texttt{/home/user} path can be found in the distribution,
+ \item Build and test
+ \begin{itemize}
+ \item on Linux (the CI has already done it, but the GUI is not tested)
+ \item on MacOS \expertise{André, Loïc}
+ \item on Windows (WSL) \expertise{Allan, André}
+ \end{itemize}
+ \item consider decompressing both the current and the previous release
+ archives in different directories, then using \texttt{meld} to compare
+ them. This allows spotting if some files were unexpectedly added, for
+ instance.
+ \end{itemize}
+\end{itemize}
+
+Alternatively, you can use \texttt{docker} to compile the archive against a
+precise configuration:
+\begin{itemize}
+ \item \verb+cp distributed/frama-c-<VERSION>.tar.gz developer_tools/docker+
+ \item \verb+cd developer_tools/docker+
+ \item \verb+make Dockerfile.dev+
+ \item \verb+docker build . -t framac/frama-c:dev --target frama-c-gui-slim \+\\
+ \verb+ -f Dockerfile.dev --build-arg=from_archive=frama-c-<VERSION>.tar.gz+
+\end{itemize}
+For the GUI: you might want to install the
+\href{https://github.com/mviereck/x11docker}{\texttt{x11docker}} script, in
+order to be able to launch \verb+x11docker framac/frama-c:dev frama-c-gui+
+
+\section{Validate release}
+
+Create the main changes file in the directory \texttt{releases}. This file must
+be named <VERSION without ext>.md (e.g. \texttt{25.0}: \texttt{25.0.md},
+\texttt{25.0~beta}: \texttt{25.0.md}, \texttt{25.1}: \texttt{25.1.md}). The
+expected format is:
+
+\begin{lstlisting}
+ # Kernel
+
+ - item
+ - ...
+
+ # <Plugin-Name> (Prefer alphabetic order)
+
+ - item
+ - ...
+
+ # ...
+\end{lstlisting}
+
+It should only list main changes, that will be displayed on the event section
+of the website and the wiki page.
+
+Create the version commit, tag it using \texttt{git tag \$(cat VERSION | sed -e "s/~/-/")}
+and push it (e.g. via \texttt{git push origin \$(cat VERSION | sed -e "s/~/-/")}).
+
+%%%Local Variables:
+%%%TeX-master: "release"
+%%%End:
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
index 9ccc398534f01b7848d92fdb420313ba38e8ffc8..de0483335050f1ba782ec032815c3c65804e1f3b 100644
--- a/nix/frama-c-checkers-shell.nix
+++ b/nix/frama-c-checkers-shell.nix
@@ -3,6 +3,7 @@
, clang_10
, frama-c-hdrck
, git
+, git-lfs
, gnumake
, headache
, ocp-indent
@@ -13,6 +14,7 @@ stdenv.mkDerivation rec {
clang_10
frama-c-hdrck
git
+ git-lfs
gnumake
headache
ocp-indent
diff --git a/nix/frama-c-public/known_hosts b/nix/frama-c-public/known_hosts
index 9d81a10a357ba18eec5f4ef0aee7e46752dfca5d..9d94a4739586650ec348f127a57f756673d14e9f 100644
--- a/nix/frama-c-public/known_hosts
+++ b/nix/frama-c-public/known_hosts
@@ -4,3 +4,6 @@ git.frama-c.com ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHAyNTYAAAAIbmlzdHAy
54.38.94.65 ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQCuywpGMKnFOqiZn32w7X1k2UbP09NLpwQkqj2dDmm9hn+Yh5MyG9qCMpPplDQW3ywyW1tvyyUDEop0modY+JL1C+CmGPPLiA3PvLQTwJZ/sKT0bGjYFlrKK6f7B6wbwvWB9KkyIdt/3VQOA+HY3ILn0nRvYSNpVFBCeQ3pJcbFeDAXLKQodQZzfLrQZ3lmccCWxvTMzhAiiaj9ybOFLptzWzpB3fmtid/XjRECfhJDreRdirntmnuuvscKOEl2jvDIxfnH9l2xPjHtVkp+xAE6u0PT4jJkFSN45ZaUhXx5+mN7XlGMGQTpXV0thtzbW1ty3cQgQk7pXrx4Q4Z23Gex
54.38.94.65 ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHAyNTYAAAAIbmlzdHAyNTYAAABBBKqxcbMBcJwt9R6Kb1d4bZwRqqPJJt478Vp52ocA2GpNSfw57MMdd/uV0X1CeFkcDUbu9R6viUN03+XIU3ArDBQ=
54.38.94.65 ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAICr2Qt3FnYcg6IxAdSJ2jHjrYUZPeYOSsPNs4r9hy5w3
+github.com ssh-rsa AAAAB3NzaC1yc2EAAAABIwAAAQEAq2A7hRGmdnm9tUDbO9IDSwBK6TbQa+PXYPCPy6rbTrTtw7PHkccKrpp0yVhp5HdEIcKr6pLlVDBfOLX9QUsyCOV0wzfjIJNlGEYsdlLJizHhbn2mUjvSAHQqZETYP81eFzLQNnPHt4EVVUh7VfDESU84KezmD5QlWpXLmvU31/yMf+Se8xhHTvKSCZIFImWwoG6mbUoWf9nzpIoaSjB+weqqUUmpaaasXVal72J+UX2B+2RPW3RcT0eOzQgqlJL3RKrTJvdsjE3JEAvGq3lGHSZXy28G3skua2SmVi/w4yCE6gbODqnTWlg7+wC604ydGXA8VJiS5ap43JXiUFFAaQ==
+github.com ecdsa-sha2-nistp256 AAAAE2VjZHNhLXNoYTItbmlzdHAyNTYAAAAIbmlzdHAyNTYAAABBBEmKSENjQEezOmxkZMy7opKgwFB9nkt5YRrYMjNuG5N87uRgg6CLrbo5wAdT/y6v0mKV0U2w0WZ2YB/++Tpockg=
+github.com ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIOMqqnkVzrm0SdG6UOoqKLsabgH5C9okWi0dh2l9GKJl
diff --git a/nix/frama-c-public/publish-opam.sh b/nix/frama-c-public/publish-opam.sh
new file mode 100755
index 0000000000000000000000000000000000000000..eddc6fa6f2b2ef5622efcd9781b182577e10041b
--- /dev/null
+++ b/nix/frama-c-public/publish-opam.sh
@@ -0,0 +1,112 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Note:
+#
+# While this script can be run locally, it is meant to run in the Frama-C CI.
+# Thus, it expects to be run from the root of the Frama-C directory and that
+# some CI artifacts are available. Namely:
+# - the 'opam-repository' as generated by the script Frama-C/dev/build-release.sh
+# Availability of the files is NOT checked when the script starts.
+# The script:
+# - clones the 'Frama-C/opam-repository' as 'pub-opam-repository'
+# - creates a remote on the 'opam/opam-repository' named 'opam'
+# - creates a branch based on 'opam/master'
+# - copies the content of 'opam-repository' to 'pub-opam-repository'
+# - commits the changes
+# - pushes the branch
+
+##########################################################################
+
+OCAML_OPAM_GIT="git@github.com:ocaml/opam-repository.git"
+PUB_OPAM_GIT="git@github.com:Frama-C/opam-repository.git"
+PUB_OPAM_DIR="pub-opam-repository"
+SRC_OPAM_DIR="opam-repository"
+
+VERSION="$(cat VERSION)"
+CODENAME="$(cat VERSION_CODENAME)"
+
+BRANCH="frama-c.$VERSION"
+
+if ! git clone $PUB_OPAM_GIT $PUB_OPAM_DIR
+then
+ echo "Failed to clone website directory"
+ exit 128
+fi
+
+GIT="git -C $PUB_OPAM_DIR"
+$GIT remote add opam $OCAML_OPAM_GIT
+
+$GIT config user.name "Frama-CI Bot"
+$GIT config user.email "frama-ci-bot@frama-c.com"
+
+function fetch_opam {
+ $GIT fetch opam
+ if [ "$?" -ne "0" ]; then
+ echo "Can't fetch from ocaml opam repository"
+ exit 128
+ fi
+}
+
+function checkout {
+ if git ls-remote --quiet --exit-code $PUB_OPAM_GIT $BRANCH
+ then
+ $GIT checkout $BRANCH
+ else
+ $GIT checkout -b $BRANCH opam/master --no-track
+ fi
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to checkout branch '$BRANCH', aborting"
+ exit 128
+ fi
+}
+
+function commit {
+ $GIT commit -m "Frama-C: new release ($VERSION-$CODENAME)"
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to commit on branch"
+ exit 128
+ fi
+}
+
+function push {
+ if git ls-remote --quiet --exit-code $PUB_OPAM_GIT $BRANCH
+ then
+ $GIT push
+ else
+ $GIT push --set-upstream origin $BRANCH
+ fi
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to push branch"
+ exit 128
+ fi
+}
+
+fetch_opam
+checkout
+
+cp -r $SRC_OPAM_DIR/* $PUB_OPAM_DIR
+$GIT add -A
+
+commit
+push
diff --git a/nix/frama-c-public/publish-release.sh b/nix/frama-c-public/publish-release.sh
new file mode 100755
index 0000000000000000000000000000000000000000..de2d8dfee701b76b96547325487d46362ac7b00c
--- /dev/null
+++ b/nix/frama-c-public/publish-release.sh
@@ -0,0 +1,47 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Note:
+#
+# While this script can be run locally, it is meant to run in the Frama-C CI.
+# Thus, it expects to be run from the root of the Frama-C directory and that
+# some CI artifacts are available. Namely:
+# - 'release-data.json' as generated by the script Frama-C/dev/build-release.sh
+# - the 'FRAMA_CI_BOT_RELEASE_TOKEN' variable
+# - the stable branch must be available on 'pub/frama-c'
+# Availability of the file is NOT checked when the script starts.
+
+##########################################################################
+
+TAG="$(git describe --tag)"
+
+if [[ $TAG =~ .*-beta$ ]] ; then
+ git push "git@git.frama-c.com:pub/frama-c.git" "$TAG"
+else
+ curl \
+ --header 'Content-Type: application/json' \
+ --header "PRIVATE-TOKEN:$FRAMA_CI_BOT_RELEASE_TOKEN" \
+ --data-binary "@release-data.json" \
+ --request POST \
+ "https://git.frama-c.com/api/v4/projects/780/releases"
+fi
diff --git a/nix/frama-c-public/publish-website.sh b/nix/frama-c-public/publish-website.sh
new file mode 100755
index 0000000000000000000000000000000000000000..42169aaa98d3c574686876cb0a7b12d6a2b7e4f7
--- /dev/null
+++ b/nix/frama-c-public/publish-website.sh
@@ -0,0 +1,118 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Note:
+#
+# While this script can be run locally, it is meant to run in the Frama-C CI.
+# Thus, it expects to be run from the root of the Frama-C directory and that
+# some CI artifacts are available. Namely:
+# - the 'website' as generated by the script Frama-C/dev/build-release.sh
+# Availability of the files is NOT checked when the script starts.
+# The following variables are used in the cloned website:
+# - GITLAB_USER_NAME (who triggered the job)
+# - GITLAB_USER_EMAIL
+# - GITLAB_USER_LOGIN
+# - GITLAB_USER_ID
+# The script:
+# - clones the website as 'pub-website'
+# - checkout 'stable/release/<VERSION>-<LOWER CODENAME>'
+# if the branch does not exist in the repo, it is created
+# - copies the content of 'website' to 'pub-website'
+# - commits the changes
+# - pushes the branch
+# if the branch does not exist in the repo, a MR is created
+
+##########################################################################
+
+PUB_WEBSITE_GIT="git@git.frama-c.com:pub/pub.frama-c.com.git"
+PUB_WEBSITE_DIR="pub-website"
+SRC_WEBSITE_DIR="website"
+
+VERSION="$(cat VERSION)"
+CODENAME="$(cat VERSION_CODENAME)"
+LOWER_CODENAME="$(echo "$CODENAME" | tr '[:upper:]' '[:lower:]')"
+
+BRANCH="release/$VERSION-$LOWER_CODENAME"
+
+if ! git clone $PUB_WEBSITE_GIT $PUB_WEBSITE_DIR
+then
+ echo "Failed to clone website directory"
+ exit 128
+fi
+
+GIT="git -C $PUB_WEBSITE_DIR"
+
+$GIT config user.name "Frama-CI Bot"
+$GIT config user.email "frama-ci-bot@frama-c.com"
+
+function checkout {
+ if git ls-remote --quiet --exit-code $PUB_WEBSITE_GIT $BRANCH
+ then
+ $GIT checkout $BRANCH
+ else
+ $GIT checkout -b $BRANCH
+ fi
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to checkout branch '$BRANCH', aborting"
+ exit 128
+ fi
+}
+
+function commit {
+ $GIT commit -F- <<EOF
+[release] prepare $VERSION-$LOWER_CODENAME
+
+On behalf of "$GITLAB_USER_NAME" <$GITLAB_USER_EMAIL> (@$GITLAB_USER_LOGIN)
+EOF
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to commit on branch"
+ exit 128
+ fi
+}
+
+function push {
+ if git ls-remote --quiet --exit-code $PUB_WEBSITE_GIT $BRANCH
+ then
+ $GIT push
+ else
+ $GIT push \
+ --set-upstream origin $BRANCH \
+ -o merge_request.create \
+ -o merge_request.title="Release $VERSION-$CODENAME" \
+ -o merge_request.assign="$GITLAB_USER_ID"\
+ -o merge_request.draft \
+ -o ci.skip
+ fi
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to push branch"
+ exit 128
+ fi
+}
+
+checkout
+
+cp -r $SRC_WEBSITE_DIR/* $PUB_WEBSITE_DIR
+$GIT add -A
+
+commit
+push
diff --git a/nix/frama-c-public/publish-wiki.sh b/nix/frama-c-public/publish-wiki.sh
new file mode 100755
index 0000000000000000000000000000000000000000..c43eaa07300c545459c59b6831d4e098ebd1f750
--- /dev/null
+++ b/nix/frama-c-public/publish-wiki.sh
@@ -0,0 +1,97 @@
+#! /usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Note:
+#
+# While this script can be run locally, it is meant to run in the Frama-C CI.
+# Thus, it expects to be run from the root of the Frama-C directory and that
+# some CI artifacts are available. Namely:
+# - the 'wiki' as generated by the script Frama-C/dev/build-release.sh
+# Availability of the files is NOT checked when the script starts.
+# The following variables are used in the cloned wiki:
+# - GITLAB_USER_NAME (who triggered the job)
+# - GITLAB_USER_EMAIL
+# - GITLAB_USER_LOGIN
+# The script:
+# - clones the wiki as 'pub-wiki'
+# - copies the content of 'wiki' to 'pub-wiki'
+# - commits the changes
+# - pushes
+
+##########################################################################
+
+PUB_WIKI_GIT="git@git.frama-c.com:pub/frama-c.wiki.git"
+PUB_WIKI_DIR="pub-wiki"
+SRC_WIKI_DIR="wiki"
+
+VERSION="$(cat VERSION)"
+CODENAME="$(cat VERSION_CODENAME)"
+LOWER_CODENAME="$(echo "$CODENAME" | tr '[:upper:]' '[:lower:]')"
+
+if ! git clone $PUB_WIKI_GIT pub-wiki
+then
+ echo "Failed to clone wiki directory"
+ exit 128
+fi
+
+GIT="git -C $PUB_WIKI_DIR"
+
+$GIT config user.name "Frama-CI Bot"
+$GIT config user.email "frama-ci-bot@frama-c.com"
+
+function checkout {
+ $GIT checkout master
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to checkout branch 'master', aborting"
+ exit 128
+ fi
+}
+
+
+function commit {
+ $GIT commit -F- <<EOF
+[release] prepare $VERSION-$LOWER_CODENAME
+
+On behalf of "$GITLAB_USER_NAME" <$GITLAB_USER_EMAIL> (@$GITLAB_USER_LOGIN)
+EOF
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to commit on branch"
+ exit 128
+ fi
+}
+
+function push {
+ $GIT push
+ if [ "$?" -ne "0" ]; then
+ echo "Failed to push branch"
+ exit 128
+ fi
+}
+
+checkout
+
+cp -r $SRC_WIKI_DIR/* $PUB_WIKI_DIR
+$GIT add -A
+
+commit
+push
diff --git a/nix/manuals.nix b/nix/manuals.nix
index 1b9cb776c261c89e40cf1224a71a20ef96b99966..30bdbd93afd69a11f16babfe9805cca8a0ecb5c2 100644
--- a/nix/manuals.nix
+++ b/nix/manuals.nix
@@ -43,12 +43,13 @@ stdenv.mkDerivation rec {
'';
buildPhase = ''
- make -C doc NO_SUFFIX=yes all
+ make -C doc NO_SUFFIX=yes all version
'';
installPhase = ''
mkdir -p $out
cp ./doc/manuals/*.pdf $out
- cp ./doc/manuals/*.tgz $out
+ cp ./doc/manuals/*.tar.gz $out
+ cp ./doc/manuals/*.txt $out
'';
}