diff --git a/.github/workflows/ci-nix.yml b/.github/workflows/ci-nix.yml deleted file mode 100644 index c1962e5390..0000000000 --- a/.github/workflows/ci-nix.yml +++ /dev/null @@ -1,20 +0,0 @@ -name: Nix -on: - push: - branches: - - master - pull_request: - paths: - - '.github/workflows/ci-nix.yml' - - '**.nix' - - 'flake.lock' - workflow_dispatch: - -jobs: - deploy: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - uses: cachix/install-nix-action@v17 - - name: Build - run: nix build -v --print-build-logs diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 591f1e5bcf..daece42b6b 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -42,7 +42,7 @@ on: ######################################################################## env: - AGDA_BRANCH: v2.6.3 + AGDA_BRANCH: v2.6.4 GHC_VERSION: 9.2.5 CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' diff --git a/CITATION.cff b/CITATION.cff index 2e2e0124f4..407d6f4eef 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.5 -date-released: 2023-07-05 +version: 0.6 +date-released: 2023-10-24 url: "https://github.com/agda/cubical" diff --git a/Cubical/Tactics/Reflection.agda b/Cubical/Tactics/Reflection.agda index 9db131d08c..ba1d3b1a82 100644 --- a/Cubical/Tactics/Reflection.agda +++ b/Cubical/Tactics/Reflection.agda @@ -89,7 +89,7 @@ get-boundary tm = unapply-path tm >>= λ where equation-solver : List Name → (Term -> Term -> TC Term) → Bool → Term → TC Unit equation-solver don't-Reduce mk-call debug hole = withNormalisation false ( - dontReduceDefs don't-Reduce ( + withReduceDefs (false , don't-Reduce) ( do -- | First we normalize the goal goal ← inferType hole >>= reduce diff --git a/README.md b/README.md index 92faa73a1d..9ce7431e45 100644 --- a/README.md +++ b/README.md @@ -12,17 +12,18 @@ 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 release of Agda you can use with which release of this library. +the following table lists which releases of Agda you can use with which release of this library. Agda versions as written below, correspond to tags. -| cubical library version | Agda version | -|-------------------------|----------------| -| `current master` | `v2.6.3` | -| `v0.5` | `v2.6.3` | -| `v0.4` | `v2.6.2.2` | -| `v0.3` | `v2.6.2` | -| `v0.2` | `v2.6.1.3` | -| `v0.1` | `v2.6.0.1` | +| cubical library version | Agda versions | +|-------------------------|-------------------| +| `current master` | `v2.6.4` | +| `v0.6` | `v2.6.4` | +| `v0.5` | `v2.6.3` `v2.6.4` | +| `v0.4` | `v2.6.2.2` | +| `v0.3` | `v2.6.2` | +| `v0.2` | `v2.6.1.3` | +| `v0.1` | `v2.6.0.1` | For example, if you have Agda 2.6.2.2, you can switch to version 0.4 of the cubical library with ``` diff --git a/cubical.agda-lib b/cubical.agda-lib index b9fcbdb627..6565f1c369 100644 --- a/cubical.agda-lib +++ b/cubical.agda-lib @@ -1,4 +1,4 @@ -name: cubical-0.5 +name: cubical-0.6 include: . depend: flags: --cubical --no-import-sorts -WnoUnsupportedIndexedMatch diff --git a/flake.lock b/flake.lock index 2be7b50878..b8510c40ce 100644 --- a/flake.lock +++ b/flake.lock @@ -10,16 +10,16 @@ ] }, "locked": { - "lastModified": 1669235596, - "narHash": "sha256-u4yZPqadMfTnE98c5FKV7yMY3cTehXqjNVZmXPXfkYo=", + "lastModified": 1696540558, + "narHash": "sha256-fqYyjgOFQrU4ryGcLyz5gMYMdPk1P24ra7kQiUrbilg=", "owner": "agda", "repo": "agda", - "rev": "19960e93da5bd775a795a4a3f7c301aceeca645d", + "rev": "f42acb696e43d382639f04f869e9a99ab36a91c6", "type": "github" }, "original": { "owner": "agda", - "ref": "release-2.6.3", + "ref": "v2.6.4", "repo": "agda", "type": "github" } @@ -27,11 +27,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1668681692, - "narHash": "sha256-Ht91NGdewz8IQLtWZ9LCeNXMSXHUss+9COoqu6JLmXU=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "009399224d5e398d03b22badca40a37ac85412a1", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -41,12 +41,15 @@ } }, "flake-utils": { + "inputs": { + "systems": "systems" + }, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -57,11 +60,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1669165918, - "narHash": "sha256-hIVruk2+0wmw/Kfzy11rG3q7ev3VTi/IKVODeHcVjFo=", + "lastModified": 1696757521, + "narHash": "sha256-cfgtLNCBLFx2qOzRLI6DHfqTdfWI+UbvsKYa3b3fvaA=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "3b400a525d92e4085e46141ff48cbf89fd89739e", + "rev": "2646b294a146df2781b1ca49092450e8a32814e1", "type": "github" }, "original": { @@ -77,6 +80,21 @@ "flake-utils": "flake-utils", "nixpkgs": "nixpkgs" } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index cec52b0c13..2d5fcb7c3d 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ flake = false; }; inputs.agda = { - url = "github:agda/agda/v2.6.3"; + url = "github:agda/agda/v2.6.4"; inputs = { nixpkgs.follows = "nixpkgs"; flake-utils.follows = "flake-utils"; @@ -21,7 +21,7 @@ overlay = final: prev: { cubical = final.agdaPackages.mkDerivation rec { pname = "cubical"; - version = "0.5"; + version = "0.6"; src = cleanSourceWith { filter = name: type: