diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index d8b3b347c4..011f755977 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -42,9 +42,9 @@ on: ######################################################################## env: - AGDA_BRANCH: v2.6.4.1 - GHC_VERSION: 9.4.7 - CABAL_VERSION: 3.6.2.0 + AGDA_BRANCH: v2.7.0.1 + GHC_VERSION: 9.10.2 + CABAL_VERSION: 3.12.1.0 CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' CACHE_PATHS: | ~/.cabal/packages @@ -67,7 +67,7 @@ jobs: # 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 + uses: actions/cache/restore@v4 id: cache-external-restore with: path: ${{ env.CACHE_PATHS }} @@ -82,23 +82,13 @@ jobs: 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 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@v3 + uses: actions/cache/save@v4 id: cache-external-save with: path: ${{ env.CACHE_PATHS }} @@ -110,14 +100,17 @@ jobs: # By default github actions do not pull the repo - name: Checkout cubical - uses: actions/checkout@v3 + uses: actions/checkout@v4 + + - name: Get and run fix-whitespace + uses: andreasabel/fix-whitespace-action@v1 ######################################################################## ## TESTING ######################################################################## - name: Restore library cache - uses: actions/cache/restore@v3 + uses: actions/cache/restore@v4 id: cache-library-restore with: path: ./_build @@ -125,19 +118,19 @@ jobs: restore-keys: | library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}- - - name: Put cabal programs in PATH + - name: Put installed programs in PATH run: echo "~/.cabal/bin" >> "${GITHUB_PATH}" - name: Test cubical run: | make test \ AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \ - FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \ + FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \ EVERYTHINGS='cabal run Everythings' - name: Save library cache if: steps.cache-library-restore.outputs.cache-hit != 'true' - uses: actions/cache/save@v3 + uses: actions/cache/save@v4 id: cache-library-save with: path: ./_build @@ -152,12 +145,12 @@ jobs: run: | make listings \ AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \ - FIX_WHITESPACE='~/.cabal/bin/fix-whitespace' \ + FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \ EVERYTHINGS='cabal run Everythings' - name: Deploy to GitHub Pages if: github.event_name == 'push' && github.ref_name == 'master' - uses: JamesIves/github-pages-deploy-action@4.1.8 + uses: JamesIves/github-pages-deploy-action@v4 with: branch: gh-pages folder: html diff --git a/CITATION.cff b/CITATION.cff index 048a89cdaf..da5f7ddd2c 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below." authors: - name: "The Agda Community" title: "Cubical Agda Library" -version: 0.7 -date-released: 2024-02-12 +version: 0.8 +date-released: 2025-05-09 url: "https://github.com/agda/cubical" diff --git a/README.md b/README.md index 384c186946..7b34cd241f 100644 --- a/README.md +++ b/README.md @@ -12,12 +12,14 @@ For detailed install instructions see the [INSTALL](https://github.com/agda/cubical/blob/master/INSTALL.md) file. If you want to use some specific release of Agda, -the following table lists which releases of Agda you can use with which release of this library. +the following table lists which releases of Agda are known to work with which release of this library. +Most likely, a lot more combinations work as well. Agda versions as written below, correspond to tags. | cubical library version | Agda versions | |-------------------------|--------------------------------| -| current master | `v2.6.4` `v2.6.4.1` `v2.6.4.3` | +| current master | `v2.7.0.1` | +| `v0.8` | `v2.6.4.1` `v2.7.0.1` | | `v0.7` | `v2.6.4` `v2.6.4.1` | | `v0.6` | `v2.6.4` | | `v0.5` | `v2.6.3` `v2.6.4` | diff --git a/RELEASE.md b/RELEASE.md index a96f8d306f..758f6814d8 100644 --- a/RELEASE.md +++ b/RELEASE.md @@ -43,3 +43,5 @@ Fill in the form with something like this: zip -r cubical-0.5.zip cubical tar cfz cubical-0.5.tar.gz cubical ``` + +Create and push a tag for the new version of the library. diff --git a/cubical-utils.cabal b/cubical-utils.cabal index 42464c3d07..a684fc4595 100644 --- a/cubical-utils.cabal +++ b/cubical-utils.cabal @@ -4,11 +4,11 @@ cabal-version: >= 1.10 build-type: Simple description: Helper programs. license: MIT -tested-with: GHC == 8.6.5 +tested-with: GHC == 9.10.2 executable Everythings hs-source-dirs: . main-is: Everythings.hs default-language: Haskell2010 - build-depends: base >= 4.9.0.0 && < 4.20 + build-depends: base >= 4.9.0.0 && < 4.22 , directory >= 1.0.0.0 && < 1.4 diff --git a/cubical.agda-lib b/cubical.agda-lib index 064f900d4c..85499ce6c6 100644 --- a/cubical.agda-lib +++ b/cubical.agda-lib @@ -1,4 +1,4 @@ -name: cubical-0.7 +name: cubical-0.8 include: . depend: flags: --cubical --no-import-sorts -WnoUnsupportedIndexedMatch diff --git a/flake.lock b/flake.lock index 6fa40f03e7..b66b947314 100644 --- a/flake.lock +++ b/flake.lock @@ -2,24 +2,22 @@ "nodes": { "agda": { "inputs": { - "flake-utils": [ - "flake-utils" - ], + "flake-parts": "flake-parts", "nixpkgs": [ "nixpkgs" ] }, "locked": { - "lastModified": 1701366566, - "narHash": "sha256-B8Jmjld0gGbkVO08GsovVqrUXCs8VfJ8UdM3sjHnzgM=", + "lastModified": 1726161230, + "narHash": "sha256-IupM/HJk1vpHTRWOakYDDliKn+RLzPjNzGlLTlF0CbY=", "owner": "agda", "repo": "agda", - "rev": "4293e0a94d15acac915ab9088b2ec028f78d14a9", + "rev": "a6fc20c27ae953149b53a8997ba4a1c8b17d628a", "type": "github" }, "original": { "owner": "agda", - "ref": "v2.6.4.1", + "ref": "v2.7.0.1", "repo": "agda", "type": "github" } @@ -27,11 +25,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1696426674, - "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "lastModified": 1747046372, + "narHash": "sha256-CIVLLkVgvHYbgI2UpXvIIBJ12HWgX+fjA8Xf8PUmqCY=", "owner": "edolstra", "repo": "flake-compat", - "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "rev": "9100a0f413b0c601e0533d1d94ffd501ce2e7885", "type": "github" }, "original": { @@ -40,16 +38,34 @@ "type": "github" } }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1701473968, + "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" }, "locked": { - "lastModified": 1705309234, - "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -60,11 +76,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1705883077, - "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=", + "lastModified": 1747426788, + "narHash": "sha256-N4cp0asTsJCnRMFZ/k19V9akkxb7J/opG+K+jU57JGc=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9", + "rev": "12a55407652e04dcf2309436eb06fef0d3713ef3", "type": "github" }, "original": { @@ -73,6 +89,24 @@ "type": "indirect" } }, + "nixpkgs-lib": { + "locked": { + "dir": "lib", + "lastModified": 1701253981, + "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58", + "type": "github" + }, + "original": { + "dir": "lib", + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "agda": "agda", diff --git a/flake.nix b/flake.nix index 42f1b1beae..3db1690054 100644 --- a/flake.nix +++ b/flake.nix @@ -8,10 +8,9 @@ flake = false; }; inputs.agda = { - url = "github:agda/agda/v2.6.4.1"; + url = "github:agda/agda/v2.7.0.1"; inputs = { nixpkgs.follows = "nixpkgs"; - flake-utils.follows = "flake-utils"; }; }; @@ -21,7 +20,7 @@ overlay = final: prev: { cubical = final.agdaPackages.mkDerivation rec { pname = "cubical"; - version = "0.7"; + version = "0.8"; src = cleanSourceWith { filter = name: type: @@ -47,7 +46,7 @@ }; agdaWithCubical = final.agdaPackages.agda.withPackages [final.cubical]; }; - overlays = [ agda.overlay overlay ]; + overlays = [ agda.overlays.default overlay ]; in { overlays.default = overlay; } // flake-utils.lib.eachDefaultSystem (system: