Customize pin set

[liyishuai]

VST can be built with several variants of CompCert: https://github.com/PrincetonUniversity/VST/blob/master/BUILD_ORGANIZATION.md#install-method-1-use-opam It'll be nice to pin down specific versions of dependencies, see: https://github.com/ocaml/ocaml-ci-scripts/blob/master/README-travis.md#customizing-the-opam-pin-set

[erikmd]

@liyishuai note that the script run by docker-coq-action can be customized. but indeed one could think about some in-between customization. do you believe that implementing #23 to pass some env. variables would suffice to support this use case (#22)?

[liyishuai]

do you believe that implementing #23 to pass some env. variables would suffice to support this use case (#22)?

Maybe yes, we can allow users to configure PINS and handle it with a bash script.

[erikmd]

But are you sure that PINS is a standard variable for opam? at first sight it is only a facility of the ocaml-ci-scripts repo scripts: https://github.com/ocaml/ocaml-ci-scripts/blob/1c49dda8815d491ea76f8562c9afb841169cd33c/.travis-docker.sh#L27 https://github.com/ocaml/ocaml-ci-scripts/blob/5e0c192eabbf32f51d9d4896d658aa7f027089c2/src/ci_opam.ml#L47

[liyishuai]

It is not part of OPAM. If configuring with PINS, we need to handle it in a similar way as ci_opam does.

[liyishuai]

My current solution is: https://github.com/liyishuai/VST/blob/a5f6d991eea2da51d4b476b2d2f3f3bfe8b438f3/.github/workflows/coq-action.yml#L42-L43 Maybe allow users to insert arbitrary before_install_script?

[erikmd]

Maybe allow users to insert arbitrary before_install_script?

Yes, that solution seems easier than the environment-variable solution (all the more as the latter solution would imply to give special semantics to some environment variables (PINS, unlike OPAMWITHTEST), which is not that intuitive)

But regarding the naming of that extra option I'm unsure, I'd like to have the opinion of @Zimmi48

Also ideally the change should be consistent with the other feature request #20

[Zimmi48]

This name sounds reasonable to me. I like the idea of being able to plug small bits of customization into the default script instead of having to copy the entire thing just to add one line.

[liyishuai]

Since this issue is mentioned by users, should we step towards implementing the before_install_script? Instead of inserting to custom_script, we should probably split custom_script into a series of actions similar to Travis CI job lifecycle, offer default operations for each, and allow users to customize at any stage.

[erikmd]

Hi @liyishuai, sorry for the delay, being quite swamped by the start of autumn term…

I fully support the feature you suggest (adding a before_install_script option that could perform additional opam pin etc.), however I'd really like to make this backward-compatible (because by definition of semver, coq-community/docker-coq-action@v1 updates should preserve backward-compatibiltiy), so in particular it would be great to be able to keep the custom_script option available with the current semantics, but just "split it" and defer the customization to new options such as before_install_script.

However, this does not seem straightforward to do it as:

• the standard GitHub Actions interpolation ${{ before_install_script }} won't work because before_install_script is not a GHA variable;
• even if we keep this entrypoint line as is, and we pass additional environment variables to the container here, such as -e INPUT_BEFORE_INSTALL_SCRIPT="$INPUT_BEFORE_INSTALL_SCRIPT", this does not work out-of-the-box if before_install_script also contain variables such as $PACKAGE or $WORKDIR.
  to sum up, we'd need here some way to perform two Bash variable-interpolations.

[erikmd]

Otherwise, while we are on it, maybe we could just decide that custom_script is a mustache-enhanced bash script? I mean, a regular bash script, with additionnaly mustache strings which will be expanded once with https://github.com/tests-always-included/mo, before running the container script with docker run?

In this case, which naming would be OK for you?

• {{ INPUT_BEFORE_INSTALL_SCRIPT }}
• or {{ before_install_script }}

Cc @Zimmi48 @liyishuai @gares

[erikmd]

Just to discuss on some example, here is a tentative draft (inspired by Travis CI :)

default custom_script:

startGroup Print opam config
  opam config list; opam repo list; opam list
endGroup
startGroup Build dependencies
  {{ before_install }}
  {{ install }}
endGroup
startGroup Build
  {{ before_script }}
  {{ script }}
  {{ after_script }}
endGroup
startGroup Uninstallation test
  {{ uninstall }}
endGroup

default before_install: ""

default install:

opam pin add -n -y -k path $PACKAGE $WORKDIR
opam update -y
opam install -y -j 2 $PACKAGE --deps-only

default before_script: ""

default script:

opam install -y -v -j 2 $PACKAGE
opam list

default after_script: ""

default uninstall:

opam remove $PACKAGE

As an aside, the current workaround by @liyishuai (https://github.com/liyishuai/VST/blob/a5f6d991eea2da51d4b476b2d2f3f3bfe8b438f3/.github/workflows/coq-action.yml#L42-L43) would be phrased like this (assuming opam update -y can/should be run after opam pin add -y coq-compcert-64 3.7~coq-platform):

    steps:
      - uses: actions/checkout@v2
      - name: Checkout submodules
        uses: textbook/git-checkout-submodule-action@2.1.1
      - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: ${{ matrix.opam_name }}.opam
          coq_version: ${{ matrix.coq_version }}
          before_install: ${{ matrix.pin_script }}
          after_script: "opam install -y -v -t -j 2 $PACKAGE"

WDYT?

[liyishuai]

Just to discuss on some example, here is a tentative draft (inspired by Travis CI :) ...

This is exactly what I intended! Thanks for composing this example!

[gares]

It looks perfect.