Skip to content

Commit

Permalink
Merge pull request #33 from coq-community/split-script
Browse files Browse the repository at this point in the history
Split custom_script to enhance the customization experience
  • Loading branch information
erikmd authored Nov 27, 2020
2 parents d520b0a + 2d785ba commit ab40295
Show file tree
Hide file tree
Showing 3 changed files with 222 additions and 71 deletions.
212 changes: 155 additions & 57 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,12 @@ For more details about these images, see the
Assuming the Git repository contains a `folder/coq-proj.opam` file,
it will run (by default) the following commands:

```bash
```
opam config list; opam repo list; opam list
opam pin add -n -y -k path coq-proj folder
opam update -y
opam install -y -j 2 coq-proj --deps-only
opam list
opam install -y -v -j 2 coq-proj
opam list
opam remove coq-proj
Expand Down Expand Up @@ -79,7 +80,7 @@ Default `"."` (if the argument is omitted or an empty string).
*Note-1:* relying on the value of this `INPUT_OPAM_FILE` variable, the
following two variables are exported when running the `custom_script`:

```bash
```
if [ -z "$INPUT_OPAM_FILE" ] || [ -d "$INPUT_OPAM_FILE" ]; then
WORKDIR=""
PACKAGE=${INPUT_OPAM_FILE:-.}
Expand All @@ -103,74 +104,128 @@ install all the `*.opam` packages stored in this directory.
*Optional* The version of OCaml. Default `"minimal"`.
Among `"minimal"`, `"4.07-flambda"`, `"4.09-flambda"`.

#### `before_install`

*Optional* The bash snippet to run before `install`

Default:

```
opam config list; opam repo list; opam list
```

