diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b7b53e3b94feb8875fb31f3d5452b9318ecc74e1..bf357ad0ef75d1adf2851ddc3c0b42e067ec85cb 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -59,20 +59,26 @@ variables: .build_template: &ivette_setup image: "ocaml/opam:ubuntu-lts-ocaml-$OCAML" before_script: + # Prepare - sudo apt update + # TS - sudo apt install -y xvfb curl unzip libnss3 libasound2-plugins - sudo curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.7/install.sh | bash - export NVM_DIR="$HOME/.nvm" - - '[ -s "$NVM_DIR/nvm.sh" ] && \. "$NVM_DIR/nvm.sh"' - - '[ -s "$NVM_DIR/bash_completion" ] && \. "$NVM_DIR/bash_completion"' + - . "$NVM_DIR/nvm.sh" - nvm install $NODE - nvm use node $NODE - corepack enable + # Opam + - opam switch create --empty . + - eval $(opam env --switch=. --set-switch) - opam pin . -n -k path - opam depext frama-c - opam install headache - opam install --jobs 2 --deps-only . + # Build Frama-C API - dune build -j2 @install + - make -C ivette api ################################################################################ ### PREPARE @@ -155,7 +161,6 @@ ivette: stage: build <<: *ivette_setup script: - - make -C ivette api - make -C ivette dist tags: - docker @@ -235,7 +240,6 @@ ivette-tests: when: manual <<: *ivette_setup script: - - make -C ivette api - make -C ivette dist - cd ivette - xvfb-run --auto-servernum -e /dev/stdout -s "-screen 0 1920x1080x24 -ac -nolisten tcp -nolisten unix" dune exec -- yarn playwright test --headed @@ -311,6 +315,49 @@ build-distrib-tarball: - ./*.tar.gz expire_in: 1 week +# Build ivette apps + +build-ivette-linux-packages: + stage: distrib + <<: *ivette_setup + script: + - make -C ivette dist-linux + - mv ivette/dist/Ivette-arm64.AppImage ./frama-c-ivette-linux-ARM64.AppImage + - mv ivette/dist/Ivette-x86_64.AppImage ./frama-c-ivette-linux-x86-64.AppImage + artifacts: + paths: + - ./*.AppImage + tags: + - docker + <<: *when_release + +build-ivette-macos-packages: + stage: distrib + script: + # TS + - export NVM_DIR="$HOME/.nvm" + - . "$NVM_DIR/nvm.sh" + - nvm install $NODE + - nvm use $NODE + # Opam + - opam switch create --empty . + - eval $(opam env --switch=. --set-switch) + - opam pin . -n -k path + - opam install headache -y + - opam install --jobs 2 --deps-only . -y + # Build Frama-C API + - dune build -j2 @install + - make -C ivette api + # Build Ivette + - make -C ivette dist-macOS + - mv ivette/dist/Ivette-universal.dmg ./frama-c-ivette-macos-universal.dmg + artifacts: + paths: + - ./*.dmg + tags: + - macos-arm + <<: *when_release + # Coverage coverage: @@ -385,6 +432,8 @@ release-content: needs: - api-doc - build-distrib-tarball + - build-ivette-linux-packages + - build-ivette-macos-packages - manuals-for-release artifacts: paths: diff --git a/INSTALL.md b/INSTALL.md index 00d02d123e0b4a40bcae96238ddba3cea7607dae..16d022cae5d886fb2b9282eeb4bd2d2b349aeed0 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -8,6 +8,9 @@ - [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c) - [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl) - [Installing Frama-C on macOS](#installing-frama-c-on-macos) + - [Installing Ivette via the online packages](#installing-ivette-via-the-online-packages) + - [On Linux](#installing-ivette-via-the-online-packages-on-linux) + - [On macOS](#installing-ivette-via-the-online-packages-on-macos) - [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora) - [Compiling from source](#compiling-from-source) - [Quick Start](#quick-start) @@ -300,6 +303,52 @@ We highly recommend to rely on it for the installation of Frama-C. Instructions on installing and running it are presented by opam when the `frama-c` package is installed. Follow them to get Ivette running. +## Installing Ivette via the online packages + +**Warning:** if you already have an `ivette` script along with `frama-c`, that +script is used for bootstrapping the installation of Ivette from source through +your internet connection. The instructions provided here are intended to +_replace_ the installation procedure from source. Hence, it is highly +recommended for you to remove the bootstrapping `ivette` script if you want to +use the binary distribution of Ivette. + +Only stable distributions are available online for now. +Download the Ivette distribution that corresponds to your version of Frama-C. + +### Installing Ivette via the online packages on Linux + +Requirement: libfuse2 must be installed. + +Download the binary distribution (for now, only x86-64 and ARM64 are supported). +Install it wherever you want: + +```sh +cp frama-c-ivette-linux-<arch>-<version>.AppImage <IVETTE-INSTALL-PATH>/ivette.AppImage +``` + +Then add an alias `ivette` that just runs the AppImage: + +```sh +alias ivette=<ABSOLUTE-IVETTE-INSTALL-PATH>/ivette.AppImage +``` + +### Installing Ivette via the online packages on macOS + +Download the universal binary distribution of Ivette and install it, typically +in `/Applications/Ivette.app`. To launch Ivette from the command line, you will +need your own `ivette` script, like the following one: + +```sh +#! /usr/bin/env sh +exec open -na <IVETTE-INSTALL>/Ivette.app --args\ + --command <FRAMAC-INSTALL>/frama-c\ + --working $PWD $* +``` + +Simply replace `<IVETTE-INSTALL>` and `<FRAMAC-INSTALL>` in the code above with +the (absolute) paths to your `Ivette.app` and `frama-c` binaries, +respectively. Then, make your `ivette` script executable and simply use it like +the `frama-c` command-line binary! ## Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora) diff --git a/dev/build-release.sh b/dev/build-release.sh index 0434490bfdc3e2cac73718f107c789a86bbf2ece..06eb4980be5f2b5a49674d77a0c707e82484405e 100755 --- a/dev/build-release.sh +++ b/dev/build-release.sh @@ -27,6 +27,9 @@ # 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' +# - 'frama-c-ivette-linux-ARM64.AppImage' +# - 'frama-c-ivette-linux-x86-64.AppImage' +# - 'frama-c-ivette-macos-universal.dmg' # - 'api' directory (with api archives inside) # - 'manuals' directory (with all manuals incl. acsl + version text files) # Availability of the files is checked when the script starts. The script also @@ -160,6 +163,18 @@ for file in "${API_FILES[@]}"; do prepare_file "$API_DIR/$file-api.tar.gz" done +show_step "Searching for Ivette packages" + +IVETTE=( + "frama-c-ivette-linux-ARM64.AppImage" + "frama-c-ivette-linux-x86-64.AppImage" + "frama-c-ivette-macos-universal.dmg" +) + +for package in "${IVETTE[@]}"; do + prepare_file "$package" +done + show_step "Searching for manuals" MANUALS=( @@ -237,6 +252,12 @@ function copy_manual_e_acsl { cp "$MANUALS_DIR/$1.$2" "$EACSL_TARGET_DIR/$(version_name "$1").$2" } +function copy_ivette_package { + name="${1%%.*}" + ext="${1#*.}" + cp "$1" "$PKGS_TARGET_DIR/$(version_name "$name").$ext" +} + function copy_api { if [ "$FINAL_RELEASE" = "yes" ]; then cp "$API_DIR/$1-api.$2" "$MANS_TARGET_DIR/$1-api.$2" @@ -258,15 +279,18 @@ function copy_files { for api in "${API_FILES[@]}"; do copy_api "$api" "tar.gz" done + for package in "${IVETTE[@]}"; do + copy_ivette_package "$package" + done # Eva has an old manual name that might be in use: if [ "$FINAL_RELEASE" = "yes" ]; then cp "$MANS_TARGET_DIR/frama-c-eva-manual.pdf" "$MANS_TARGET_DIR/frama-c-value-analysis.pdf" fi - cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_VERSION" + cp $TARGZ_BASE "$PKGS_TARGET_DIR/$TARGZ_VERSION" if [ "$FINAL_RELEASE" = "yes" ]; then - cp $TARGZ_BASE "$GZ_TARGET_DIR/$TARGZ_GENERIC" + cp $TARGZ_BASE "$PKGS_TARGET_DIR/$TARGZ_GENERIC" fi } @@ -338,6 +362,13 @@ for archive in "${COMPANIONS[@]}"; do echo "- [$archive]($FRAMAC_COM_DOWNLOAD/$NAME.tar.gz)" >> $WIKI_PAGE done echo "" >> $WIKI_PAGE +echo "## Ivette packages" >> $WIKI_PAGE +for package in "${IVETTE[@]}"; do + NAME="${package%%.*}" + EXT="${package#*.}" + echo "- [$NAME]($FRAMAC_COM_DOWNLOAD/$(version_name $NAME).$EXT)" >> $WIKI_PAGE +done +echo "" >> $WIKI_PAGE echo "## Main changes" >> $WIKI_PAGE sed 's/\(\#.*\)/##\1/' $CHANGES >> $WIKI_PAGE @@ -371,6 +402,21 @@ cat >$JSON_DATA <<EOL "name": "Official source archive", "url": "https://frama-c.com/download/$TARGZ_VERSION", "link_type":"other" + }, + { + "name": "Ivette (Linux ARM64)", + "url": "https://frama-c.com/download/frama-c-ivette-linux-ARM64-$VERSION_AND_CODENAME.AppImage", + "link_type":"other" + }, + { + "name": "Ivette (Linux x86-64)", + "url": "https://frama-c.com/download/frama-c-ivette-linux-x86-64-$VERSION_AND_CODENAME.AppImage", + "link_type":"other" + }, + { + "name": "Ivette (macOS universal)", + "url": "https://frama-c.com/download/frama-c-ivette-macos-universal-$VERSION_AND_CODENAME.dmg", + "link_type":"other" } ] }, @@ -387,7 +433,6 @@ 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" @@ -398,31 +443,13 @@ mkdir -p $WEBSITE_DIR mkdir -p $WEBSITE_DL_DIR mkdir -p $WEBSITE_DL_DIR/e-acsl -GZ_TARGET_DIR=$WEBSITE_DL_DIR +PKGS_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="$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 @@ -469,6 +496,9 @@ else ACSL_OR_BETA="acsl: $ACSL_VERSION_WEBSITE" fi +INSTALL_WEBPAGE="https://git.frama-c.com/pub/frama-c/-/blob/$TAG/INSTALL.md" +IVETTE_INSTALL="$INSTALL_WEBPAGE#installing-ivette-via-the-online-packages-on-" + cat >$VERSION_WEBPAGE <<EOL --- layout: version @@ -483,7 +513,7 @@ releases: - name: Source distribution link: /download/$TARGZ_VERSION help: Compilation instructions - help_link: https://git.frama-c.com/pub/frama-c/-/blob/$TAG/INSTALL.md + help_link: $INSTALL_WEBPAGE - name: User manual link: /download/user-manual-$VERSION_AND_CODENAME.pdf - name: Plug-in development guide @@ -513,6 +543,20 @@ releases: link: /download/wp-manual-$VERSION_AND_CODENAME.pdf - name: E-ACSL manual link: /download/e-acsl/e-acsl-manual-$VERSION_AND_CODENAME.pdf + - name: Ivette Packages (experimental) + files: + - name: Linux x86-64 AppImage + link: /download/frama-c-ivette-linux-x86-64-$VERSION_AND_CODENAME.AppImage + help: Installation instructions + help_link: ${IVETTE_INSTALL}linux + - name: Linux ARM64 AppImage + link: /download/frama-c-ivette-linux-ARM64-$VERSION_AND_CODENAME.AppImage + help: Installation instructions + help_link: ${IVETTE_INSTALL}linux + - name: macOS universal + link: /download/frama-c-ivette-macOS-universal-$VERSION_AND_CODENAME.dmg + help: Installation instructions + help_link: ${IVETTE_INSTALL}macos --- EOL diff --git a/doc/release/deploy.tex b/doc/release/deploy.tex index 7a77fd1464ed1d55ffc12781321dbbddd07252c4..0b65e17fbe9206d959febc6c3f68d4b70ee0b74d 100644 --- a/doc/release/deploy.tex +++ b/doc/release/deploy.tex @@ -47,7 +47,7 @@ Once the pipeline for the website has run, open \texttt{https://pub.frama-c.com} \item \texttt{index.html} must display: \begin{itemize} \item the new event, - \item a link to the (beta) release at the bottom. + \item if it is beta a link to the beta next to "All versions". \end{itemize} \item \texttt{/fc-versions/<codename>.html}: \begin{itemize} diff --git a/doc/release/validation.tex b/doc/release/validation.tex index 758a75b3fc38f5e091d62b3a00251daadfbba299..98329d65dd16fae1c7885ef27071b4f605cc848a 100644 --- a/doc/release/validation.tex +++ b/doc/release/validation.tex @@ -120,35 +120,31 @@ They shall succeed. Collect the artifacts of the following targets: \begin{itemize} \item api-doc \item build-distrib-tarball + \item build-ivette-linux-packages + \item build-ivette-macos-packages \item manuals \end{itemize} \noindent Check that these artifacts are as expected. In particular: \begin{itemize} - \item API documentatation: + \item API documentation: \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 (note: unless - someone inadvertently added non-free code, \FramaC does not contain any, - this check is obsolete). - \item Check that no \texttt{/home/user} path can be found in the distribution, - \item Build and test - \begin{itemize} - \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} + \item Ivette packages + \begin{itemize} + \item check that the packages can be run on each system + \end{itemize} + \item Check versions in the manuals \end{itemize} \noindent Alternatively, you can use \texttt{docker} to compile the archive against a diff --git a/ivette/package.json b/ivette/package.json index 49e31360eb05a50046257c12cee821e16ea931f9..eef7a002a74584454b3ca6784498ddeb2089e26a 100644 --- a/ivette/package.json +++ b/ivette/package.json @@ -98,7 +98,7 @@ "appId": "com.framac.ivette", "compression": "store", "copyright": "Copyright © 2007-2024 Frama-C. All Rights Reserved.", - "artifactName": "${productName}-${arch}-${version}.${ext}", + "artifactName": "${productName}-${arch}.${ext}", "win": { "target": [ {