From db4163611ec4b29a6dd20a4729223a3044e1d047 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 21 Jul 2023 13:04:52 -0300 Subject: [PATCH 1/9] Put indexed data types in the right universe To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default. There is an infective flag `--large-indices` to bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with `--no-large-indices` instead of adding the flag to the modules that used them. --- src/Data/Star/Decoration.agda | 2 +- src/Data/Star/Pointer.agda | 2 +- src/Reflection/Annotated.agda | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda index 24428a5843..170b5abb07 100644 --- a/src/Data/Star/Decoration.agda +++ b/src/Data/Star/Decoration.agda @@ -28,7 +28,7 @@ data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r) -- Decorating an edge with more information. data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T) - : Rel (NonEmpty (Star T)) p where + : Rel (NonEmpty (Star T)) (ℓ ⊔ r ⊔ p) where ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs) diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda index 6214e3e7dc..70dfdb94be 100644 --- a/src/Data/Star/Pointer.agda +++ b/src/Data/Star/Pointer.agda @@ -21,7 +21,7 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive data Pointer {r p q} {T : Rel I r} (P : EdgePred p T) (Q : EdgePred q T) - : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where + : Rel (Maybe (NonEmpty (Star T))) (ℓ ⊔ r ⊔ p ⊔ q) where step : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs))) (just (nonEmpty xs)) diff --git a/src/Reflection/Annotated.agda b/src/Reflection/Annotated.agda index ba63faf0fb..171dfe75c4 100644 --- a/src/Reflection/Annotated.agda +++ b/src/Reflection/Annotated.agda @@ -35,8 +35,8 @@ Annotation : ∀ ℓ → Set (suc ℓ) Annotation ℓ = ∀ {u} → ⟦ u ⟧ → Set ℓ -- An annotated type is a family over an Annotation and a reflected term. -Typeₐ : ∀ ℓ → Univ → Set (suc ℓ) -Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set ℓ +Typeₐ : ∀ ℓ → Univ → Set (suc (suc ℓ)) +Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set (suc ℓ) private variable @@ -168,7 +168,7 @@ mutual -- An annotation function computes the top-level annotation given a -- term annotated at all sub-terms. -AnnotationFun : Annotation ℓ → Set ℓ +AnnotationFun : Annotation ℓ → Set (suc ℓ) AnnotationFun Ann = ∀ u {t : ⟦ u ⟧} → Annotated′ Ann t → Ann t From c38f1409cd826e881a835945129a2032e770298e Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 10 Oct 2023 10:45:02 +0200 Subject: [PATCH 2/9] Prepare for v1.7.3: move CHANGELOG to CHANGELOG/v1.7.2 --- CHANGELOG.md => CHANGELOG/v1.7.2.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename CHANGELOG.md => CHANGELOG/v1.7.2.md (100%) diff --git a/CHANGELOG.md b/CHANGELOG/v1.7.2.md similarity index 100% rename from CHANGELOG.md rename to CHANGELOG/v1.7.2.md From 2f2c413d4adcb854f25a865d578e929020d82d5b Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 10 Oct 2023 10:48:05 +0200 Subject: [PATCH 3/9] v1.7.3 CHANGELOG entry for `--large-indices` (#2030) --- CHANGELOG.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 CHANGELOG.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000000..0b05a15bbd --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,11 @@ +Version 1.7.3 +============= + +The library has been tested using Agda 2.6.4. + +* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4, + universe levels have been increased in the following definitions: + - `Data.Star.Decoration.DecoratedWith` + - `Data.Star.Pointer.Pointer` + - `Reflection.AnnotatedAST.Typeₐ` + - `Reflection.AnnotatedAST.AnnotationFun` From 84c16c18813941c981b8df8816b36f061af982fc Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 10 Oct 2023 11:02:47 +0200 Subject: [PATCH 4/9] Bump agda-stdlib-utils to 1.7.3; update its dependencies and CI --- .github/workflows/haskell-ci.yml | 180 +++++++++++++++++++++++-------- agda-stdlib-utils.cabal | 16 +-- 2 files changed, 146 insertions(+), 50 deletions(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 3eef98ae73..871f408c65 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -6,79 +6,144 @@ # # haskell-ci regenerate # -# For more information, see https://github.com/haskell-CI/haskell-ci +# For more information, see https://github.com/andreasabel/haskell-ci # -# version: 0.12.1 +# version: 0.17.20231002 # -# REGENDATA ("0.12.1",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) +# REGENDATA ("0.17.20231002",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) # name: Haskell-CI on: - push: - branches: - - master - - experimental - pull_request: - branches: - - master - - experimental + - push + - pull_request jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }} - runs-on: ubuntu-18.04 + runs-on: ubuntu-20.04 + timeout-minutes: + 60 container: - image: buildpack-deps:xenial + image: buildpack-deps:focal continue-on-error: ${{ matrix.allow-failure }} strategy: matrix: include: - - compiler: ghc-9.0.1 + - compiler: ghc-9.8.0.20230929 + compilerKind: ghc + compilerVersion: 9.8.0.20230929 + setup-method: ghcup + allow-failure: true + - compiler: ghc-9.6.3 + compilerKind: ghc + compilerVersion: 9.6.3 + setup-method: ghcup allow-failure: false - - compiler: ghc-8.10.4 + - compiler: ghc-9.4.7 + compilerKind: ghc + compilerVersion: 9.4.7 + setup-method: ghcup + allow-failure: false + - compiler: ghc-9.2.8 + compilerKind: ghc + compilerVersion: 9.2.8 + setup-method: ghcup + allow-failure: false + - compiler: ghc-9.0.2 + compilerKind: ghc + compilerVersion: 9.0.2 + setup-method: ghcup + allow-failure: false + - compiler: ghc-8.10.7 + compilerKind: ghc + compilerVersion: 8.10.7 + setup-method: ghcup allow-failure: false - compiler: ghc-8.8.4 + compilerKind: ghc + compilerVersion: 8.8.4 + setup-method: hvr-ppa allow-failure: false - compiler: ghc-8.6.5 + compilerKind: ghc + compilerVersion: 8.6.5 + setup-method: hvr-ppa allow-failure: false - compiler: ghc-8.4.4 + compilerKind: ghc + compilerVersion: 8.4.4 + setup-method: hvr-ppa allow-failure: false - compiler: ghc-8.2.2 + compilerKind: ghc + compilerVersion: 8.2.2 + setup-method: hvr-ppa allow-failure: false - compiler: ghc-8.0.2 + compilerKind: ghc + compilerVersion: 8.0.2 + setup-method: hvr-ppa allow-failure: false fail-fast: false steps: - name: apt run: | apt-get update - apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common - apt-add-repository -y 'ppa:hvr/ghc' - apt-get update - apt-get install -y $CC cabal-install-3.4 + apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5 + if [ "${{ matrix.setup-method }}" = ghcup ]; then + mkdir -p "$HOME/.ghcup/bin" + curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup" + chmod a+x "$HOME/.ghcup/bin/ghcup" + "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml; + "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false) + "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false) + else + apt-add-repository -y 'ppa:hvr/ghc' + apt-get update + apt-get install -y "$HCNAME" + mkdir -p "$HOME/.ghcup/bin" + curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup" + chmod a+x "$HOME/.ghcup/bin/ghcup" + "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml; + "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false) + fi env: - CC: ${{ matrix.compiler }} + HCKIND: ${{ matrix.compilerKind }} + HCNAME: ${{ matrix.compiler }} + HCVER: ${{ matrix.compilerVersion }} - name: Set PATH and environment variables run: | echo "$HOME/.cabal/bin" >> $GITHUB_PATH - echo "LANG=C.UTF-8" >> $GITHUB_ENV - echo "CABAL_DIR=$HOME/.cabal" >> $GITHUB_ENV - echo "CABAL_CONFIG=$HOME/.cabal/config" >> $GITHUB_ENV - HCDIR=$(echo "/opt/$CC" | sed 's/-/\//') - HCNAME=ghc - HC=$HCDIR/bin/$HCNAME - echo "HC=$HC" >> $GITHUB_ENV - echo "HCPKG=$HCDIR/bin/$HCNAME-pkg" >> $GITHUB_ENV - echo "HADDOCK=$HCDIR/bin/haddock" >> $GITHUB_ENV - echo "CABAL=/opt/cabal/3.4/bin/cabal -vnormal+nowrap" >> $GITHUB_ENV + echo "LANG=C.UTF-8" >> "$GITHUB_ENV" + echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV" + echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV" + HCDIR=/opt/$HCKIND/$HCVER + if [ "${{ matrix.setup-method }}" = ghcup ]; then + HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER") + HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#') + HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#') + echo "HC=$HC" >> "$GITHUB_ENV" + echo "HCPKG=$HCPKG" >> "$GITHUB_ENV" + echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV" + echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.1.0 -vnormal+nowrap" >> "$GITHUB_ENV" + else + HC=$HCDIR/bin/$HCKIND + echo "HC=$HC" >> "$GITHUB_ENV" + echo "HCPKG=$HCDIR/bin/$HCKIND-pkg" >> "$GITHUB_ENV" + echo "HADDOCK=$HCDIR/bin/haddock" >> "$GITHUB_ENV" + echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.1.0 -vnormal+nowrap" >> "$GITHUB_ENV" + fi + HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))') - echo "HCNUMVER=$HCNUMVER" >> $GITHUB_ENV - echo "ARG_TESTS=--enable-tests" >> $GITHUB_ENV - echo "ARG_BENCH=--enable-benchmarks" >> $GITHUB_ENV - echo "HEADHACKAGE=false" >> $GITHUB_ENV - echo "ARG_COMPILER=--$HCNAME --with-compiler=$HC" >> $GITHUB_ENV - echo "GHCJSARITH=0" >> $GITHUB_ENV + echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV" + echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV" + echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV" + if [ $((HCNUMVER >= 90800)) -ne 0 ] ; then echo "HEADHACKAGE=true" >> "$GITHUB_ENV" ; else echo "HEADHACKAGE=false" >> "$GITHUB_ENV" ; fi + echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV" + echo "GHCJSARITH=0" >> "$GITHUB_ENV" env: - CC: ${{ matrix.compiler }} + HCKIND: ${{ matrix.compilerKind }} + HCNAME: ${{ matrix.compiler }} + HCVER: ${{ matrix.compilerVersion }} - name: env run: | env @@ -101,6 +166,22 @@ jobs: repository hackage.haskell.org url: http://hackage.haskell.org/ EOF + if $HEADHACKAGE; then + cat >> $CABAL_CONFIG <> $CABAL_CONFIG < cabal-plan.xz - echo 'de73600b1836d3f55e32d80385acc055fd97f60eaa0ab68a755302685f5d81bc cabal-plan.xz' | sha256sum -c - + curl -sL https://github.com/haskell-hvr/cabal-plan/releases/download/v0.7.3.0/cabal-plan-0.7.3.0-x86_64-linux.xz > cabal-plan.xz + echo 'f62ccb2971567a5f638f2005ad3173dba14693a45154c1508645c52289714cb2 cabal-plan.xz' | sha256sum -c - xz -d < cabal-plan.xz > $HOME/.cabal/bin/cabal-plan rm -f cabal-plan.xz chmod a+x $HOME/.cabal/bin/cabal-plan cabal-plan --version - name: checkout - uses: actions/checkout@v2 + uses: actions/checkout@v4 with: path: source - name: initial cabal.project for sdist @@ -139,7 +220,8 @@ jobs: - name: generate cabal.project run: | PKGDIR_agda_stdlib_utils="$(find "$GITHUB_WORKSPACE/unpacked" -maxdepth 1 -type d -regex '.*/agda-stdlib-utils-[0-9.]*')" - echo "PKGDIR_agda_stdlib_utils=${PKGDIR_agda_stdlib_utils}" >> $GITHUB_ENV + echo "PKGDIR_agda_stdlib_utils=${PKGDIR_agda_stdlib_utils}" >> "$GITHUB_ENV" + rm -f cabal.project cabal.project.local touch cabal.project touch cabal.project.local echo "packages: ${PKGDIR_agda_stdlib_utils}" >> cabal.project @@ -147,6 +229,9 @@ jobs: if [ $((HCNUMVER >= 80200)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi cat >> cabal.project <> cabal.project + fi $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(agda-stdlib-utils)$/; }' >> cabal.project.local cat cabal.project cat cabal.project.local @@ -154,8 +239,8 @@ jobs: run: | $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH --dry-run all cabal-plan - - name: cache - uses: actions/cache@v2 + - name: restore cache + uses: actions/cache/restore@v3 with: key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }} path: ~/.cabal/store @@ -170,7 +255,16 @@ jobs: - name: build run: | $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --write-ghc-environment-files=always + - name: haddock + run: | + $CABAL v2-haddock --disable-documentation --haddock-all $ARG_COMPILER --with-haddock $HADDOCK $ARG_TESTS $ARG_BENCH all - name: unconstrained build run: | rm -f cabal.project.local $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all + - name: save cache + uses: actions/cache/save@v3 + if: always() + with: + key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }} + path: ~/.cabal/store diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index 6e8bc7b33b..6cabbb5b2b 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -1,5 +1,5 @@ name: agda-stdlib-utils -version: 1.7.2 +version: 1.7.3 cabal-version: >= 1.10 build-type: Simple description: Helper programs. @@ -11,24 +11,26 @@ tested-with: GHC == 8.0.2 GHC == 8.8.4 GHC == 8.10.7 GHC == 9.0.2 - GHC == 9.2.1 - GHC == 9.4.4 + GHC == 9.2.8 + GHC == 9.4.7 + GHC == 9.6.3 + GHC == 9.8.0 executable GenerateEverything hs-source-dirs: . main-is: GenerateEverything.hs default-language: Haskell2010 default-extensions: PatternGuards, PatternSynonyms - build-depends: base >= 4.9.0.0 && < 4.18 + build-depends: base >= 4.9.0.0 && < 4.20 , directory >= 1.0.0.0 && < 1.4 , filemanip >= 0.3.6.2 && < 0.4 , filepath >= 1.4.1.0 && < 1.5 - , mtl >= 2.2.2 && < 2.3 + , mtl >= 2.2.2 && < 2.4 executable AllNonAsciiChars hs-source-dirs: . main-is: AllNonAsciiChars.hs default-language: Haskell2010 - build-depends: base >= 4.9.0.0 && < 4.18 + build-depends: base >= 4.9.0.0 && < 4.20 , filemanip >= 0.3.6.2 && < 0.4 - , text >= 1.2.3.0 && < 2.1 + , text >= 1.2.3.0 && < 2.2 From 3f869a309ab03ba1e4f6cccc41fd292943b20cb2 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 10 Oct 2023 11:05:52 +0200 Subject: [PATCH 5/9] Update CI for v1.7.3: Use Agda 2.6.4; deploy HTML to v1.7.3 subdirectory Also: - install alex and happy - bump Agda heap to -M6G --- .github/workflows/ci-ubuntu.yml | 49 ++++++++++++--------------------- 1 file changed, 17 insertions(+), 32 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 70773cd832..b602f65748 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -1,13 +1,7 @@ name: Ubuntu build on: push: - branches: - - master - - experimental pull_request: - branches: - - master - - experimental ######################################################################## ## CONFIGURATION @@ -46,11 +40,11 @@ on: ######################################################################## env: - GHC_VERSION: 8.6.5 - CABAL_VERSION: 3.2.0.0 + GHC_VERSION: 9.6.3 + CABAL_VERSION: 3.10.1.0 CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' # 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/ + AGDA: agda -Werror +RTS -M6G -H3.5G -A128M -RTS -i. -i src/ jobs: test-stdlib: @@ -71,22 +65,10 @@ jobs: - name: Initialise variables run: | - if [[ '${{ github.ref }}' == 'refs/heads/master' \ - || '${{ github.base_ref }}' == 'master' ]]; then - # Pick Agda version for master - echo "AGDA_COMMIT=tags/v2.6.1.3.20210524" >> $GITHUB_ENV; - echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV - elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \ - || '${{ github.base_ref }}' == 'experimental' ]]; then - # Pick Agda version for experimental - echo "AGDA_COMMIT=9047e32a1b0cba98a299ed439a08d35bc4846f99" >> $GITHUB_ENV; - echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV - fi - - if [[ '${{ github.ref }}' == 'refs/heads/master' \ - || '${{ github.ref }}' == 'refs/heads/experimental' ]]; then - echo "AGDA_DEPLOY=true" >> $GITHUB_ENV - fi + echo "AGDA_COMMIT=tags/v2.6.4" >> "$GITHUB_ENV" + echo "AGDA_HTML_DIR=html/v1.7.3" >> "$GITHUB_ENV" + echo "AGDA_DEPLOY=true" >> "$GITHUB_ENV" + ######################################################################## ## CACHING @@ -98,7 +80,7 @@ jobs: # 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 + uses: actions/cache@v3 id: cache-cabal with: path: | @@ -113,16 +95,19 @@ jobs: - name: Install cabal if: steps.cache-cabal.outputs.cache-hit != 'true' - uses: actions/setup-haskell@v1.1.3 + uses: haskell-actions/setup@v2 with: ghc-version: ${{ env.GHC_VERSION }} cabal-version: ${{ env.CABAL_VERSION }} + cabal-update: true - name: Put cabal programs in PATH - run: echo "~/.cabal/bin" >> $GITHUB_PATH + run: echo "~/.cabal/bin" >> "$GITHUB_PATH" - - name: Cabal update - run: cabal update + - name: Install alex and happy + if: steps.cache-cabal.outputs.cache-hit != 'true' + run: | + ${{ env.CABAL_INSTALL }} alex happy - name: Download and install Agda from github if: steps.cache-cabal.outputs.cache-hit != 'true' @@ -141,7 +126,7 @@ jobs: # By default github actions do not pull the repo - name: Checkout stdlib - uses: actions/checkout@v2 + uses: actions/checkout@v4 - name: Test stdlib run: | @@ -188,4 +173,4 @@ jobs: with: branch: gh-pages folder: html - git-config-name: Github Actions \ No newline at end of file + git-config-name: Github Actions From d883ecced61b2a0cc7403dc8140dbd3a8fd5bc36 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 11 Oct 2023 11:54:19 +0200 Subject: [PATCH 6/9] Bump Haskell CI to GHC 9.8.1; bump deploy action; only branch release-1.7.3-base Restricting to branch release-1.7.3-base will hopefully stop duplicate CI runs. --- .github/workflows/ci-ubuntu.yml | 6 +++++- .github/workflows/haskell-ci.yml | 35 +++++++++++--------------------- agda-stdlib-utils.cabal | 2 +- cabal.haskell-ci | 1 + 4 files changed, 19 insertions(+), 25 deletions(-) create mode 100644 cabal.haskell-ci diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index b602f65748..1bf5ae836d 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -1,7 +1,11 @@ name: Ubuntu build on: push: + branches: + - release-1.7.3-base pull_request: + branches: + - release-1.7.3-base ######################################################################## ## CONFIGURATION @@ -167,7 +171,7 @@ jobs: - name: Deploy HTML - uses: JamesIves/github-pages-deploy-action@4.1.3 + uses: JamesIves/github-pages-deploy-action@v4 if: ${{ success() && env.AGDA_DEPLOY }} with: diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 871f408c65..064b6865a1 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -8,14 +8,18 @@ # # For more information, see https://github.com/andreasabel/haskell-ci # -# version: 0.17.20231002 +# version: 0.17.20231010 # -# REGENDATA ("0.17.20231002",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) +# REGENDATA ("0.17.20231010",["github","--no-cabal-check","agda-stdlib-utils.cabal"]) # name: Haskell-CI on: - - push - - pull_request + push: + branches: + - release-1.7.3-base + pull_request: + branches: + - release-1.7.3-base jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }} @@ -28,11 +32,11 @@ jobs: strategy: matrix: include: - - compiler: ghc-9.8.0.20230929 + - compiler: ghc-9.8.1 compilerKind: ghc - compilerVersion: 9.8.0.20230929 + compilerVersion: 9.8.1 setup-method: ghcup - allow-failure: true + allow-failure: false - compiler: ghc-9.6.3 compilerKind: ghc compilerVersion: 9.6.3 @@ -137,7 +141,7 @@ jobs: echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV" echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV" echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV" - if [ $((HCNUMVER >= 90800)) -ne 0 ] ; then echo "HEADHACKAGE=true" >> "$GITHUB_ENV" ; else echo "HEADHACKAGE=false" >> "$GITHUB_ENV" ; fi + echo "HEADHACKAGE=false" >> "$GITHUB_ENV" echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV" echo "GHCJSARITH=0" >> "$GITHUB_ENV" env: @@ -166,18 +170,6 @@ jobs: repository hackage.haskell.org url: http://hackage.haskell.org/ EOF - if $HEADHACKAGE; then - cat >> $CABAL_CONFIG <> $CABAL_CONFIG <= 80200)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi cat >> cabal.project <> cabal.project - fi $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(agda-stdlib-utils)$/; }' >> cabal.project.local cat cabal.project cat cabal.project.local diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal index 6cabbb5b2b..b3860888ab 100644 --- a/agda-stdlib-utils.cabal +++ b/agda-stdlib-utils.cabal @@ -14,7 +14,7 @@ tested-with: GHC == 8.0.2 GHC == 9.2.8 GHC == 9.4.7 GHC == 9.6.3 - GHC == 9.8.0 + GHC == 9.8.1 executable GenerateEverything hs-source-dirs: . diff --git a/cabal.haskell-ci b/cabal.haskell-ci new file mode 100644 index 0000000000..ec3b597c83 --- /dev/null +++ b/cabal.haskell-ci @@ -0,0 +1 @@ +branches: release-1.7.3-base \ No newline at end of file From d622fa5d3b471875ff3d2ee88407566e7e6fff3c Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 11 Oct 2023 12:06:55 +0200 Subject: [PATCH 7/9] Add CITATION.cff; bump version to 1.7.3 bump to 1.7.3 in - standard-library.agda-lib - README.agda - installation-guide.txt --- CITATION.cff | 8 ++++++++ README.agda | 4 ++-- notes/installation-guide.md | 12 ++++++------ standard-library.agda-lib | 2 +- 4 files changed, 17 insertions(+), 9 deletions(-) create mode 100644 CITATION.cff diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000000..78e63bd810 --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,8 @@ +cff-version: 1.2.0 +message: "If you use this software, please cite it as below." +authors: +- name: "The Agda Community" +title: "Agda Standard Library" +version: 1.7.3 +date-released: 2023-10-15 +url: "https://github.com/agda/agda-stdlib" \ No newline at end of file diff --git a/README.agda b/README.agda index 1406d70967..1b5bc7f351 100644 --- a/README.agda +++ b/README.agda @@ -3,7 +3,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 1.7.2 +-- The Agda standard library, version 1.7.3 -- -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais -- with contributions from Andreas Abel, Stevan Andjelkovic, @@ -18,7 +18,7 @@ module README where -- Noam Zeilberger and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.2. +-- This version of the library has been tested using Agda 2.6.4. -- The library comes with a .agda-lib file, for use with the library -- management system. diff --git a/notes/installation-guide.md b/notes/installation-guide.md index e51088aa6a..0086700170 100644 --- a/notes/installation-guide.md +++ b/notes/installation-guide.md @@ -1,19 +1,19 @@ Installation instructions ========================= -Use version v1.7.2 of the standard library with Agda 2.6.2. +Use version v1.7.3 of the standard library with Agda 2.6.4. 1. Navigate to a suitable directory `$HERE` (replace appropriately) where you would like to install the library. -2. Download the tarball of v1.7.2 of the standard library. This can either be +2. Download the tarball of v1.7.3 of the standard library. This can either be done manually by visiting the Github repository for the library, or via the command line as follows: ``` - wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.2.tar.gz + wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.3.tar.gz ``` Note that you can replace `wget` with other popular tools such as `curl` and that - you can replace `1.7.2` with any other version of the library you desire. + you can replace `1.7.3` with any other version of the library you desire. 3. Extract the standard library from the tarball. Again this can either be done manually or via the command line as follows: @@ -24,14 +24,14 @@ Use version v1.7.2 of the standard library with Agda 2.6.2. 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run the commands to install via cabal: ``` - cd agda-stdlib-1.7.2 + cd agda-stdlib-1.7.3 cabal install ``` 5. Register the standard library with Agda's package system by adding the following line to `$HOME/.agda/libraries`: ``` - $HERE/agda-stdlib-1.7.2/standard-library.agda-lib + $HERE/agda-stdlib-1.7.3/standard-library.agda-lib ``` Now, the standard library is ready to be used either: diff --git a/standard-library.agda-lib b/standard-library.agda-lib index 29885b7c5c..4f40cf4b61 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,4 +1,4 @@ -name: standard-library-1.7.2 +name: standard-library-1.7.3 include: src flags: --warning=noUnsupportedIndexedMatch From 3d2002b9bd7d23390b766cd5945710fe775a6beb Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Wed, 11 Oct 2023 13:34:35 +0200 Subject: [PATCH 8/9] CI: always fresh cache key --- .github/workflows/ci-ubuntu.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 1bf5ae836d..c8f3e3f4d2 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -91,7 +91,10 @@ jobs: ~/.cabal/packages ~/.cabal/store ~/.cabal/bin - key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }} + key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}- + ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}- ######################################################################## ## INSTALLATION STEPS From 44bd3be0b44ff57470cebfe5ab8a9c1ff649a02d Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Thu, 12 Oct 2023 14:50:46 +0200 Subject: [PATCH 9/9] Add some aliases for forward compatibility with v2.0 Some objects will get a new name in v2.0. We add some of these names already here to ease the transition to v2.0: - add modules `Effect.*` reexporting `Category.*` - add `IO.Primitive.pure` as alias for `IO.Primitive.return` --- CHANGELOG.md | 7 +++++++ src/Effect/Applicative.agda | 12 ++++++++++++ src/Effect/Applicative/Indexed.agda | 12 ++++++++++++ src/Effect/Applicative/Predicate.agda | 12 ++++++++++++ src/Effect/Comonad.agda | 12 ++++++++++++ src/Effect/Functor.agda | 12 ++++++++++++ src/Effect/Functor/Indexed.agda | 12 ++++++++++++ src/Effect/Functor/Predicate.agda | 12 ++++++++++++ src/Effect/Monad.agda | 12 ++++++++++++ src/Effect/Monad/Continuation.agda | 12 ++++++++++++ src/Effect/Monad/Indexed.agda | 12 ++++++++++++ src/Effect/Monad/Partiality.agda | 12 ++++++++++++ src/Effect/Monad/Partiality/All.agda | 12 ++++++++++++ src/Effect/Monad/Partiality/Instances.agda | 12 ++++++++++++ src/Effect/Monad/Predicate.agda | 12 ++++++++++++ src/Effect/Monad/Reader.agda | 12 ++++++++++++ src/Effect/Monad/State.agda | 12 ++++++++++++ src/IO/Primitive.agda | 3 +++ 18 files changed, 202 insertions(+) create mode 100644 src/Effect/Applicative.agda create mode 100644 src/Effect/Applicative/Indexed.agda create mode 100644 src/Effect/Applicative/Predicate.agda create mode 100644 src/Effect/Comonad.agda create mode 100644 src/Effect/Functor.agda create mode 100644 src/Effect/Functor/Indexed.agda create mode 100644 src/Effect/Functor/Predicate.agda create mode 100644 src/Effect/Monad.agda create mode 100644 src/Effect/Monad/Continuation.agda create mode 100644 src/Effect/Monad/Indexed.agda create mode 100644 src/Effect/Monad/Partiality.agda create mode 100644 src/Effect/Monad/Partiality/All.agda create mode 100644 src/Effect/Monad/Partiality/Instances.agda create mode 100644 src/Effect/Monad/Predicate.agda create mode 100644 src/Effect/Monad/Reader.agda create mode 100644 src/Effect/Monad/State.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 0b05a15bbd..8de9bf14ee 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,3 +9,10 @@ The library has been tested using Agda 2.6.4. - `Data.Star.Pointer.Pointer` - `Reflection.AnnotatedAST.Typeₐ` - `Reflection.AnnotatedAST.AnnotationFun` + +* The following aliases have been added: + - `IO.Primitive.pure` as alias for `IO.Primitive.return` + - modules `Effect.*` as aliases for modules `Category.*` + + These allow to address said objects with the new name they will have in v2.0 of the library, + to ease the transition from v1.7.3 to v2.0. diff --git a/src/Effect/Applicative.agda b/src/Effect/Applicative.agda new file mode 100644 index 0000000000..859131b8a6 --- /dev/null +++ b/src/Effect/Applicative.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative where + +open import Category.Applicative public diff --git a/src/Effect/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda new file mode 100644 index 0000000000..58a7c6418a --- /dev/null +++ b/src/Effect/Applicative/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative.Indexed where + +open import Category.Applicative.Indexed public diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda new file mode 100644 index 0000000000..b28c57598f --- /dev/null +++ b/src/Effect/Applicative/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Applicative.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Applicative.Predicate where + +open import Category.Applicative.Predicate public diff --git a/src/Effect/Comonad.agda b/src/Effect/Comonad.agda new file mode 100644 index 0000000000..45ea111c5a --- /dev/null +++ b/src/Effect/Comonad.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Comonad` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Comonad where + +open import Category.Comonad public diff --git a/src/Effect/Functor.agda b/src/Effect/Functor.agda new file mode 100644 index 0000000000..5c276929b6 --- /dev/null +++ b/src/Effect/Functor.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor where + +open import Category.Functor public diff --git a/src/Effect/Functor/Indexed.agda b/src/Effect/Functor/Indexed.agda new file mode 100644 index 0000000000..9d4efdef1f --- /dev/null +++ b/src/Effect/Functor/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor.Indexed where + +open import Category.Functor.Indexed public diff --git a/src/Effect/Functor/Predicate.agda b/src/Effect/Functor/Predicate.agda new file mode 100644 index 0000000000..a11b2cef64 --- /dev/null +++ b/src/Effect/Functor/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Functor.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Functor.Predicate where + +open import Category.Functor.Predicate public diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda new file mode 100644 index 0000000000..c4df178be8 --- /dev/null +++ b/src/Effect/Monad.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad where + +open import Category.Monad public diff --git a/src/Effect/Monad/Continuation.agda b/src/Effect/Monad/Continuation.agda new file mode 100644 index 0000000000..357102eef6 --- /dev/null +++ b/src/Effect/Monad/Continuation.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Continuation` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Continuation where + +open import Category.Monad.Continuation public diff --git a/src/Effect/Monad/Indexed.agda b/src/Effect/Monad/Indexed.agda new file mode 100644 index 0000000000..8bed8e27eb --- /dev/null +++ b/src/Effect/Monad/Indexed.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Indexed` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Indexed where + +open import Category.Monad.Indexed public diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda new file mode 100644 index 0000000000..80783e6148 --- /dev/null +++ b/src/Effect/Monad/Partiality.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality where + +open import Category.Monad.Partiality public diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda new file mode 100644 index 0000000000..f91e83b6d5 --- /dev/null +++ b/src/Effect/Monad/Partiality/All.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality.All` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality.All where + +open import Category.Monad.Partiality.All public diff --git a/src/Effect/Monad/Partiality/Instances.agda b/src/Effect/Monad/Partiality/Instances.agda new file mode 100644 index 0000000000..aa322c83ab --- /dev/null +++ b/src/Effect/Monad/Partiality/Instances.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Partiality.Instances` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Partiality.Instances where + +open import Category.Monad.Partiality.Instances public diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda new file mode 100644 index 0000000000..56d6dbe0a4 --- /dev/null +++ b/src/Effect/Monad/Predicate.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Predicate` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Predicate where + +open import Category.Monad.Predicate public diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda new file mode 100644 index 0000000000..78d05ae0de --- /dev/null +++ b/src/Effect/Monad/Reader.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.Reader` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.Reader where + +open import Category.Monad.Reader public diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda new file mode 100644 index 0000000000..14ffbf6b5c --- /dev/null +++ b/src/Effect/Monad/State.agda @@ -0,0 +1,12 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- This module duplicates `Category.Monad.State` +-- for forward compatibility with v2.0. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Effect.Monad.State where + +open import Category.Monad.State public diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index 45ae1b5fc5..a0e15a3c5d 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -27,3 +27,6 @@ postulate {-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-} {-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-} {-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-} + +-- Forward compatibility with v2.0. +pure = return