See [`custom_script`](#custom_script) for more details.

#### `install`

*Optional* The bash snippet to install the `opam` `PACKAGE` dependencies.

Default:

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

See [`custom_script`](#custom_script) for more details.

#### `after_install`

*Optional* The bash snippet to run after `install` (if successful).

Default:

```
opam list
```

See [`custom_script`](#custom_script) for more details.

#### `before_script`

*Optional* The bash snippet to run before `script`. Default `""` (empty string).

See [`custom_script`](#custom_script) for more details.

#### `script`

*Optional* The bash snippet to install the `opam` `PACKAGE`.

Default:

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

See [`custom_script`](#custom_script) for more details.

#### `after_script`

*Optional* The bash snippet to run after `script` (if successful). Default `""` (empty string).

See [`custom_script`](#custom_script) for more details.

#### `uninstall`

*Optional* The bash snippet to uninstall the `opam` `PACKAGE`.

Default:

```
opam remove $PACKAGE
```

See [`custom_script`](#custom_script) for more details.

#### `custom_script`

*Optional* The main script run in the container; may be overridden. Default:
*Optional* The main script run in the container; may be overridden; but overriding more specific parts of the script is preferred.

Default:

```bash
startGroup Print opam config
opam config list; opam repo list; opam list
```
startGroup before_install dependencies
{{before_install}}
endGroup
startGroup install dependencies
{{install}}
endGroup
startGroup after_install dependencies
{{after_install}}
endGroup
startGroup Build dependencies
opam pin add -n -y -k path $PACKAGE $WORKDIR
opam update -y
opam install -y -j 2 $PACKAGE --deps-only
startGroup before_script
{{before_script}}
endGroup
startGroup List installed packages
opam list
startGroup script
{{script}}
endGroup
startGroup Build
opam install -y -v -j 2 $PACKAGE
opam list
startGroup after_script
{{after_script}}
endGroup
startGroup Uninstallation test
opam remove $PACKAGE
startGroup uninstall
{{uninstall}}
endGroup
```

*Note-1:* if you use the `docker-coq` images, the container user has
UID=GID=1000 while the GitHub action workdir has (UID=1001, GID=116).
This is not an issue when relying on `opam` to build the Coq project.
Otherwise, you may want to use `sudo` in the container to change the
permissions. You may also install additional Debian packages.

Typically, this would lead to a workflow specification like this:

```yaml
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-bignums.opam'
custom_image: ${{ matrix.image }}
custom_script: |
...
startGroup Workaround permission issue
sudo chown -R coq:coq . # <--
endGroup
startGroup Run tests
make -C tests
endGroup
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 . # <--
```
*Note-1:* the semantics of this variable is a *standard Bash script*,
that is evaluated within the workflow container after replacing the
"mustache" placeholders with the value of their variable counterpart.
For example, `{{uninstall}}` will be replaced with the value of the
[`uninstall`](#uninstall) variable (the default value of which being
the string `opam remove $PACKAGE`).

This example was taken from the [coq/bignums CI workflow](https://github.com/coq/bignums/blob/master/.github/workflows/build-coq-bignums.yml).
*Note-2:* this option is named `custom_script` rather than `run` or so
to **discourage changing its recommended, default value** for building
a regular `opam` project, while keeping the flexibility to be able to
change it.

For more details, see also the
[CI setup / Remarks](https://github.com/coq-community/docker-coq/wiki/CI-setup#remarks)
section in the `docker-coq` wiki.
*Note-3:* if you decide to override the `custom_script` value anyway,
you can just as well rely on the "mustache interpolation" of
`{{before_install}}` … `{{uninstall}}`, and customize the underlying
values.

*Note-2: this option is named `custom_script` rather than `script` or
`run` to discourage changing its recommended, default value, while
keeping the flexibility to be able to change it.*

#### `custom_image`

Expand Down Expand Up @@ -242,6 +297,49 @@ clause) after the package build.

### Remarks

#### Permissions

If you use the
[`docker-coq`](https://github.com/coq-community/docker-coq) images,
the container user has UID=GID=1000 while the GitHub action workdir
has (UID=1001, GID=116).
This is not an issue when relying on `opam` to build the Coq project.
Otherwise, you may want to use `sudo` in the container to change the
permissions. You may also install additional Debian packages.

Typically, this would lead to a workflow specification like this:

```yaml
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
before_script: |
echo Workaround permission issue
sudo chown -R coq:coq . # <--
script: |
make -j2
uninstall: |
make clean
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 . # <--
```

For more details, see the
[CI setup / Remarks](https://github.com/coq-community/docker-coq/wiki/CI-setup#remarks)
section in the `docker-coq` wiki.

#### OPAM

The `docker-coq-action` provides built-in support for `opam` builds.

If your project does not already have a `coq-….opam` file, you might
Expand Down
56 changes: 43 additions & 13 deletions action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,26 +14,56 @@ inputs:
ocaml_version:
description: 'minimal, 4.07-flambda, or 4.09-flambda'
default: 'minimal'
before_install:
description: 'Customizable script run before "install", empty by default.'
default: |
opam config list; opam repo list; opam list
install:
description: 'Customizable script to install the opam dependencies.'
default: |
opam pin add -n -y -k path $PACKAGE $WORKDIR
opam update -y
opam install -y -j 2 $PACKAGE --deps-only
after_install:
description: 'Customizable script run after "install".'
default: |
opam list
before_script:
description: 'Customizable script run before the opam build, empty by default.'
script:
description: 'Customizable script run to install the opam package(s).'
default: |
opam install -y -v -j 2 $PACKAGE
opam list
after_script:
description: 'Customizable script run after the opam build, empty by default.'
uninstall:
description: 'Customizable script run to uninstall the opam package(s).'
default: |
opam remove $PACKAGE
custom_script:
description: 'The main script run in the container; may be overridden.'
default: |
startGroup Print opam config
opam config list; opam repo list; opam list
startGroup before_install dependencies
{{before_install}}
endGroup
startGroup install dependencies
{{install}}
endGroup
startGroup after_install dependencies
{{after_install}}
endGroup
startGroup Build dependencies
opam pin add -n -y -k path $PACKAGE $WORKDIR
opam update -y
opam install -y -j 2 $PACKAGE --deps-only
startGroup before_script
{{before_script}}
endGroup
startGroup List installed packages
opam list
startGroup script
{{script}}
endGroup
startGroup Build
opam install -y -v -j 2 $PACKAGE
opam list
startGroup after_script
{{after_script}}
endGroup
startGroup Uninstallation test
opam remove $PACKAGE
startGroup uninstall
{{uninstall}}
endGroup
custom_image:
description: 'The name of the Docker image to pull; unset by default.'
Expand Down
25 changes: 24 additions & 1 deletion entrypoint.sh
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,29 @@ if printf "%s" "$INPUT_EXPORT" | grep -e '^[a-zA-Z_][a-zA-Z0-9_ ]*$' -q -v; then
exit 1
fi

apk add --no-cache perl

moperl() {
mo="$1"
value="$2"
perl -wpe 'BEGIN {$dest = '\'"$value"\'';}; s/\{\{'"$mo"'\}\}/$dest/g;'
}

INPUT_CUSTOM_SCRIPT_EXPANDED=$(printf "%s" "$INPUT_CUSTOM_SCRIPT" | \
moperl before_install "$INPUT_BEFORE_INSTALL" | \
moperl install "$INPUT_INSTALL" | \
moperl after_install "$INPUT_AFTER_INSTALL" | \
moperl before_script "$INPUT_BEFORE_SCRIPT" | \
moperl script "$INPUT_SCRIPT" | \
moperl after_script "$INPUT_AFTER_SCRIPT" | \
moperl uninstall "$INPUT_UNINSTALL")

if test -z "$INPUT_CUSTOM_SCRIPT_EXPANDED"; then
echo "ERROR: The expanded script is empty."
usage
exit 1
fi

# todo: update this after the one-switch docker-coq migration
OCAML407="false"
if [ "$INPUT_OCAML_VERSION" = '4.09-flambda' ]; then
Expand Down Expand Up @@ -154,6 +177,6 @@ docker run -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e
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" script
$INPUT_CUSTOM_SCRIPT_EXPANDED" script

echo "::remove-matcher owner=coq-problem-matcher::"

0 comments on commit ab40295

Please sign in to comment.