ci_build.yaml

name: CI build
on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main

env:
  OCAML_VER: "4.14.1-flambda"
  COQ_VER: "8.17.1"
  REGISTRY: ghcr.io
      
jobs:
  wf:
    name: Completeness of _CoqProject
    runs-on: ubuntu-latest
    steps:
      - name: repo checkout
        uses: actions/checkout@v3
      - name: check
        run: |
          .github/scripts/check_projects.sh theories

  build:
    name: Continuous Intergration
    runs-on: ubuntu-latest
    permissions:
      contents: read
      packages: write
      attestations: write
      id-token: write
    steps:
      - name: get number of CPU cores
        uses: SimenB/github-actions-cpu-cores@v2
        id: cpu-cores

      - name: repo checkout
        uses: actions/checkout@v3

      - name: registry login
        run: echo "${{ secrets.GITHUB_TOKEN }}" | docker login ghcr.io -u ${{ github.actor }} --password-stdin

      - name: registry login
        run: docker pull ${{ env.REGISTRY }}/beluga-lang/mcltt:main

      - name: coq processing
        uses: coq-community/docker-coq-action@v1
        with:
          custom_image: ${{ env.REGISTRY }}/beluga-lang/mcltt:main
          install: |
          before_script: |
            startGroup "Fix the permission issue"
              sudo chown -R coq:coq .
            endGroup
          script: |
            startGroup "Build Coq lib"
              cd theories/
              make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
            endGroup
          after_script: |
            startGroup "Test parser"
              dune build
              dune runtest
            endGroup
          export: "OPAMJOBS OPAMYES"
        env:
          OPAMJOBS: ${{ steps.cpu-cores.outputs.count }}
          OPAMYES: "true"

      - name: permissions revert
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .