From 141e422629663739f4fcfd4e7afac24af91fbab8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Mon, 7 Dec 2020 11:22:36 +0100
Subject: [PATCH] feat: Support more compilers & Remove useless 'opam switch
 $COMPILER_EDGE'

* This patch is a backward-compatible change

* Related:
- https://github.com/coq-community/docker-coq/pull/7
- https://github.com/coq-community/docker-coq/issues/12#issuecomment-707165691
---
 README.md     |  7 ++++++-
 action.yml    |  4 +++-
 entrypoint.sh | 28 ++++++++++------------------
 3 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/README.md b/README.md
index 03392f9..696d6ab 100644
--- a/README.md
+++ b/README.md
@@ -102,7 +102,12 @@ install all the `*.opam` packages stored in this directory.
 #### `ocaml_version`
 
 *Optional* The version of OCaml. Default `"minimal"`.
-Among `"minimal"`, `"4.07-flambda"`, `"4.09-flambda"`.
+Among `"minimal"` (*deprecated, to be removed on 14 December 2020*),
+`"default"`, `"4.02"`, `"4.05"`, `"4.07-flambda"`,
+`"4.08-flambda"`, `"4.09-flambda"`, `"4.10-flambda"`, `"4.11-flambda"`.
+
+The supported compilers w.r.t. each version of Coq are documented in the
+[Supported tags](https://github.com/coq-community/docker-coq/wiki#supported-tags) section of the `docker-coq` wiki.
 
 #### `before_install`
 
diff --git a/action.yml b/action.yml
index 9e55ea4..1a626f1 100644
--- a/action.yml
+++ b/action.yml
@@ -12,8 +12,10 @@ inputs:
     description: '"8.X", "latest", or "dev".'
     default: 'latest'
   ocaml_version:
-    description: 'minimal, 4.07-flambda, or 4.09-flambda'
+    description: 'minimal (deprecated), default, 4.02, 4.05, 4.07-flambda, 4.08-flambda, 4.09-flambda, 4.10-flambda, or 4.11-flambda'
     default: 'minimal'
+    # TODO: uncomment this at the end of the one-switch docker-coq migration
+    # default: 'default'
   before_install:
     description: 'Customizable script run before "install", empty by default.'
     default: |
diff --git a/entrypoint.sh b/entrypoint.sh
index c87a396..71d5756 100755
--- a/entrypoint.sh
+++ b/entrypoint.sh
@@ -103,6 +103,16 @@ if test -z "$INPUT_CUSTOM_IMAGE"; then
 
     # TODO: validation of INPUT_COQ_VERSION, INPUT_OCAML_VERSION
     COQ_IMAGE="coqorg/coq:$INPUT_COQ_VERSION"
+
+    # TODO: uncomment this at the end of the one-switch docker-coq migration
+    # if [ "$INPUT_OCAML_VERSION" = 'minimal' ]; then
+    #     echo "ERROR: 'ocaml_version: minimal' is not supported anymore."
+    #     exit 1
+    # fi
+    if [ "$INPUT_OCAML_VERSION" != 'default' ] \
+       && [ "$INPUT_OCAML_VERSION" != 'minimal' ]; then
+        COQ_IMAGE="${COQ_IMAGE}-ocaml-${INPUT_OCAML_VERSION}"
+    fi
 else
     COQ_IMAGE="$INPUT_CUSTOM_IMAGE"
 fi
@@ -146,16 +156,6 @@ if test -z "$INPUT_CUSTOM_SCRIPT_EXPANDED"; then
     exit 1
 fi
 
-# todo: update this after the one-switch docker-coq migration
-OCAML407="false"
-if [ "$INPUT_OCAML_VERSION" = '4.09-flambda' ]; then
-    COQ_IMAGE="${COQ_IMAGE}-ocaml-4.09-flambda"
-elif [ "$INPUT_OCAML_VERSION" = '4.07-flambda' ]; then
-    OCAML407="true"
-# else Assume "$INPUT_OCAML_VERSION" = 'minimal'
-fi
-echo OCAML407="$OCAML407"
-
 startGroup "Pull docker-coq image"
 
 echo COQ_IMAGE="$COQ_IMAGE"
@@ -163,13 +163,6 @@ docker pull "$COQ_IMAGE"
 
 endGroup
 
-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
-
 cp /app/coq.json "$HOME/coq.json"
 echo "::add-matcher::$HOME/coq.json"
 
@@ -180,7 +173,6 @@ docker run -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e
        "$COQ_IMAGE" /bin/bash --login -c "
 exec 2>&1 ; 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
 $INPUT_CUSTOM_SCRIPT_EXPANDED" script
 
 echo "::remove-matcher owner=coq-problem-matcher::"