Vertical Terminal Objects, some naming updates (#83) #251
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
| # 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 | |
| paths-ignore: | |
| - 'README.org' | |
| - 'Notes/*' | |
| pull_request: | |
| branches: | |
| - main | |
| paths-ignore: | |
| - 'README.org' | |
| - '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.6.4 | |
| GHC_VERSION: 9.4.7 | |
| CABAL_VERSION: 3.6.2.0 | |
| 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: | |
| line-lengths: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Set up Python 3.8 | |
| uses: actions/setup-python@v2 | |
| with: | |
| python-version: 3.8 | |
| - name: Install dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install wcwidth | |
| - name: Check line lengths | |
| run: 'make check-line-lengths' | |
| 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 | |
| # This caching step allows us to save a lot of building time by only | |
| # rebuilding Agda, and re-checking unchanged library files if | |
| # absolutely necessary i.e. if we change either the version of Agda, | |
| # ghc, or cabal that we want to use for the build. | |
| - name: Restore external dependencies cache | |
| uses: actions/cache/restore@v3 | |
| id: cache-external-restore | |
| with: | |
| path: ${{ env.CACHE_PATHS }} | |
| key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }} | |
| ######################################################################## | |
| ## INSTALLATION STEPS | |
| ######################################################################## | |
| - name: Download and install Agda from github | |
| if: steps.cache-external-restore.outputs.cache-hit != 'true' | |
| 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 Agda Standard Library from github | |
| run : | | |
| cd ~ | |
| git clone https://github.com/agda/agda-stdlib.git | |
| echo "AGDA_STDLIB_DIR=$PWD/agda-stdlib" >> "$GITHUB_ENV" | |
| - name: Download Cubical from github | |
| run : | | |
| cd ~ | |
| git clone https://github.com/agda/cubical --branch master | |
| cd cubical | |
| git checkout 2ae84643c74750b49865e44c05b508cb2117c740 | |
| cd .. | |
| echo "CUBICAL_DIR=$PWD/cubical" >> "$GITHUB_ENV" | |
| - name: Set up Agda dependencies | |
| run : | | |
| mkdir ~/.agda | |
| touch ~/.agda/libraries | |
| echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries | |
| echo "$AGDA_STDLIB_DIR/standard-library.agda-lib" >> ~/.agda/libraries | |
| echo "$GITHUB_WORKSPACE/cubical-categorical-logic.agda-lib" >> ~/.agda/libraries | |
| - name: Download and install fix-whitespace | |
| if: steps.cache-external-restore.outputs.cache-hit != 'true' | |
| run: | | |
| cd ~ | |
| git clone https://github.com/agda/fix-whitespace --depth=1 | |
| cd fix-whitespace | |
| ${{ env.CABAL_INSTALL }} fix-whitespace.cabal | |
| cd .. | |
| - name: Cache External Dependencies | |
| if: steps.cache-external-restore.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v3 | |
| id: cache-external-save | |
| with: | |
| path: ${{ env.CACHE_PATHS }} | |
| key: ${{ steps.cache-external-restore.outputs.cache-primary-key }} | |
| ######################################################################## | |
| ## CHECKOUT | |
| ######################################################################## | |
| # By default github actions do not pull the repo | |
| - name: Checkout cubical-categorical-logic | |
| uses: actions/checkout@v3 | |
| ######################################################################## | |
| ## TESTING | |
| ######################################################################## | |
| - name: Put cabal programs in PATH | |
| run: echo "~/.cabal/bin" >> $GITHUB_PATH | |
| - name: Cache Agdai Files | |
| uses: actions/cache@v3 | |
| with: | |
| path: '**/*.agdai' | |
| key: ${{ runner.os }}-agdai-${{ hashFiles('**/*.agda') }} | |
| restore-keys: | | |
| ${{ runner.os }}-agdai- | |
| - name: Test cubical-categorical-logic | |
| run: | | |
| make test \ | |
| AGDA='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \ | |
| FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' |