diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 0000000..223774c --- /dev/null +++ b/.dockerignore @@ -0,0 +1,5 @@ +* +!LICENSE +!README.md +!entrypoint.sh +!timegroup.sh \ No newline at end of file diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..6d8126d --- /dev/null +++ b/.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 diff --git a/Dockerfile b/Dockerfile index d0b970a..9bcc77c 100644 --- a/Dockerfile +++ b/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"] diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..b996032 --- /dev/null +++ b/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 + diff --git a/README.md b/README.md index 2bb3ab1..3cb86fa 100644 --- a/README.md +++ b/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 diff --git a/action.yml b/action.yml index bdebf96..557e306 100644 --- a/action.yml +++ b/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' diff --git a/entrypoint.sh b/entrypoint.sh index 393834a..3894cd5 100755 --- a/entrypoint.sh +++ b/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" diff --git a/helper.sh b/helper.sh new file mode 100755 index 0000000..d8f905f --- /dev/null +++ b/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 </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 +}