coq-demo.yml

name: Docker-Coq CI
on:
  push:
    branches:
      - master  # forall push/merge in master
      - v1      # forall push/merge in v1
  pull_request:
    branches:
      - "**"  # forall submitted Pull Requests
  schedule:
  # test master every day at 16:00 UTC
  # cf. https://crontab.guru/
    - cron: '0 16 * * *'

jobs:

  # The following two jobs are standard/recommended versions, assuming
  # your coq project repository contains a committed .opam file.

  demo-1:
    name: coq_version / docker-coq / opam
    runs-on: ubuntu-latest
    strategy:
      matrix:
        # To get the list of supported (coq, ocaml) versions from coqorg/coq,
        # see https://github.com/coq-community/docker-coq/wiki#supported-tags
        coq_version:
          - '8.18'
          - 'latest-native'
          - 'dev'
        ocaml_version: ['default']
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          coq_version: ${{ matrix.coq_version }}
          ocaml_version: ${{ matrix.ocaml_version }}

  demo-2:
    name: custom_image / docker-mathcomp / opam
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'mathcomp/mathcomp-dev:coq-dev'
          - 'mathcomp/mathcomp:latest-coq-8.19'
          # - 'mathcomp/mathcomp:latest-coq-dev'  # not always available,
          # see https://hub.docker.com/r/mathcomp/mathcomp#supported-tags
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          custom_image: ${{ matrix.image }}

  # The following job illustrates the use of several customizable fields,
  # while keeping the default value of the overall "custom_script" field,
  # see https://github.com/coq-community/docker-coq-action#custom_script

  demo-3:
    name: custom_image / docker-coq / make / script
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          # TODO: Update as soon as Rocq 9.0.0 goes live
          - 'coqorg/coq:latest'
          - 'rocq/rocq-prover:dev'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          # As the install/script/uninstall fields are overridden,
          # the "opam_file" field is unneeded in this example job.
          custom_image: ${{ matrix.image }}
          install: |
            startGroup "Install dependencies"
              opam install -y -j 2 coq-mathcomp-ssreflect
            endGroup
          before_script: |
            startGroup "Workaround permission issue"
              sudo chown -R coq:coq .
            endGroup
          script: |
            startGroup "Build project"
              coq_makefile -f _CoqProject -o Makefile
              make -j2
              make test
              make install
            endGroup
          uninstall: |
            startGroup "Clean project"
              make clean
              make uninstall
            endGroup
      - name: Revert permissions
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .

  # The following job illustrates the redefinition of the
  # "custom_script" field.
  
  demo-4:
    name: custom_image / docker-coq / make / custom_script
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:latest'
          - 'rocq/rocq-prover:dev'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          custom_image: ${{ matrix.image }}
          custom_script: |
            startGroup "Print opam config"
              opam config list; opam repo list; opam list
            endGroup
            startGroup "Install dependencies"
              opam update -y
              opam install -y -j 2 coq-mathcomp-ssreflect
            endGroup
            startGroup "List installed packages"
              opam list
            endGroup
            startGroup "Workaround permission issue"
              sudo chown -R coq:coq .
            endGroup
            startGroup "Build project"
              coq_makefile -f _CoqProject -o Makefile
              make -j2
              make test
              make install
            endGroup
            startGroup "Clean project"
              make clean
              make uninstall
            endGroup
      - name: Revert permissions
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .

  # The following job illustrates how to pass environment variables.

  demo-5:
    name: custom_image / docker-coq / opam / env
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:latest'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          custom_image: ${{ matrix.image }}
          before_script: |
            startGroup "Toy example"
              echo "COQ_IMAGE=$COQ_IMAGE"
              [ -n "$COQ_IMAGE" ]
              echo "ex_var=$ex_var"
              [ "$ex_var" = "ex_value" ]
            endGroup
          export: 'COQ_IMAGE ex_var OPAMWITHTEST'  # space-sep. list of vars
        env:
          OPAMWITHTEST: 'true'
          ex_var: 'ex_value'

  # The following two jobs illustrate the installation of system packages.

  demo-6:
    name: custom_image / docker-coq / opam / auto install depexts
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'rocq/rocq-prover:dev'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-depexts-test.opam'
          custom_image: ${{ matrix.image }}
          after_script: |
            startGroup "Post-test"
              gappa --version
            endGroup

  demo-7:
    name: custom_image / docker-coq / opam / apt-get install more
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:latest'
          - 'rocq/rocq-prover:dev'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          custom_image: ${{ matrix.image }}
          before_script: |
            startGroup "Install APT dependencies"
              cat /etc/os-release
              # sudo apt-get update -y -q # this mandatory command is already run in install step by default
              sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends \
                emacs \
                tree  # for instance
                # Alphabetical order is recommended for long package lists to ease review and update
            endGroup
          after_script: |
            startGroup "Post-test"
              emacs --version
              tree
            endGroup

  # The following job illustrates the upload of generated artifacts.

  demo-8:
    name: custom_image / docker-coq / opam+make / upload-artifacts
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:latest'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          custom_image: ${{ matrix.image }}
          before_script: |
            startGroup "Workaround permission issue"
              sudo chown -R coq:coq .
            endGroup
          script: |
            startGroup "Build project"
              coq_makefile -f _CoqProject -o Makefile
              make -j2
            endGroup
          after_script: |
            set -o pipefail  # recommended if the script uses pipes

            startGroup "Build artifacts"
              mkdir -v -p artifacts
              opam list > artifacts/opam_list.txt
              make test 2>&1 | tee artifacts/make_test.txt
            endGroup
          uninstall: ''
      - name: Revert permissions
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .
      - uses: actions/upload-artifact@v4
        with:
          name: example-artifact
          path: artifacts/
          if-no-files-found: error  # 'warn' or 'ignore' are also available, defaults to `warn`
          retention-days: 8


  # The following job illustrates the upload of github environment files.

  demo-9:
    name: custom_image / docker-mathcomp / opam / env+GITHUB_ENV
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'mathcomp/mathcomp:latest-coq-8.19'
      fail-fast: false  # don't stop jobs if one fails
    steps:
      ################################################################
      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
      #                    # if you copy this demo workflow elsewhere!
      - uses: actions/checkout@v4
        with:
          repository: 'erikmd/docker-coq-github-action-demo'
          ref: 'master'
      - uses: actions/checkout@v4
        with:
          path: 'docker-coq-action'
      - uses: './docker-coq-action'
        # End GHA_TEST_ENV
        ##################
        # - uses: actions/checkout@v4
        # - uses: coq-community/docker-coq-action@v1
        id: docker-coq-action
        env:
          # Pass string data to docker-coq-action
          after_ok: 'Test successful!'
        with:
          export: 'COQ_IMAGE after_ok'
          custom_image: ${{ matrix.image }}
          opam_file: 'coq-demo.opam'
          before_script: |
            # Pass step outputs (Docker image name) to next step
            echo "docker_image=$COQ_IMAGE" >> "$GITHUB_OUTPUT"
          after_script: |
            # Pass env vars (Coq version string...) to next step
            echo "coq_version=$(opam var coq:version)" >> "$GITHUB_ENV"
            echo "some_variable=expected_value" >> "$GITHUB_ENV"
            # Display Markdown summary
            [ -n "$after_ok" ]
            echo "### $after_ok :rocket:" >> "$GITHUB_STEP_SUMMARY"
      - name: Next step
        env:
          docker_image: ${{ steps.docker-coq-action.outputs.docker_image }}
        run: |
          : Summary
          echo "Previous step pulled Docker image: $docker_image"
          [ -n "$docker_image" ]
          echo "Previous step used: coq_version=$coq_version"
          [ -n "$coq_version" ]
          echo "some_variable=$some_variable"
          [ "$some_variable" = "expected_value" ]