ci_build.yaml

name: CI build
on:
  push:
    branches:
      - main
      - ext/**
  pull_request:
    branches:
      - main
      - ext/**
  workflow_dispatch:
      
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:
      actions: write
      packages: read
      contents: write
    env:
      REGISTRY: "ghcr.io"
      IMAGE_TAG: "beluga-lang/mctt:main"
      # Only deploy if the build follows from pushing to one of main branches
      DOC_DEPLOY: ${{ (github.ref_name == 'main' || startsWith(github.ref_name, 'ext/')) && 'true' || 'false' }}
      DOC_DEPLOY_DEST: ${{ startsWith(github.ref_name, 'ext/') && github.ref_name || '' }}
    steps:
      - name: Get number of CPU cores
        uses: SimenB/github-actions-cpu-cores@v2
        id: cpu-cores

      - name: Checkout repo
        uses: actions/checkout@v4
          
      - name: Log in container registry
        uses: docker/login-action@v3
        with:
          registry: ${{ env.REGISTRY }}
          username: ${{ github.actor }}
          password: ${{ secrets.GITHUB_TOKEN }}

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

      - name: Process main steps
        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
            endGroup
            startGroup "Build HTMLs for GitHub pages"
              if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
                make coqdoc
                DOC_BASE="${{ env.DOC_DEPLOY_DEST }}" make depgraphdoc
                mv theories/html html
                mv theories/dep.html html/dep.html
                cp assets/styling.css html/styling.css
                cp -r assets/images html/images
                sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McTT/dep\.html)![Coqdoc](dep.html)!' README.md
                pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McTT: Building A Correct-By-Construction Proof Checkers For Type Theories' -t html --css styling.css -o html/index.html
              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: Revert permissions
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .

      - name: Deploy GitHub pages
        uses: JamesIves/github-pages-deploy-action@v4
        if: ${{ env.DOC_DEPLOY == 'true' }}
        with:
          folder: html
          target-folder: ${{ env.DOC_DEPLOY_DEST }}
          clean-exclude: ext