opam_file should not be mandatory

[JasonGross]

It doesn't seem necessary, and I'd rather not be forced to pass a dummy string / create a dummy opam file.

[Zimmi48]

But what would be the default in case you don't set custom_script?

[JasonGross]

Make the default script error if it's not there. It seems fine to make having neither custom script nor opam file a runtime error, rather than picking one of them and making it an earlier runtime error to not have that one.

[Zimmi48]

Another solution would be for the default script to look for a unique *.opam file at the root of the repository if this variable is not provided. This would mean that the simplest possible CI configuration would become just:

name: CI

on:
  push:
  pull_request:

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v2
    - uses: coq-community/docker-coq-action@v1

WDYT @erikmd?

[erikmd]

Hi, admittedly in the docker-coq-action snippet I suggested on Zulip, the fact one has to put a dummy .opam filename when overriding custom_script (albeit this is not the "standard" use case of docker-coq-action) is a bit ugly. Next, what @Zimmi48 suggest in his comment https://github.com/coq-community/docker-coq-action/issues/26#issuecomment-695772309 looks appealing, and I'd just suggest a variation of his suggestion:

• Keep the opam_script default value as is:

  startGroup Print opam config
    opam config list; opam repo list; opam list
  endGroup
  startGroup Build dependencies
    opam pin add -n -y -k path $PACKAGE $WORKDIR
    opam update -y
    opam install -y -j 2 $PACKAGE --deps-only
  endGroup
  startGroup Build
    opam install -y -v -j 2 $PACKAGE
    opam list
  endGroup
  startGroup Uninstallation test
    opam remove $PACKAGE
  endGroup

• Allow passing some opam_file without the .opam suffix, as well as an empty string.

• Replace these lines, currently:

  WORKDIR=$(dirname "$INPUT_OPAM_FILE")
  PACKAGE=$(basename "$INPUT_OPAM_FILE" .opam)

  with:

  if [ -z "$INPUT_OPAM_FILE" ] || [ -d "$INPUT_OPAM_FILE" ]; then
      WORKDIR=""
      PACKAGE=${INPUT_OPAM_FILE:-.}
  else
      WORKDIR=$(dirname "$INPUT_OPAM_FILE")
      PACKAGE=$(basename "$INPUT_OPAM_FILE" .opam)
  fi

  (I first thought about a condition [ "${INPUT_OPAM_FILE%.opam}" = "$INPUT_OPAM_FILE" ] for the first if, but this wouldn't work if the opam_file is just …/opam, since that filename is still supported by opam 2.0)

As a result:

• if opam_file is empty, no error is raised, and @JasonGross's use case can be run directly without a dummy .opam file;

• if opam_file is a directory (instead of a filename ending in .opam), e.g. ., we get another feature for free: the default custom_script will run:

  startGroup Print opam config
    opam config list; opam repo list; opam list
  endGroup
  startGroup Build dependencies
    opam pin add -n -y -k path .
    opam update -y
    opam install -y -j 2 . --deps-only
  endGroup
  startGroup Build
    opam install -y -v -j 2 .
    opam list
  endGroup
  startGroup Uninstallation test
    opam remove .
  endGroup

  which can be handy for the following use case: *compiling a Coq project that contains several `.opamfiles in one go**. (incidentally, this works out-of-the-box just because$WORKDIRwas not quoted (vs."$WORKDIR"`), which is fortunately not a issue given that the directory structure of a Coq project / module path does not contain any space :)

@Zimmi48 @JasonGross: If this new semantics look good to you, I'll open a PR.

[Zimmi48]

Looks terrific!

[Zimmi48]

Since opam_file is now optional, this means that the most simple workflow configuration corresponds to the one I wrote in my comment above (except that we can compress the on: part even more). I think that showing such a simple (complete) configuration somewhere near the top of the README would look great (to show how simple it is to use Docker-Coq-Action for simple use cases).