Skip to content

isSet for Grammars, Monoidal Category of grammars, finish Dyck Trace Equivalence #68

isSet for Grammars, Monoidal Category of grammars, finish Dyck Trace Equivalence

isSet for Grammars, Monoidal Category of grammars, finish Dyck Trace Equivalence #68

Workflow file for this run

# This is a basic workflow to help you get started with Actions
name: CI
# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the "main" branch
push:
branches:
- main
- impl
paths-ignore:
- 'paper/*'
- 'notes/*'
pull_request:
branches:
- main
paths-ignore:
- 'paper/*'
- 'notes/*'
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
########################################################################
## CONFIGURATION
##
## See SETTINGS for the most important configuration variable: AGDA_BRANCH.
## It has to be defined as a build step because it is potentially branch
## dependent.
##
## As for the rest:
##
## Basically do not touch GHC_VERSION and CABAL_VERSION as long as
## they aren't a problem in the build. If you have time to waste, it
## could be worth investigating whether newer versions of ghc produce
## more efficient Agda executable and could cut down the build time.
## Just be aware that actions are flaky and small variations are to be
## expected.
##
## The CABAL_INSTALL variable only passes `-O1` optimisations to ghc
## because github actions cannot currently handle a build using `-O2`.
## To be experimented with again in the future to see if things have
## gotten better.
##
########################################################################
########################################################################
## SETTINGS
##
## AGDA_BRANCH picks the branch of Agda to use to build the library.
## It doesn't really track the branch, so you have to drop caches to
## get a new branch version if it changes. This will be fixed in the
## next PR.
########################################################################
env:
AGDA_BRANCH: v2.7.0.1
GHC_VERSION: 9.8.2
CABAL_VERSION: 3.10.2.1
CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
CACHE_PATHS: |
~/.cabal/packages
~/.cabal/store
~/.cabal/bin
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
check-whitespace:
runs-on: ubuntu-latest
steps:
- name: Install cabal
uses: haskell-actions/setup@v2
with:
ghc-version: ${{ env.GHC_VERSION }}
cabal-version: ${{ env.CABAL_VERSION }}
cabal-update: true
########################################################################
## INSTALLATION STEPS
########################################################################
- name: Download and install fix-whitespace
run: |
cd ~
git clone https://github.com/agda/fix-whitespace --depth=1
cd fix-whitespace
${{ env.CABAL_INSTALL }} fix-whitespace.cabal
cd ..
########################################################################
## CHECKOUT
########################################################################
# By default github actions do not pull the repo
- name: Checkout grammars-and-semantic-actions
uses: actions/checkout@v3
########################################################################
## TESTING
########################################################################
- name: Test whitespace
run: |
~/.cabal/bin/fix-whitespace --check
compile-agda:
runs-on: ubuntu-latest
steps:
- name: Install cabal
uses: haskell-actions/setup@v2
with:
ghc-version: ${{ env.GHC_VERSION }}
cabal-version: ${{ env.CABAL_VERSION }}
cabal-update: true
########################################################################
## INSTALLATION STEPS
########################################################################
- name: Download and install Agda from github
run: |
git clone https://github.com/agda/agda --branch ${{ env.AGDA_BRANCH }} --depth=1
cd agda
mkdir -p doc
touch doc/user-manual.pdf
${{ env.CABAL_INSTALL }}
cd ..
rm -rf agda
- name: Download Cubical from github
run : |
cd ~
git clone https://github.com/agda/cubical --branch master
cd cubical
git checkout 581748b01bc43a25295993347bdc8c7cb2166090
cd ..
echo "CUBICAL_DIR=$PWD/cubical" >> "$GITHUB_ENV"
- name: Download categorical-logic from github
run : |
cd ~
git clone https://github.com/maxsnew/cubical-categorical-logic --branch master
cd cubical-categorical-logic
git checkout 295cc5defa414b861959f89f52325e098b9db6ec
cd ..
echo "CATLOG_DIR=$PWD/cubical-categorical-logic" >> "$GITHUB_ENV"
- name: Set up Agda dependencies
run : |
mkdir ~/.agda
touch ~/.agda/libraries
echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
echo "$CATLOG_DIR/cubical.agda-lib" >> ~/.agda/libraries
echo "$GITHUB_WORKSPACE/code/cubical/grammar.agda-lib" >> ~/.agda/libraries
########################################################################
## CHECKOUT
########################################################################
# By default github actions do not pull the repo
- name: Checkout grammars-and-semantic-actions
uses: actions/checkout@v3
########################################################################
## TESTING
########################################################################
- name: Put cabal programs in PATH
run: echo "~/.cabal/bin" >> $GITHUB_PATH
- name: Test grammars-and-semantic-actions
run: |
cd code/cubical && make quicktest \
AGDA='~/.cabal/bin/agda +RTS -M6G -RTS -WnoUnsupportedIndexedMatch -W error' \