acquire total orders + add strict&trichotomous orders (#56) #614
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
| ## Adapted from the agda/agda-stdlib workflow | |
| name: Ubuntu build | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| ######################################################################## | |
| ## CONFIGURATION | |
| ## | |
| ## See SETTINGS for the most important configuration variable: `agda-tag`. | |
| ## It has to be defined as a build step because it is potentially tag | |
| ## 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. | |
| ## | |
| ######################################################################## | |
| env: | |
| 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 | |
| jobs: | |
| test-cubical: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| agda-tag: [ nightly , v2.7.0.1 ] | |
| steps: | |
| - name: Install cabal | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| ghc-version: ${{ env.ghc-version }} | |
| cabal-version: ${{ env.cabal-version }} | |
| cabal-update: true | |
| - name: Get latest commit hash on agda-tag | |
| uses: octokit/[email protected] | |
| id: agda-tag-commit-hash | |
| with: | |
| route: GET /repos/agda/agda/git/ref/tags/${{ matrix.agda-tag }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # This caching step allows us to save a lot of building time by only | |
| # downloading ghc and cabal, 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@v4 | |
| id: cache-external-restore | |
| with: | |
| path: ${{ env.cache-paths }} | |
| key: ${{ runner.os }}-${{ env.ghc-version }}-${{ env.cabal-version }}-${{ env.agda-tag-hash }} | |
| env: | |
| agda-tag-hash: ${{ fromJson(steps.agda-tag-commit-hash.outputs.data).object.sha }} | |
| ######################################################################## | |
| ## 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 ${{ matrix.agda-tag }} --depth=1 | |
| cd agda | |
| mkdir -p doc | |
| touch doc/user-manual.pdf | |
| ${{ env.cabal-install }} | |
| cd .. | |
| rm -rf agda | |
| - name: Download and install fix-whitespace | |
| if: steps.cache-external-restore.outputs.cache-hit != 'true' | |
| run: | | |
| git clone https://github.com/agda/fix-whitespace --depth=1 | |
| cd fix-whitespace | |
| ${{ env.cabal-install }} fix-whitespace.cabal | |
| cd .. | |
| - name: Save external dependencies cache | |
| if: steps.cache-external-restore.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| 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 | |
| uses: actions/checkout@v4 | |
| ######################################################################## | |
| ## TESTING | |
| ######################################################################## | |
| - name: Restore library cache | |
| uses: actions/cache/restore@v4 | |
| id: cache-library-restore | |
| with: | |
| path: ./_build | |
| key: | |
| library-${{ runner.os }}-${{ env.ghc-version }}-${{ env.cabal-version }}-${{ env.agda-tag-hash }}-${{ hashFiles('src/**', 'cubical-mini.agda-lib') }} | |
| restore-keys: | | |
| library-${{ runner.os }}-${{ env.ghc-version }}-${{ env.cabal-version }}-${{ env.agda-tag-hash }}- | |
| env: | |
| agda-tag-hash: ${{ fromJson(steps.agda-tag-commit-hash.outputs.data).object.sha }} | |
| - name: Put cabal programs in PATH | |
| run: echo "~/.cabal/bin" >> $GITHUB_PATH | |
| - name: Test cubical | |
| if: steps.cache-library-restore.outputs.cache-hit != 'true' | |
| run: | | |
| make test \ | |
| AGDA_EXEC='~/.cabal/bin/agda' \ | |
| FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \ | |
| EVERYTHINGS='cabal run Everythings' | |
| - name: Save library cache | |
| if: steps.cache-library-restore.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| id: cache-library-save | |
| with: | |
| path: ./_build | |
| key: ${{ steps.cache-library-restore.outputs.cache-primary-key }} | |
| ######################################################################## | |
| ## HTML GENERATION | |
| ######################################################################## | |
| - name: Htmlize cubical | |
| if: | | |
| github.event_name == 'push' && github.ref_name == 'master' && | |
| matrix.agda-tag == 'nightly' && steps.cache-library-restore.outputs.cache-hit != 'true' | |
| run: | | |
| make listings \ | |
| AGDA_EXEC='~/.cabal/bin/agda' \ | |
| FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \ | |
| EVERYTHINGS='cabal run Everythings' | |
| - name: Deploy to GitHub Pages | |
| if: | | |
| github.event_name == 'push' && github.ref_name == 'master' && | |
| matrix.agda-tag == 'nightly' && steps.cache-library-restore.outputs.cache-hit != 'true' | |
| uses: JamesIves/[email protected] | |
| with: | |
| branch: gh-pages | |
| folder: html | |
| ######################################################################## | |
| ## FULL SOURCE CODE RELEASE GENERATION | |
| ######################################################################## | |
| - name: Generate full source archive | |
| if: | | |
| github.event_name == 'push' && github.ref_name == 'master' && | |
| matrix.agda-tag == 'nightly' && steps.cache-library-restore.outputs.cache-hit != 'true' | |
| run: | | |
| make gen-everythings \ | |
| AGDA_EXEC='~/.cabal/bin/agda' \ | |
| FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \ | |
| EVERYTHINGS='cabal run Everythings' | |
| tar czf cm-full-source.tar.gz *.md LICENSE fix-whitespace.yaml cubical-mini.agda-lib src/ | |
| - name: Update Nightly Release | |
| if: | | |
| github.event_name == 'push' && github.ref_name == 'master' && | |
| matrix.agda-tag == 'nightly' && steps.cache-library-restore.outputs.cache-hit != 'true' | |
| uses: andelf/nightly-release@main | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| tag_name: nightly | |
| name: 'nightly-$$' | |
| prerelease: true | |
| files: | | |
| ./cm-full-source.tar.gz |