Skip to content

Build TypeTheory

Build TypeTheory #197

name: Build TypeTheory
on:
push:
branches: [master]
pull_request:
branches: [master]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
schedule:
# Based on https://github.com/marketplace/actions/set-up-ocaml
# Prime the caches every Monday
- cron: '0 3 * * MON'
env:
DUNE_CACHE_STORAGE_MODE: copy
jobs:
build-typetheory:
strategy:
fail-fast: false
matrix:
coq-version: [dev, latest, 8.16]
ocaml-version: [4.14-flambda]
name: Build with ${{ matrix.coq-version }}
runs-on: ubuntu-22.04
steps:
# Checkout UniMath in the current directory.
- name: Checkout UniMath
uses: actions/checkout@v4
with:
repository: UniMath/UniMath
path: .
clean: false
# Checkout TypeTheory in TypeTheory/
- name: Checkout TypeTheory
uses: actions/checkout@v4
with:
path: TypeTheory
# Grab the cache if available. We tell dune to use $(pwd)/dune-cache/ in
# the custom_script below.
- uses: actions/cache@v4
with:
path: dune-cache
key: TypeTheory-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
restore-keys: |
TypeTheory-coq-${{ matrix.coq-version }}-${{ github.run_id }}
TypeTheory-coq-${{ matrix.coq-version }}
TypeTheory-coq
- name: Build TypeTheory
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.coq-version }}
ocaml_version: ${{ matrix.ocaml-version }}
custom_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
startGroup "Print versions"
opam --version
opam exec -- dune --version
opam exec -- coqc --version
endGroup
startGroup "Build TypeTheory"
export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
opam exec -- dune build TypeTheory --display=short \
--cache=enabled --error-reporting=twice
endGroup
- name: Revert permissions
if: ${{ always() }}
run: sudo chown -R 1001:116 .