From 4de4d6eceab9121afdff39cdc1ce98dfc332f3ac Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Sun, 26 Apr 2020 23:02:01 +0200
Subject: [PATCH 01/12] fix: Generate coq-proj.opam instead of coq.opam

---
 generate.sh | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/generate.sh b/generate.sh
index bf9b328..f7b5e8a 100755
--- a/generate.sh
+++ b/generate.sh
@@ -3,6 +3,13 @@
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
 for f in "$srcdir"/{,.}*.mustache; do
-    echo "Generating $(basename "$f" .mustache)..."
-    mustache meta.yml "$f" > "$(basename "$f" .mustache)"
+    target=$(basename "$f" .mustache)
+    case "$target" in
+        *.opam)
+            shortname=$(grep -e "shortname:" meta.yml | sed -e "s/^shortname: //")
+            target=${target/coq/coq-$shortname}
+            ;;
+    esac
+    echo "Generating $target..."
+    mustache meta.yml "$f" > "$target"
 done

From 5831eeff7d0ba3c91803ceabdb4ce0aea48d7243 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Sun, 26 Apr 2020 23:14:28 +0200
Subject: [PATCH 02/12] Add coq-action.yml.mustache

Note: GitHub actions relies on the ${{ _ }} syntax, which conflicts
with mustache.

This can be workarounded by changing the delimiters beforehand, as
suggested by theK42 <https://stackoverflow.com/a/13695429/9164010> and
documented in https://mustache.github.io/mustache.5.html#Set-Delimiter
---
 coq-action.yml.mustache | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 coq-action.yml.mustache

