Merge pull request #29 from gallais/upgrade

Upgrade to recent agdarsec & add CI

.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/[email protected]
+        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

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