merge #282
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI build | |
| on: | |
| push: | |
| branches: | |
| - main | |
| - ext/** | |
| pull_request: | |
| branches: | |
| - main | |
| - ext/** | |
| 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/[email protected] | |
| if: ${{ success() && env.DOC_DEPLOY == 'true' }} | |
| with: | |
| branch: gh-pages | |
| folder: html |