Support time-group feature

.dockerignore

@@ -0,0 +1,5 @@
+*
+!LICENSE
+!README.md
+!entrypoint.sh
+!timegroup.sh

.gitignore

@@ -0,0 +1,52 @@
+### Emacs ###
+# -*- mode: gitignore; -*-
+*~
+\#*\#
+/.emacs.desktop
+/.emacs.desktop.lock
+*.elc
+auto-save-list
+tramp
+.\#*
+
+# Org-mode
+.org-id-locations
+*_archive
+
+# flymake-mode
+*_flymake.*
+
+# eshell files
+/eshell/history
+/eshell/lastdir
+
+# elpa packages
+/elpa/
+
+# reftex files
+*.rel
+
+# AUCTeX auto folder
+/auto/
+
+# cask packages
+.cask/
+dist/
+
+# Flycheck
+flycheck_*.el
+
+# server auth directory
+/server/
+
+# projectiles files
+.projectile
+
+# directory configuration
+.dir-locals.el
+
+# network security
+/network-security.data
+
+### Misc ###
+min.sh

Dockerfile

@@ -1,7 +1,9 @@
 FROM docker:latest
 
-COPY LICENSE README.md /
+WORKDIR /app
 
-COPY entrypoint.sh /entrypoint.sh
+COPY LICENSE README.md ./
 
-ENTRYPOINT ["/entrypoint.sh"]
+COPY entrypoint.sh timegroup.sh ./
+
+ENTRYPOINT ["/app/entrypoint.sh"]

Makefile

@@ -0,0 +1,19 @@
+all: help
+
+help:
+	@echo "make help   # display this section"
+	@echo "make gen    # generate min.sh to be copied in entrypoint.sh"
+	@echo "make test   # test timegroup.sh - should print DONE without FAILURE"
+	@echo "make check  # analyze the scripts using shellcheck"
+
+gen:
+	./helper.sh gen
+
+test:
+	./helper.sh test
+
+check:
+	shellcheck timegroup.sh
+	shellcheck -x helper.sh
+	shellcheck -x entrypoint.sh
+

README.md

@@ -52,12 +52,20 @@ Among `"minimal"`, `"4.07-flambda"`, `"4.09-flambda"`.
 
 *Optional* The main script run in the container; may be overridden. Default:
 
-    opam config list; opam repo list; opam list
-    opam pin add -n -y -k path $PACKAGE .
-    opam update -y
-    opam install -y -v -j 2 $PACKAGE
-    opam list
-    opam remove $PACKAGE
+    startGroup Print opam config
+      opam config list; opam repo list; opam list
+    endGroup
+    startGroup Fetch dependencies
+      opam pin add -n -y -k path $PACKAGE .
+      opam update -y
+    endGroup
+    startGroup Build
+      opam install -y -v -j 2 $PACKAGE
+      opam list
+    endGroup
+    startGroup Uninstallation test
+      opam remove $PACKAGE
+    endGroup
 
 *Note: this option is named `custom-script` rather than `script` or
 `run` to discourage changing its recommended, default value, while

action.yml

@@ -14,12 +14,20 @@ inputs:
   custom_script:
     description: 'The main script run in the container; may be overridden.'
     default: |
-      opam config list; opam repo list; opam list
-      opam pin add -n -y -k path $PACKAGE .
-      opam update -y
-      opam install -y -v -j 2 $PACKAGE
-      opam list
-      opam remove $PACKAGE
+      startGroup Print opam config
+        opam config list; opam repo list; opam list
+      endGroup
+      startGroup Fetch dependencies
+        opam pin add -n -y -k path $PACKAGE .
+        opam update -y
+      endGroup
+      startGroup Build
+        opam install -y -v -j 2 $PACKAGE
+        opam list
+      endGroup
+      startGroup Uninstallation test
+        opam remove $PACKAGE
+      endGroup
 runs:
   using: 'docker'
   image: 'Dockerfile'

entrypoint.sh

@@ -3,6 +3,12 @@
 
 set -e
 
+timegroup_file="/app/timegroup.sh"
+# shellcheck source=./timegroup.sh
+. "$timegroup_file"
+
+startGroup Print runner configuration
+
 echo "GITHUB_WORKFLOW=$GITHUB_WORKFLOW"
 echo "RUNNER_OS=$RUNNER_OS"
 echo "RUNNER_TEMP=$RUNNER_TEMP"
@@ -16,6 +22,8 @@ echorun cat /proc/cpuinfo || true
 echorun cat /proc/meminfo || true
 echorun cat /etc/os-release || true
 
+endGroup
+
 ## Initial values
 PACKAGE=""
 _OPAM_FILE=""
@@ -110,9 +118,13 @@ elif [ "$_OCAML_VERSION" = '4.07-flambda' ]; then
 fi
 echo OCAML407="$OCAML407"
 
+startGroup Pull docker-coq image
+
 echo COQ_IMAGE="$COQ_IMAGE"
 docker pull "$COQ_IMAGE"
 
+endGroup
+
 # Assuming you used https://github.com/actions/checkout,
 # the GITHUB_WORKSPACE variable corresponds to the following host dir:
 # ${RUNNER_WORKSPACE}/${GITHUB_REPOSITORY#*/}, see also
