From 60f1195793dfa251f78d838146801550ff4f50ca Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Mon, 21 Jun 2021 16:34:54 +0100 Subject: [PATCH 1/2] [ ci ] using github actions --- .github/workflows/ci-ubuntu.yml | 163 ++++++++++++++++++++++++++++++++ 1 file changed, 163 insertions(+) create mode 100644 .github/workflows/ci-ubuntu.yml diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml new file mode 100644 index 0000000..ba287ac --- /dev/null +++ b/.github/workflows/ci-ubuntu.yml @@ -0,0 +1,163 @@ +name: Ubuntu build +on: + push: + branches: + - master + pull_request: + branches: + - master + +######################################################################## +## CONFIGURATION +## +## Key variables: +## +## AGDA_COMMIT picks the version of Agda to use to build the library. +## It can either be a hash of a specific commit (to target a bugfix for +## instance) or a tag e.g. tags/v2.6.1.3 (to target a released version). +## +## STDLIB_VERSION picks the version of the stdlib to pull. The current +## design requires that the number corresponds to a released version +## but we could change that to a commit-based approach if you need to. +## +## AGDARSEC_COMMIT picks the commit of agdarsec to use. Just like +## AGDA_COMMIT it can either be a hash of a specific commit or a tag. +## +## 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. +## +## The AGDA variable specifies the command to use to build the library. +## It currently passes the flag `-Werror` to ensure maximal compliance +## with e.g. not relying on deprecated definitions. +## The rest are some arbitrary runtime arguments that shape the way Agda +## allocates and garbage collects memory. It should make things faster. +## Limits can be bumped if the builds start erroring with out of memory +## errors. +## +######################################################################## + +env: + AGDA_COMMIT: tags/v2.6.2 + STDLIB_VERSION: 1.7 + AGDARSEC_VERSION: fd6e7de75bd0215065cec25c81e911352a86191d + + GHC_VERSION: 8.6.5 + CABAL_VERSION: 3.2.0.0 + CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' + AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/ + +jobs: + test-schmitty: + runs-on: ubuntu-latest + steps: + +######################################################################## +## SETTINGS +######################################################################## + + - name: Initialise variables + run: | + # Only deploy if the build follows from pushing to master + if [[ '${{ github.ref }}' == 'refs/heads/master' ]]; then + echo "AGDA_DEPLOY=true" >> $GITHUB_ENV + fi + + # The script won't be able to find Agda if we don't tell it to look at the + # content of ~/.cabal/bin + - name: Put cabal programs in PATH + run: echo "~/.cabal/bin" >> $GITHUB_PATH + +######################################################################## +## CACHING +######################################################################## + + # This caching step allows us to save a lot of building time by only + # downloading ghc and cabal and rebuilding Agda 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: Cache cabal packages + uses: actions/cache@v2 + id: cache-cabal + with: + path: | + ~/.cabal/packages + ~/.cabal/store + ~/.cabal/bin + key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }} + +######################################################################## +## INSTALLATION STEPS +######################################################################## + + - name: Install ghc and cabal + if: steps.cache-cabal.outputs.cache-hit != 'true' + uses: actions/setup-haskell@v1.1.3 + with: + ghc-version: ${{ env.GHC_VERSION }} + cabal-version: ${{ env.CABAL_VERSION }} + + - name: Cabal update + if: steps.cache-cabal.outputs.cache-hit != 'true' + run: cabal update + + - name: Download and install Agda from github + if: steps.cache-cabal.outputs.cache-hit != 'true' + run: | + git clone https://github.com/agda/agda + cd agda + git checkout ${{ env.AGDA_COMMIT }} + mkdir -p doc + touch doc/user-manual.pdf + ${{ env.CABAL_INSTALL }} + cd .. + + - name: Install stdlib + run: | + mkdir -p $HOME/.agda + cd $HOME/.agda + wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz + tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz + mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib + echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries + cd $HOME + + - name: Install agdarsec + run: | + cd $HOME/.agda + git clone https://github.com/gallais/agdarsec + cd agdarsec + git checkout ${{ env.AGDARSEC_COMMIT }} + cd .. + echo "~/.agda/agdarsec/agdarsec.agda-lib" >> libraries + cd $HOME + + - name: Install z3 + run: | + sudo apt-get -y install z3 + +######################################################################## +## TESTING +######################################################################## + + # By default github actions do not pull the repo + - name: Checkout schmitty + uses: actions/checkout@v2 + + - name: Test schmitty + run: | + echo "/usr/bin/z3" >> $HOME/.agda/executables + # The counter models returned by failing tests can vary depending + # on the SMT solver being used so we only run the successful tests + # on the CI. + AGDA="~/.cabal/bin/agda" make test-succeed From 949a4296734a14ef58e48cf56d32e6bee77b1ca7 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Mon, 21 Jun 2021 16:36:13 +0100 Subject: [PATCH 2/2] [ fix ] agdarsec imports The upstream library has been refactored so we need to slightly change the imports. --- src/Text/Parser/String.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Text/Parser/String.agda b/src/Text/Parser/String.agda index 10d0593..f7986f4 100644 --- a/src/Text/Parser/String.agda +++ b/src/Text/Parser/String.agda @@ -32,7 +32,9 @@ open import Data.Subset public open import Level.Bounded as Bounded using ([_]) import Text.Parser.Monad as ParserMonad -open import Text.Parser.Types as Parser using (_^_,_) +import Text.Parser.Monad.Result as ParserMonad +import Text.Parser.Types as Parser +open import Text.Parser.Types.Core as Parser using (_^_,_) import Text.Parser.Position as Position