Skip to content

Fix realizability and Lemmas #426

Fix realizability and Lemmas

Fix realizability and Lemmas #426

Workflow file for this run

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