@@ -121,17 +133,25 @@ docker pull "$COQ_IMAGE"
 HOST_WORKSPACE_REPO="${RUNNER_WORKSPACE}/${GITHUB_REPOSITORY#*/}"
 echo "HOST_WORKSPACE_REPO=$HOST_WORKSPACE_REPO"
 
-echorun pwd
-# should be /github/workspace
-echorun ls -hal
+# echorun pwd
+## should be /github/workspace
+# echorun ls -hal
+
+if [ "$OCAML407" = "true" ]; then
+    # shellcheck disable=SC2016
+    _OCAML407_COMMAND='startGroup Change opam switch; opam switch ${COMPILER_EDGE}; eval $(opam env); endGroup'
+else
+    _OCAML407_COMMAND=''
+fi
 
+## Note to docker-coq-action maintainers: Run ./helper.sh gen & Copy min.sh
 echo PACKAGE="$PACKAGE"
 docker run -i --init --rm --name=COQ -e PACKAGE="$PACKAGE" \
        -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \
        "$COQ_IMAGE" /bin/bash --login -c "
+endGroup () {  {  init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in  *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in  *x*) set -x ;; esac; } ; startGroup () {  {  init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in  *x*) set -x ;; esac; } # generated from helper.sh
 export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '; set -ex
-if [ $OCAML407 = true ]; then opam switch \${COMPILER_EDGE}; eval \$(opam env); fi
-pwd; ls -hal
+$_OCAML407_COMMAND
 $_SCRIPT" script
 
 echo "done"

helper.sh

@@ -0,0 +1,65 @@
+#!/bin/bash
+# -*- compile-command: "./helper.sh gen"; -*-
+# Author: Erik Martin-Dorel, 2020
+
+srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
+
+# shellcheck source=./timegroup.sh
+. "$srcdir/timegroup.sh"
+
+run_tests() {
+    set -e
+    if endGroup; then
+        echo "FAILURE: endGroup should raise an error"
+    else
+        echo "Error OK."
+    fi
+    startGroup
+    sleep 1s
+    # endGroup
+    startGroup This is a test
+    sleep 2s
+    endGroup
+    echo "DONE."
+}
+
+minimify() {
+    local escape="true"
+    # This function is intended to export a minimified version of the
+    # specified functions, developed in this file, then incorporated
+    # in entrypoint.sh
+    for fun; do
+        if [ "$escape" = "true" ]; then
+            type "$fun" | tail -n+2 | perl -pwe 'chomp; s/ +/ /g; s/}/; }/g; s/\$/\\\$/g; s/"/\\"/g'
+        else
+            type "$fun" | tail -n+2 | perl -pwe 'chomp; s/ +/ /g; s/}/; }/g'
+        fi
+    done
+}
+
+main_helper () {
+    local gen_file="min.sh"
+    if [ $# -eq 1 ] && [ "$1" = "test" ]; then
+        run_tests
+    elif [ $# -eq 1 ] && [ "$1" = "gen" ]; then
+        set -x
+        exec > "$gen_file"
+
+        minimify endGroup
+        echo -n ' ; '
+        minimify startGroup
+        echo ' # generated from helper.sh'
+    elif [ $# -eq 1 ] && [ "$1" = "--help" ]; then
+        cat <<EOF
+Usage:
+
+  $0 test
+    Run tests.
+
+  $0 gen
+    Generate '$gen_file'.
+EOF
+    fi
+}
+
+main_helper "$@"

timegroup.sh

@@ -0,0 +1,42 @@
+#!/bin/sh
+# Author: Erik Martin-Dorel, 2020
+
+endGroup() {
+    # This function unsets the env var 'startTime'.
+    { init_opts="$-"; set +x; } 2>/dev/null
+    # local endTime
+    if [ -n "$startTime" ]; then
+        # endTime=$(TZ=UTC+0 printf '%(%s)T\n' '-1')  # not POSIX
+        endTime=$(date -u +%s)
+        echo "::endgroup::"
+        # TZ=UTC-0 printf '↳ %(%-Hh %-Mm %-Ss)T\n' "$((endTime - startTime))"  # not POSIX
+        printf "↳ "; date -u -d "@$((endTime - startTime))" '+%-Hh %-Mm %-Ss'; echo
+        # Assume the time difference < 24h
+        unset startTime
+    else
+        echo 'Error: missing startGroup command.'
+        case "$init_opts" in *x*) set -x; esac
+        return 1
+    fi
+    case "$init_opts" in *x*) set -x; esac
+}
+
+startGroup() {
+    # This function sets the env var 'startTime'.
+    { init_opts="$-"; set +x; } 2>/dev/null
+    # Nesting groups is not supported; call 'endGroup' if need be.
+    if [ -n "$startTime" ]; then
+        endGroup
+    fi
+    # local groupTitle
+    if [ $# -ge 1 ]; then
+        groupTitle="$*"
+    else
+        groupTitle="Unnamed group"
+    fi
+    echo
+    echo "::group::$groupTitle"
+    # startTime=$(TZ=UTC-0 printf '%(%s)T\n' '-1')  # not POSIX
+    startTime=$(date -u +%s)
+    case "$init_opts" in *x*) set -x; esac
+}