[CI] Add snap package

.github/workflows/snap.yml

@@ -0,0 +1,112 @@
+# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions
+# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners
+# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob
+
+name: Snap package
+
+###############################################################################
+# Schedule:
+# - push on any branch whose name matches v** or master
+# - any pull request
+# - once a day
+# - manually with parameters (see also github_actions/run_snap.sh)
+###############################################################################
+on:
+  push:
+    branches:
+      - v**
+      - master
+  pull_request:
+    branches:
+      - '**'
+  schedule:
+    - cron: '0 0 * * *'
+  workflow_dispatch:
+    inputs:
+      save:
+        description: 'Save artifact for download'
+        default: false
+      upload:
+        description: 'Upload artifact to snap store'
+        default: false
+      platform:
+        description: 'Arguments for the platform script'
+        required: true
+        default: '-extent=f -parallel=p -jobs=2 -vst=y -compcert=f'
+
+###############################################################################
+# Platform script options shared among all jobs
+#
+# Default values when the job is run automatically
+###############################################################################
+env:
+  COQREGTESTING: y
+  PLATFORM: -extent=i -parallel=p -jobs=2
+  SAVE_ARTIFACT: true
+
+jobs:
+###############################################################################
+# Snap
+#
+# CAVEATS:
+# - bubblewrap does not work inside lxd (used by snap)
+# - uploading requires a secret in GH https://github.com/snapcore/action-publish
+###############################################################################
+
+  Ubuntu_snap:
+    name: Snap package
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Git checkout
+        uses: actions/checkout@v2
+
+      - name: Set PLATFORM
+        if: ${{ github.event.inputs.platform != '' }}
+        run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV
+
+      - name: Set SAVE_ARTIFACT
+        if: ${{ github.event.inputs.save != '' }}
+        run: echo "SAVE_ARTIFACT=${{ github.event.inputs.save }}" >> $GITHUB_ENV
+
+      - name: Install opam
+        env:
+          OPAM_VERSION: 2.0.7
+        run: |
+          curl -L https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-linux > opam.${OPAM_VERSION}
+          chmod a+x opam.${OPAM_VERSION}
+          sudo cp opam.${OPAM_VERSION} /usr/local/bin/opam.${OPAM_VERSION}
+          sudo ln -s /usr/local/bin/opam.${OPAM_VERSION} /usr/local/bin/opam
+          opam init --bare --disable-sandboxing -y
+          opam switch create default --empty -y
+          opam repo add coq-released https://coq.inria.fr/opam/released
+          opam repo add coq-dev https://coq.inria.fr/opam/core-dev
+          opam repo add coq-extra https://coq.inria.fr/opam/extra-dev
+          opam repo add coq-platform file://$PWD/opam
+          opam repo set-repos coq-platform coq-released coq-dev coq-extra default
+          opam update
+
+      - name: Generate snapcraft file
+        run: linux/create_linux_installer.sh $PLATFORM
+
+      - name: Print snapcraft file
+        run: cat snap/snapcraft.yaml
+
+      - name: Run snapcraft
+        uses: snapcore/action-build@v1
+        id: build
+
+      - name: Save Artifact
+        if: ${{ env.SAVE_ARTIFACT }}
+        uses: actions/upload-artifact@v2
+        with:
+          name: 'Snap package'
+          path: ${{ steps.build.outputs.snap }}
+
+      - name: Upload Artifact to the Snap store
+        if: ${{ github.event.inputs.upload }}
+        uses: snapcore/action-publish@v1
+        with:
+          store_login: ${{ secrets.STORE_LOGIN }}
+          snap: ${{ steps.build.outputs.snap }}
+          release: edge

linux/create_linux_installer.sh