diff --git a/coq-action.yml.mustache b/coq-action.yml.mustache
new file mode 100644
index 0000000..da2694a
--- /dev/null
+++ b/coq-action.yml.mustache
@@ -0,0 +1,33 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        coq_version:
+{{# tested_coq_opam_versions }}
+          - {{ version }}
+{{/ tested_coq_opam_versions }}
+        ocaml_version: ['4.07-flambda']
+    steps:
+    - uses: actions/checkout@v2
+    - uses: coq-community/docker-coq-action@v1
+      with:
+        opam_file: 'coq-{{ shortname }}.opam'
+{{=<% %>=}}
+        coq_version: ${{ matrix.coq_version }}
+        ocaml_version: ${{ matrix.ocaml_version }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

From 2a94c0774a3fb47b0f191b093d968f43083739ff Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Sun, 26 Apr 2020 23:22:05 +0200
Subject: [PATCH 03/12] feat: Propose to create a subfolder before generating
 coq-action.yml

---
 generate.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/generate.sh b/generate.sh
index f7b5e8a..cad4b13 100755
--- a/generate.sh
+++ b/generate.sh
@@ -2,6 +2,8 @@
 
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
+function ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
+
 for f in "$srcdir"/{,.}*.mustache; do
     target=$(basename "$f" .mustache)
     case "$target" in
@@ -9,6 +11,10 @@ for f in "$srcdir"/{,.}*.mustache; do
             shortname=$(grep -e "shortname:" meta.yml | sed -e "s/^shortname: //")
             target=${target/coq/coq-$shortname}
             ;;
+        coq-action.yml)
+            ask1 "Do you want to create a .github/workflows subfolder for coq-action.yml?" &&
+                { mkdir -p .github/workflows; target=".github/workflows/$target"; }
+            ;;
     esac
     echo "Generating $target..."
     mustache meta.yml "$f" > "$target"

From d10c50aa1cf75ab6d603b6527c030056093cfcd9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Sun, 26 Apr 2020 23:35:00 +0200
Subject: [PATCH 04/12] =?UTF-8?q?docs(README.md):=20Add=20"mustache=20meta?=
 =?UTF-8?q?.yml=20=E2=80=A6"=20command?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index 7bb42b6..194fa3f 100644
--- a/README.md
+++ b/README.md
@@ -38,6 +38,8 @@ mustache meta.yml ../templates/default.nix.mustache > default.nix
 mustache meta.yml ../templates/README.md.mustache > README.md
 mustache meta.yml ../templates/.travis.yml.mustache > .travis.yml
 mustache meta.yml ../templates/coq.opam.mustache > coq-aac-tactics.opam
+mkdir -p .github/workflows
+mustache meta.yml ../templates/coq-action.yml.mustache > .github/workflows/coq-action.yml
 ```
 Other projects using the templates in a similar way include
 [Chapar](https://github.com/coq-community/chapar) and

From acbd3faec00f529d3e22a836fe665e3645df42ea Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Mon, 27 Apr 2020 13:28:51 +0200
Subject: [PATCH 05/12] fix: Address review comments by @Zimmi48

---
 coq-action.yml.mustache |  3 ++-
 generate.sh             | 10 +++++++---
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/coq-action.yml.mustache b/coq-action.yml.mustache
index da2694a..6229876 100644
--- a/coq-action.yml.mustache
+++ b/coq-action.yml.mustache
@@ -18,12 +18,13 @@ jobs:
 {{# tested_coq_opam_versions }}
           - {{ version }}
 {{/ tested_coq_opam_versions }}
-        ocaml_version: ['4.07-flambda']
+        ocaml_version: ['minimal']
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
       with:
         opam_file: 'coq-{{ shortname }}.opam'
+{{! Change delimiters to avoid the next two lines being parsed as mustache syntax. }}
 {{=<% %>=}}
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
diff --git a/generate.sh b/generate.sh
index cad4b13..955fc6b 100755
--- a/generate.sh
+++ b/generate.sh
@@ -7,9 +7,13 @@ function ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Y
 for f in "$srcdir"/{,.}*.mustache; do
     target=$(basename "$f" .mustache)
     case "$target" in
-        *.opam)
-            shortname=$(grep -e "shortname:" meta.yml | sed -e "s/^shortname: //")
-            target=${target/coq/coq-$shortname}
+        coq.opam)
+            shortname=$(grep -e "^shortname:" meta.yml | sed -e 's/^shortname:\s\+//')
+            [ -n "$shortname" ] && target=${target/coq/coq-$shortname}
+            ;;
+        extracted.opam)
+            extracted_shortname=$(grep -e "^\s\+extracted_shortname:" meta.yml | sed -e 's/^\s\+extracted_shortname:\s\+//')
+            [ -n "$extracted_shortname" ] && target=${target/extracted/$extracted_shortname}
             ;;
         coq-action.yml)
             ask1 "Do you want to create a .github/workflows subfolder for coq-action.yml?" &&

From 7178ff84a49e9ef9cb5bb450ee33864239fe48e0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Mon, 27 Apr 2020 13:39:52 +0200
Subject: [PATCH 06/12] fix: Skip {*.opam, coq-action.yml} steps if they're not
 applicable

---
 generate.sh | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/generate.sh b/generate.sh
index 955fc6b..1f40e5e 100755
--- a/generate.sh
+++ b/generate.sh
@@ -9,15 +9,26 @@ for f in "$srcdir"/{,.}*.mustache; do
     case "$target" in
         coq.opam)
             shortname=$(grep -e "^shortname:" meta.yml | sed -e 's/^shortname:\s\+//')
-            [ -n "$shortname" ] && target=${target/coq/coq-$shortname}
+            if [ -n "$shortname" ]; then
+                target=${target/coq/coq-$shortname}
+            else
+                continue
+            fi
             ;;
         extracted.opam)
             extracted_shortname=$(grep -e "^\s\+extracted_shortname:" meta.yml | sed -e 's/^\s\+extracted_shortname:\s\+//')
-            [ -n "$extracted_shortname" ] && target=${target/extracted/$extracted_shortname}
+            if [ -n "$extracted_shortname" ]; then
+                target=${target/extracted/$extracted_shortname}
+            else
+                continue
+            fi
             ;;
         coq-action.yml)
-            ask1 "Do you want to create a .github/workflows subfolder for coq-action.yml?" &&
-                { mkdir -p .github/workflows; target=".github/workflows/$target"; }
+            if ask1 "Do you wish to generate the file .github/workflows/coq-action.yml?"; then
+                mkdir -p .github/workflows; target=".github/workflows/$target"
+            else
+                continue
+            fi
             ;;
     esac
     echo "Generating $target..."

From 4f1a8d70bb6f38ee6a3560187bdc4c3f3ef4551e Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Mon, 27 Apr 2020 13:43:39 +0200
Subject: [PATCH 07/12] =?UTF-8?q?fix:=20Use=20"mkdir=20-p=20-v=20=E2=80=A6?=
 =?UTF-8?q?=20&&=20=E2=80=A6"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 generate.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/generate.sh b/generate.sh
index 1f40e5e..058c872 100755
--- a/generate.sh
+++ b/generate.sh
@@ -25,7 +25,7 @@ for f in "$srcdir"/{,.}*.mustache; do
             ;;
         coq-action.yml)
             if ask1 "Do you wish to generate the file .github/workflows/coq-action.yml?"; then
-                mkdir -p .github/workflows; target=".github/workflows/$target"
+                mkdir -p -v .github/workflows && target=".github/workflows/$target"
             else
                 continue
             fi

From 7303c58b2a6e686e9eeae813c73c672cbc9bd777 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Tue, 28 Apr 2020 20:10:39 +0200
Subject: [PATCH 08/12] refactor: Query meta.yml in a more semantical way using
 mustache

---
 generate.sh | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/generate.sh b/generate.sh
index 058c872..9d2afd2 100755
--- a/generate.sh
+++ b/generate.sh
@@ -2,13 +2,24 @@
 
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
-function ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
+ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
+
+get_yaml() {
+    # Arg 1: the meta.yml path
+    # STDIN: the mustache code
+    local meta="$1" temp
+    temp=$(mktemp --tmpdir --suffix .yml template-XXX)
+    cat > "$temp"
+    mustache "$meta" "$temp"
+    rm -f "$temp"
+}
 
 for f in "$srcdir"/{,.}*.mustache; do
     target=$(basename "$f" .mustache)
     case "$target" in
         coq.opam)
-            shortname=$(grep -e "^shortname:" meta.yml | sed -e 's/^shortname:\s\+//')
+            mustache='{{ shortname }}'
+            shortname=$(get_yaml meta.yml <<<"$mustache")
             if [ -n "$shortname" ]; then
                 target=${target/coq/coq-$shortname}
             else
@@ -16,7 +27,8 @@ for f in "$srcdir"/{,.}*.mustache; do
             fi
             ;;
         extracted.opam)
-            extracted_shortname=$(grep -e "^\s\+extracted_shortname:" meta.yml | sed -e 's/^\s\+extracted_shortname:\s\+//')
+            mustache='{{# extracted }}{{ extracted_shortname }}{{/ extracted }}'
+            extracted_shortname=$(get_yaml meta.yml <<<"$mustache")
             if [ -n "$extracted_shortname" ]; then
                 target=${target/extracted/$extracted_shortname}
             else

From cc3e3508090089314ad0e569b7f0ec9a6f346e7d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Fri, 1 May 2020 00:32:47 +0200
Subject: [PATCH 09/12] feat: Gen .travis.yml & coq-action.yml conditionally in
 batch mode

namely if meta.yml contains a "travis" (resp. "action") key with a
different value than "false".
---
 generate.sh | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/generate.sh b/generate.sh
index 9d2afd2..254f6bc 100755
--- a/generate.sh
+++ b/generate.sh
@@ -2,7 +2,8 @@
 
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
-ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
+# ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
+# if ask1 "Question?"; then ...; else ...; fi
 
 get_yaml() {
     # Arg 1: the meta.yml path
@@ -11,7 +12,7 @@ get_yaml() {
     temp=$(mktemp --tmpdir --suffix .yml template-XXX)
     cat > "$temp"
     mustache "$meta" "$temp"
-    rm -f "$temp"
+    rm -f -- "$temp"
 }
 
 for f in "$srcdir"/{,.}*.mustache; do
@@ -36,12 +37,23 @@ for f in "$srcdir"/{,.}*.mustache; do
             fi
             ;;
         coq-action.yml)
-            if ask1 "Do you wish to generate the file .github/workflows/coq-action.yml?"; then
+            mustache='{{ action }}'
+            bool=$(get_yaml meta.yml <<<"$mustache")
+            if [ -n "$bool" ] && [ "$bool" != false ]; then
                 mkdir -p -v .github/workflows && target=".github/workflows/$target"
             else
                 continue
             fi
             ;;
+        .travis.yml | default.nix)
+            mustache='{{ travis }}'
+            bool=$(get_yaml meta.yml <<<"$mustache")
+            if [ -n "$bool" ] && [ "$bool" != false ]; then
+                : noop
+            else
+                continue
+            fi
+            ;;
     esac
     echo "Generating $target..."
     mustache meta.yml "$f" > "$target"

From a2fe3e2136c3c7ba0d15f65f93be1f4f801a3ee8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Fri, 1 May 2020 00:39:48 +0200
Subject: [PATCH 10/12] feat(README.md.mustache): Add GitHub action badge if
 need be

---
 README.md.mustache | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/README.md.mustache b/README.md.mustache
index f37375f..cc2a55e 100644
--- a/README.md.mustache
+++ b/README.md.mustache
@@ -3,6 +3,9 @@
 {{# travis }}
 [![Travis][travis-shield]][travis-link]
 {{/ travis }}
+{{# action }}
+[![CI][action-shield]][action-link]
+{{/ action }}
 {{# circleci }}
 [![CircleCI][circleci-shield]][circleci-link]
 {{/ circleci }}
@@ -22,6 +25,10 @@
 [travis-shield]: https://travis-ci.com/{{ organization }}/{{ shortname }}.svg?branch=master
 [travis-link]: https://travis-ci.com/{{ organization }}/{{ shortname }}/builds
 {{/ travis }}
+{{# action }}
+[action-shield]: https://github.com/{{ organization }}/{{ shortname }}/workflows/CI/badge.svg?branch=master
+[action-link]: https://github.com/{{ organization }}/{{ shortname }}/actions?query=workflow%3ACI
+{{/ action }}
 {{# circleci }}
 [circleci-shield]: https://circleci.com/gh/{{ organization }}/{{ shortname }}.svg?style=svg
 [circleci-link]:   https://circleci.com/gh/{{ organization }}/{{ shortname }}

From d9f7aa032e7d35d4b1f0be080803bcef0bdddb57 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Fri, 1 May 2020 13:49:37 +0200
Subject: [PATCH 11/12] feat: Don't cancel all in-progress jobs if one matrix
 job fails

---
 coq-action.yml.mustache | 1 +
 1 file changed, 1 insertion(+)

diff --git a/coq-action.yml.mustache b/coq-action.yml.mustache
index 6229876..a14bd9a 100644
--- a/coq-action.yml.mustache
+++ b/coq-action.yml.mustache
@@ -19,6 +19,7 @@ jobs:
           - {{ version }}
 {{/ tested_coq_opam_versions }}
         ocaml_version: ['minimal']
+      fail-fast: false
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

From f623a574cf9b311b65d00605240cee1e112999fa Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Fri, 1 May 2020 15:42:10 +0200
Subject: [PATCH 12/12] docs: Address review comments by @Zimmi48

---
 README.md   | 14 ++++++++++----
 generate.sh | 14 ++++++++++----
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index 194fa3f..bae5ead 100644
--- a/README.md
+++ b/README.md
@@ -34,12 +34,10 @@ configuration and boilerplate files in the
 [AAC Tactics](https://github.com/coq-community/aac-tactics)
 project are generated as follows:
 ```shell
-mustache meta.yml ../templates/default.nix.mustache > default.nix
 mustache meta.yml ../templates/README.md.mustache > README.md
-mustache meta.yml ../templates/.travis.yml.mustache > .travis.yml
 mustache meta.yml ../templates/coq.opam.mustache > coq-aac-tactics.opam
-mkdir -p .github/workflows
-mustache meta.yml ../templates/coq-action.yml.mustache > .github/workflows/coq-action.yml
+mustache meta.yml ../templates/default.nix.mustache > default.nix
+mustache meta.yml ../templates/.travis.yml.mustache > .travis.yml
 ```
 Other projects using the templates in a similar way include
 [Chapar](https://github.com/coq-community/chapar) and
@@ -54,6 +52,14 @@ cd -
 ../templates/generate.sh
 git add <the_generated_files>
 ```
+Regarding continuous integration, the `generate.sh` script will create:
+* a [Travis CI](https://docs.travis-ci.com/) configuration
+    [(based on opam + Nix)](./.travis.yml.mustache),
+* or a [GitHub Action](https://help.github.com/en/actions) workflow
+    [(based on opam)](./coq-action.yml.mustache),
+
+depending on whether `meta.yml` contains `travis: true` or `action: true`.
+
 Keeping generated files under version control is not ideal, but `README.md` has to exist,
 and generally this is a common practice when using build systems such as Autotools.
 To get a `mustache` tool in, e.g., NixOS, you can run `nix-env -i mustache-go`.
diff --git a/generate.sh b/generate.sh
index 254f6bc..452c2b5 100755
--- a/generate.sh
+++ b/generate.sh
@@ -2,9 +2,6 @@
 
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
-# ask1() { local yn; echo -n "$* [Y/n] "; read -r -n 1 yn; [[ "$yn" =~ [Yy] ]] && echo && return 0; [ -z "$yn" ] && return 0; echo; return 1; }
-# if ask1 "Question?"; then ...; else ...; fi
-
 get_yaml() {
     # Arg 1: the meta.yml path
     # STDIN: the mustache code
@@ -45,7 +42,7 @@ for f in "$srcdir"/{,.}*.mustache; do
                 continue
             fi
             ;;
-        .travis.yml | default.nix)
+        .travis.yml)
             mustache='{{ travis }}'
             bool=$(get_yaml meta.yml <<<"$mustache")
             if [ -n "$bool" ] && [ "$bool" != false ]; then
@@ -54,6 +51,15 @@ for f in "$srcdir"/{,.}*.mustache; do
                 continue
             fi
             ;;
+        default.nix)
+            mustache='{{ tested_coq_nix_versions }}'
+            bool=$(get_yaml meta.yml <<<"$mustache")
+            if [ -n "$bool" ] && [ "$bool" != false ]; then
+                : noop
+            else
+                continue
+            fi
+            ;;
     esac
     echo "Generating $target..."
     mustache meta.yml "$f" > "$target"