From 720016f06aefebbd3e1e8d56f2f6f64ad0aa44de Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 20:41:43 +0100 Subject: [PATCH 01/10] chore: Add .gitignore href: https://www.gitignore.io/api/emacs --- .gitignore | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e67d36e --- /dev/null +++ b/.gitignore @@ -0,0 +1,49 @@ +### 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 From ebc888219081c1ee0d9355c9916bd912ca3f6f26 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 20:49:26 +0100 Subject: [PATCH 02/10] chore: Add whitelist .dockerignore --- .dockerignore | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 .dockerignore diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 0000000..c896642 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,4 @@ +* +!LICENSE +!README.md +!entrypoint.sh From ab9918245d07003e2a63f6a56ba90980d367ba90 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 20:46:17 +0100 Subject: [PATCH 03/10] feat: Implement startGroup/endGroup with time-difference feature MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * helper.sh is a sourceable Bash script & timegroup.sh a POSIX script References: * https://github.community/t5/GitHub-Actions/Has-github-action-somthing-like-travis-fold/m-p/37715 * https://stackoverflow.com/a/27442175/ Example usage: $ startGroup Startup phase $ … $ endGroup Example output: ::group::Startup phase … ::endgroup:: ↳0h 0m 2s --- .gitignore | 3 +++ helper.sh | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++ timegroup.sh | 42 ++++++++++++++++++++++++++++++++++ 3 files changed, 109 insertions(+) create mode 100755 helper.sh create mode 100755 timegroup.sh diff --git a/.gitignore b/.gitignore index e67d36e..6d8126d 100644 --- a/.gitignore +++ b/.gitignore @@ -47,3 +47,6 @@ flycheck_*.el # network security /network-security.data + +### Misc ### +min.sh diff --git a/helper.sh b/helper.sh new file mode 100755 index 0000000..91e2aff --- /dev/null +++ b/helper.sh @@ -0,0 +1,64 @@ +#!/bin/bash +# -*- compile-command: "./helper.sh gen"; -*- +# Author: Erik Martin-Dorel, 2020 + +srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd ) + +. "$srcdir/timegroup.sh" + +run_tests() { + set -e + if endGroup; then + echo "FAILURE: endGroup should raise an error" + else + : 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 < Date: Sat, 28 Mar 2020 21:53:44 +0100 Subject: [PATCH 04/10] feat: Copy timegroup.sh in the action image --- .dockerignore | 1 + Dockerfile | 8 +++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/.dockerignore b/.dockerignore index c896642..223774c 100644 --- a/.dockerignore +++ b/.dockerignore @@ -2,3 +2,4 @@ !LICENSE !README.md !entrypoint.sh +!timegroup.sh \ No newline at end of file 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"] From 5893da232742585e58e6ed66aee8289e3b7e7812 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 21:13:38 +0100 Subject: [PATCH 05/10] feat: Add minimified version of startGroup/endGroup in entrypoint.sh feat: Take advantage of timegroup.sh twice in entrypoint.sh $ ./helper.sh gen & Comment-out or Remove "pwd; ls -hal" --- entrypoint.sh | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/entrypoint.sh b/entrypoint.sh index 393834a..173328e 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -3,6 +3,10 @@ set -e +. /app/timegroup.sh + +startGroup Print runner configuration + echo "GITHUB_WORKFLOW=$GITHUB_WORKFLOW" echo "RUNNER_OS=$RUNNER_OS" echo "RUNNER_TEMP=$RUNNER_TEMP" @@ -16,6 +20,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 +116,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 +131,18 @@ 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 +## 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; 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; 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 $_SCRIPT" script echo "done" From b800cf762087cff84150b3663bfb2c0ed277f288 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 22:35:15 +0100 Subject: [PATCH 06/10] fix: Remove clutter by evaluating the if-then-else beforehand --- entrypoint.sh | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/entrypoint.sh b/entrypoint.sh index 173328e..ee4f41d 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -135,6 +135,12 @@ echo "HOST_WORKSPACE_REPO=$HOST_WORKSPACE_REPO" ## should be /github/workspace # echorun ls -hal +if [ "$OCAML407" = "true" ]; then + _OCAML407_COMMAND='opam switch ${COMPILER_EDGE}; eval $(opam env)' +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" \ @@ -142,7 +148,7 @@ docker run -i --init --rm --name=COQ -e PACKAGE="$PACKAGE" \ "$COQ_IMAGE" /bin/bash --login -c " endGroup () { init_opts=\"\$-\"; set +x; 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; 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 +$_OCAML407_COMMAND $_SCRIPT" script echo "done" From ceb59e6c2de4b5a2c5ce5b8254b82bcdeced6da5 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 28 Mar 2020 23:12:24 +0100 Subject: [PATCH 07/10] docs: Update the custom_script default and documentation * The "startGroup GroupTitle"/"endGroup" commands allow one to create timed foldable sections in the GitHub action logging. --- README.md | 20 ++++++++++++++------ action.yml | 20 ++++++++++++++------ 2 files changed, 28 insertions(+), 12 deletions(-) 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' From adf418b7554e5b412f21dc9bd167ecae2cc297f5 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 1 Apr 2020 20:25:13 +0200 Subject: [PATCH 08/10] chore: Add Makefile to automate the generation/tests --- Makefile | 19 +++++++++++++++++++ entrypoint.sh | 5 ++++- helper.sh | 5 +++-- 3 files changed, 26 insertions(+), 3 deletions(-) create mode 100644 Makefile 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/entrypoint.sh b/entrypoint.sh index ee4f41d..a896821 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -3,7 +3,9 @@ set -e -. /app/timegroup.sh +timegroup_file="/app/timegroup.sh" +# shellcheck source=./timegroup.sh +. "$timegroup_file" startGroup Print runner configuration @@ -136,6 +138,7 @@ echo "HOST_WORKSPACE_REPO=$HOST_WORKSPACE_REPO" # echorun ls -hal if [ "$OCAML407" = "true" ]; then + # shellcheck disable=SC2016 _OCAML407_COMMAND='opam switch ${COMPILER_EDGE}; eval $(opam env)' else _OCAML407_COMMAND='' diff --git a/helper.sh b/helper.sh index 91e2aff..d8f905f 100755 --- a/helper.sh +++ b/helper.sh @@ -4,6 +4,7 @@ srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd ) +# shellcheck source=./timegroup.sh . "$srcdir/timegroup.sh" run_tests() { @@ -11,7 +12,7 @@ run_tests() { if endGroup; then echo "FAILURE: endGroup should raise an error" else - : OK + echo "Error OK." fi startGroup sleep 1s @@ -19,7 +20,7 @@ run_tests() { startGroup This is a test sleep 2s endGroup - echo "Done." + echo "DONE." } minimify() { From e3697ee03d31930942320d8751b23fe17b5b30e1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 1 Apr 2020 20:27:01 +0200 Subject: [PATCH 09/10] fix(timegroup.sh): reduce $(set -x)'s noise in startGroup/endGroup $ make gen --- entrypoint.sh | 2 +- timegroup.sh | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/entrypoint.sh b/entrypoint.sh index a896821..cba4e50 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -149,7 +149,7 @@ 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; 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; 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 +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 $_OCAML407_COMMAND $_SCRIPT" script diff --git a/timegroup.sh b/timegroup.sh index be29f64..4a3831b 100755 --- a/timegroup.sh +++ b/timegroup.sh @@ -3,7 +3,7 @@ endGroup() { # This function unsets the env var 'startTime'. - init_opts="$-"; set +x + { init_opts="$-"; set +x; } 2>/dev/null # local endTime if [ -n "$startTime" ]; then # endTime=$(TZ=UTC+0 printf '%(%s)T\n' '-1') # not POSIX @@ -23,7 +23,7 @@ endGroup() { startGroup() { # This function sets the env var 'startTime'. - init_opts="$-"; set +x + { init_opts="$-"; set +x; } 2>/dev/null # Nesting groups is not supported; call 'endGroup' if need be. if [ -n "$startTime" ]; then endGroup From 25213563b0af62a9f02202442c6bbe3501ece17b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 1 Apr 2020 20:36:15 +0200 Subject: [PATCH 10/10] fix: Enclose the 'opam switch' command in a timegroup --- entrypoint.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/entrypoint.sh b/entrypoint.sh index cba4e50..3894cd5 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -139,7 +139,7 @@ echo "HOST_WORKSPACE_REPO=$HOST_WORKSPACE_REPO" if [ "$OCAML407" = "true" ]; then # shellcheck disable=SC2016 - _OCAML407_COMMAND='opam switch ${COMPILER_EDGE}; eval $(opam env)' + _OCAML407_COMMAND='startGroup Change opam switch; opam switch ${COMPILER_EDGE}; eval $(opam env); endGroup' else _OCAML407_COMMAND='' fi