@@ -0,0 +1,57 @@
+#!/bin/bash
+
+# This script creates a Linux installer based on snap
+cd "$(dirname "$0")/.."
+source shell_scripts/init_safety_debug.sh
+source shell_scripts/init_paths.sh
+source shell_scripts/init_utilities.sh
+source coq_platform_switch_name.sh
+source shell_scripts/parse_cmdline_arguments.sh
+source shell_scripts/ask_introduction.sh
+source coq_platform_packages.sh
+
+# Snap versions cannot contain . nor +
+COQ_VERSION=${COQ_PLATFORM_VERSION//[.+]/-}
+
+# Description of the snap
+COQ_DESCRIPTION=`mktemp`
+cat > $COQ_DESCRIPTION <<EOT
+  The Coq interactive prover provides a formal language to write
+  mathematical definitions, executable algorithms, and theorems, together
+  with an environment for semi-interactive development of machine-checked
+  proofs.
+
+  This snap contains the Coq prover version $COQ_PLATFORM_VERSION
+  along with CoqIDE and the following packages:
+EOT
+
+for p in $(echo ${PACKAGES} | sed -e 's/ /\n/g' | sort); do
+  pname=`echo $p | sed 's/\..*//'`
+  if [ "${pname##coq-}" == "$pname" ]; then continue; fi
+  pversion="$(opam show $p -f version: | tr -d \")"
+  plicense="$(opam show $p -f license: | tr -d \")"
+  pdescr="$(opam show $p -f synopsis: | tr -d \")"
+  printf "  * **%s**: %s (version: %s, license: %s)\n" ${pname##coq-} "$pdescr" "$pversion" "$plicense" >> $COQ_DESCRIPTION
+done
+
+mkdir -p snap/
+
+sed \
+   -e "s/@@COQ_VERSION@@/$COQ_VERSION/g" \
+   -e "s/@@PLATFORM_ARGS@@/$*/g" \
+   -e "/@@COQ_DESCRIPTION@@/r $COQ_DESCRIPTION" -e "/@@COQ_DESCRIPTION@@/d" \
+   linux/snap/snapcraft.yaml.in > snap/snapcraft.yaml
+
+echo "INFO: filled in snap/snapcraft.yaml"
+
+mkdir -p snap/gui/
+
+sed \
+   -e "s/@@COQ_VERSION@@/$COQ_VERSION/g" \
+   linux/snap/coqide.desktop.in > snap/gui/coqide.desktop
+
+echo "INFO: filled in snap/gui/coqide.desktop"
+
+echo -e "Done, now run:\n\tsnapcraft snap"
+
+rm -f $COQ_DESCRIPTION

linux/snap/README.md

@@ -0,0 +1,59 @@
+Snap package for Coq
+====================
+
+URL: https://snapcraft.io/coq-prover
+
+Maintainer: Enrico Tassi
+
+Package name
+------------
+The name of the package is `coq-prover` since `coq` was considered
+unacceptable by the snap store admins (too short and non informative).
+
+Aliases
+-------
+The snap package can install binaries in the path, but they are all called
+`coq-prover.something` and `something` cannot contain `_`.
+
+As per [request](https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925)
+Coq is granted the `coqide -> coq-prover.coqide` and
+`coq_makefile -> coq-prover.coq-makefile` aliases (shorthands generated
+on the fly).
+
+Channels and updates
+--------------------
+Each package is available on a channel, which is a combination of track and
+risk level.
+A track is something like `latest` (the default one) or, `major-version` (as
+many packages do).
+A risk level is something like `stable`, `beta`, `edge`.
+
+By default users install from `latest/stable`.
+The CI script uploads to `latest/edge`, then via a web ui the package
+maintainer can promote a package from one level to another.
+
+IMPORTANT: snap packages are *automatically* updated. This means that when *we*
+make a new release the package installed by a user *silently* upgrades, no
+questions asked!
+
+A user can install from `latest/edge` to test the very last upload, but also,
+and more interestingly, from `8.13/stable` to *never* move to Coq 8.14 without
+consent. This last option makes snap package also usable by developers (and
+indeed one finds stuff like `node` or `go` distributed via snap).
+
+CAVEAT: track's creation need to be explicitly requested. The store admins are
+happy to grant quickly a new track if it follows the same schema of an existing
+one. TODO: I did not ask yet for the `8.13` track.
+
+See also
+--------
+- linux/snap/github_actions for a script to trigger a CI build for a platform
+  branch also uploading to the snap store
+
+Snap doc
+--------
+
+- Channels
+  https://snapcraft.io/docs/channels
+- Process for manual store actions (tracks, aliases)
+  https://forum.snapcraft.io/t/process-for-aliases-auto-connections-and-tracks/455

linux/snap/coq_wrapper

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# This shell scripts uses the path of the scipt itself to
+# set the COQBIN directory
+
+export COQBIN="$(cd $(dirname $0); pwd)"
+export COQLIB="$(cd $(dirname $0)/../lib/coq/; pwd)"
+
+THIS="$(basename $0)"
+SELF="${THIS##coq_wrapper_}"
+
+if [ "$SELF" == "coq_makefile" ]; then
+  exec $(dirname $0)/$SELF COQBIN = "$COQBIN/" "$@"
+else
+  exec $(dirname $0)/$SELF "$@"
+fi

linux/snap/coq_wrapper_coq_makefile

@@ -0,0 +1 @@
+coq_wrapper

linux/snap/coq_wrapper_coqc

@@ -0,0 +1 @@
+coq_wrapper

linux/snap/coq_wrapper_coqide

@@ -0,0 +1 @@
+coq_wrapper

linux/snap/coq_wrapper_coqidetop.opt

@@ -0,0 +1 @@
+coq_wrapper

linux/snap/coq_wrapper_coqtop

@@ -0,0 +1 @@
+coq_wrapper

linux/snap/coqide.desktop.in

@@ -0,0 +1,6 @@
+[Desktop Entry]
+Name=CoqIDE
+Exec=${SNAP}/coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coqide %F
+Icon=${SNAP}/coq-platform/@@COQ_VERSION@@/share/coq/coq.png
+Type=Application
+MimeType=text/x-verilog

linux/snap/github_actions/README.md

@@ -0,0 +1,20 @@
+## Build the snap package for the full platform
+
+The web UI only lets you do this for the default branch, in order to run the
+`snap.yml` workflow on another branch (a git ref really) you can use the
+`./github_actions/run_snap.sh`.
+
+First of all you need to generate (once and forall) a token from
+https://github.com/settings/tokens (tick the "workflow" box).
+
+Then:
+```shell
+export GHTOKEN=6NDVjMDhmZDAwMGZ...
+export GHUSER=gares
+export BRANCH=v8.13
+export PLATFORM="-extent=f -parallel=p -jobs=2 -vst=y -compcert=f"
+export SAVE=true
+export UPLOAD=false
+./github_actions/run_snap.sh
+```
+The shell script prints a `curl` invocation you have to run (after inspection).

linux/snap/github_actions/run_snap.sh

@@ -0,0 +1,17 @@
+#!/bin/bash
+
+[ -z "$GHUSER"   ] && echo "please set GHUSER to your github user" && exit 1
+[ -z "$GHTOKEN"  ] && echo "please set GHTOKEN to your github access token (generate one here: https://github.com/settings/tokens)" && exit 1
+[ -z "$BRANCH"   ] && echo "please set BRANCH to the branch to build" && exit 1
+[ -z "$PLATFORM" ] && echo "please set PLATFORM to the arguments for the script, eg \"-extent=f -parallel=p -jobs=2 -vst=y -compcert=f\"" && exit 1
+[ -z "$SAVE"     ] && echo "INFO: set SAVE to true to save the artifact (default false)" && SAVE=false
+[ -z "$UPLOAD"   ] && echo "INFO: set UPLOAD to true to upload to the snap store (default false)" && UPLOAD=false
+
+function go {
+  local obj=$(printf '{ "ref": "%s", "inputs": { "save" : "%s", "upload" : "%s", "platform" : "%s" } }' "$BRANCH" "$SAVE" "$UPLOAD" "$PLATFORM")
+  echo curl -u $GHUSER:\$GHTOKEN -X POST \
+    https://api.github.com/repos/coq/platform/actions/workflows/snap.yml/dispatches -d $(printf "'%s'" "$obj")
+}
+
+echo "Run this:"
+echo $(go)

linux/snap/snapcraft.yaml.in

@@ -0,0 +1,60 @@
+name: coq-prover
+base: core18
+version: '@@COQ_VERSION@@'
+summary: Coq
+description: |
+  @@COQ_DESCRIPTION@@
+
+grade: stable
+confinement: strict
+
+parts:
+  coq:
+    plugin: nil
+    build-packages: [build-essential, curl, m4, unzip, git]
+    source: .
+    source-type: local
+    override-build: |
+      if [ -d $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/ ]; then exit 0; fi
+      # build
+      echo "COQ_PLATFORM_VERSION=@@COQ_VERSION@@" >> coq_platform_switch_name.sh
+      echo "COQ_PLATFORM_SWITCH_NAME=@@COQ_VERSION@@" >> coq_platform_switch_name.sh
+      COQREGTESTING=y OPAMROOT=$SNAPCRAFT_PART_INSTALL/coq-platform/ ./coq_platform_make.sh @@PLATFORM_ARGS@@
+      # cleanup
+      OPAMROOT=$SNAPCRAFT_PART_INSTALL/coq-platform/ opam clean
+      find $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/ \( -name '*.byte.exe' -o -name '*.byte' -o -name '*.cm[aioxt]' -o -name '*.cmxa' -o -name '*.[oa]' -o -name '*.cmti' -o -name '*.glob' \) -type f  -delete
+      find $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/bin/ -maxdepth 1 -mindepth 1 \! -name 'coq*' -exec rm -f {} \;
+      find $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/lib/ -maxdepth 1 -mindepth 1 \! \( -name 'coq' -o -name 'stublibs' \) -exec rm -rf {} \;
+      rm -rf $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/share/ocaml-secondary-compiler
+      rm -rf $SNAPCRAFT_PART_INSTALL/coq-platform/repo/
+
+  wrapper:
+    plugin: nil
+    after: [coq]
+    source: .
+    source-type: local
+    override-build: |
+      # install wrapper for apps
+      mkdir -p $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/bin/
+      cp linux/snap/coq_wrapper_* $SNAPCRAFT_PART_INSTALL/coq-platform/@@COQ_VERSION@@/bin/
+
+apps:
+  coqide:
+    command: coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coqide
+    plugs: [desktop, home]
+    extensions: [gnome-3-28]
+    desktop: ../project/snap/gui/coqide.desktop
+  coqtop:
+    plugs: [home]
+    command: coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coqtop
+  coqc:
+    plugs: [home]
+    command: coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coqc
+  coq-makefile:
+    plugs: [home]
+    command: coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coq_makefile
+  coqidetop:
+    plugs: [home]
+    command: coq-platform/@@COQ_VERSION@@/bin/coq_wrapper_coqidetop.opt
+
+