ci_build.yaml

name: CI build
on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main
  workflow_dispatch:
  
permissions:
  actions: write
  contents: write

env:
  REGISTRY: "ghcr.io"
  IMAGE_TAG: "beluga-lang/mcltt:main"
      
jobs:
  wf:
    name: Completeness of _CoqProject
    runs-on: ubuntu-latest
    steps:
      - name: repo checkout
        uses: actions/checkout@v4
      - name: check
        run: |
          .github/scripts/check_projects.sh theories

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

      - name: repo checkout
        uses: actions/checkout@v4
        
      - name: Initialise variables
        run: |
          # Only deploy if the build follows from pushing to master
          if [[ '${{ github.ref }}' == 'refs/heads/main' ]]; then
             echo "DOC_DEPLOY=true" >> $GITHUB_ENV
          else
             echo "DOC_DEPLOY=false" >> $GITHUB_ENV
          fi
          
      - name: container registry log in
        uses: docker/login-action@v3
        with:
          registry: ${{ env.REGISTRY }}
          username: ${{ github.actor }}
          password: ${{ secrets.GITHUB_TOKEN }}

      - name: image pre-pulling
        run: docker pull ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }}

      - name: coq processing
        uses: coq-community/docker-coq-action@v1
        with:
          custom_image: ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }}
          install: |
          before_script: |
            startGroup "Fix the permission issue"
              sudo chown -R coq:coq .
            endGroup
          script: |
            startGroup "Build binary"
              make pretty-timed
              if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
                make coqdoc
              fi
            endGroup
            startGroup "Run inline tests"
              dune runtest
            endGroup
          after_script: |
            startGroup "after"
            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 .

      - name: generate Github pages
        if: ${{ success() && env.DOC_DEPLOY == 'true' }}
        run: |
          sudo apt install -y pandoc
          mv theories/html html
          cp assets/styling.css html/styling.css
          cp -r assets/images html/images
          pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McLTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html

      - name: Deploy HTML
        uses: JamesIves/github-pages-deploy-action@v4.6.4
        if: ${{ success() && env.DOC_DEPLOY == 'true' }}
        with:
          branch: gh-pages
          folder: html