From 6ebe52b1caf6925bdcc885017935d01c82d6f45e Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 13:25:13 +0100 Subject: [PATCH 01/14] remove 'suggested' heap size from RTS options in makefile The suggested heap size also seems to set a maximum. I don't why we have a suggested heap size anyway, so I just removed that, since make failed with agda 2.6.4.1, compiled with ghc 9.8.1. --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 6e58efd832..d91ba8a724 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS=+RTS -H6G -RTS +RTS_OPTIONS= # +RTS $OPTIONS -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From f519d9459dce48c82d17d1112936b7dacd2390ae Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 15:00:44 +0100 Subject: [PATCH 02/14] incease agda version, see if it fails --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 5129d5ff2b..d8b3b347c4 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -42,7 +42,7 @@ on: ######################################################################## env: - AGDA_BRANCH: v2.6.4 + AGDA_BRANCH: v2.6.4.1 GHC_VERSION: 9.4.7 CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' From 3195827e1392757d9b50adc400bf42cba0d96678 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 17:44:47 +0100 Subject: [PATCH 03/14] see if there even is a ci-problem with the makefile --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index d91ba8a724..6e58efd832 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS= # +RTS $OPTIONS -RTS +RTS_OPTIONS=+RTS -H6G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From c63998c8991c53735e7b15036f8f4f8471c8a93e Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 13:25:13 +0100 Subject: [PATCH 04/14] remove 'suggested' heap size from RTS options in makefile The suggested heap size also seems to set a maximum. I don't why we have a suggested heap size anyway, so I just removed that, since make failed with agda 2.6.4.1, compiled with ghc 9.8.1. --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 9ff39ba0d1..cc1b821f08 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS=+RTS -H6G -RTS +RTS_OPTIONS= # +RTS $OPTIONS -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From 3b9292c889207a1e9feb253010739cfa027a4cdc Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 15:00:44 +0100 Subject: [PATCH 05/14] incease agda version, see if it fails --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 5129d5ff2b..d8b3b347c4 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -42,7 +42,7 @@ on: ######################################################################## env: - AGDA_BRANCH: v2.6.4 + AGDA_BRANCH: v2.6.4.1 GHC_VERSION: 9.4.7 CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' From 26cacced1cb1d4ee62641f8598016480ba3c3e9b Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 4 Dec 2023 17:44:47 +0100 Subject: [PATCH 06/14] see if there even is a ci-problem with the makefile --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index cc1b821f08..9ff39ba0d1 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS= # +RTS $OPTIONS -RTS +RTS_OPTIONS=+RTS -H6G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From c30632e971b59e35bca51f4edecfefda2461fdef Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 22 Jan 2024 09:53:02 +0100 Subject: [PATCH 07/14] switch the heap suggestions off again --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 9ff39ba0d1..39b5335528 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS=+RTS -H6G -RTS +RTS_OPTIONS= AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From 1d814c9e23c600201bcffe171e4928f521624190 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 22 Jan 2024 11:57:42 +0100 Subject: [PATCH 08/14] README: update version table --- README.md | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 9ce7431e45..e27dacc8eb 100644 --- a/README.md +++ b/README.md @@ -15,15 +15,16 @@ 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. Agda versions as written below, correspond to tags. -| 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` | +| cubical library version | Agda versions | +|-------------------------|---------------------| +| current master | `v2.6.4` `v2.6.4.1` | +| `v0.7` | `v2.6.4` `v2.6.4.1` | +| `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 ``` From b3622fa8be647a8917459f98d27cc3f7d24f26fd Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 22 Jan 2024 12:01:39 +0100 Subject: [PATCH 09/14] update version everywhere to 0.7 --- CITATION.cff | 4 ++-- cubical.agda-lib | 2 +- flake.nix | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CITATION.cff b/CITATION.cff index 407d6f4eef..8e12eb5483 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.6 -date-released: 2023-10-24 +version: 0.7 +date-released: 2024-01-22 url: "https://github.com/agda/cubical" diff --git a/cubical.agda-lib b/cubical.agda-lib index 6565f1c369..064f900d4c 100644 --- a/cubical.agda-lib +++ b/cubical.agda-lib @@ -1,4 +1,4 @@ -name: cubical-0.6 +name: cubical-0.7 include: . depend: flags: --cubical --no-import-sorts -WnoUnsupportedIndexedMatch diff --git a/flake.nix b/flake.nix index 2d5fcb7c3d..42f1b1beae 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ flake = false; }; inputs.agda = { - url = "github:agda/agda/v2.6.4"; + url = "github:agda/agda/v2.6.4.1"; 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.6"; + version = "0.7"; src = cleanSourceWith { filter = name: type: From 499a58d8252c0faa76a9fc4ed964d366e43b3bdc Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Mon, 22 Jan 2024 13:21:54 +0200 Subject: [PATCH 10/14] nix: Update flake inputs --- flake.lock | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/flake.lock b/flake.lock index b8510c40ce..6fa40f03e7 100644 --- a/flake.lock +++ b/flake.lock @@ -10,16 +10,16 @@ ] }, "locked": { - "lastModified": 1696540558, - "narHash": "sha256-fqYyjgOFQrU4ryGcLyz5gMYMdPk1P24ra7kQiUrbilg=", + "lastModified": 1701366566, + "narHash": "sha256-B8Jmjld0gGbkVO08GsovVqrUXCs8VfJ8UdM3sjHnzgM=", "owner": "agda", "repo": "agda", - "rev": "f42acb696e43d382639f04f869e9a99ab36a91c6", + "rev": "4293e0a94d15acac915ab9088b2ec028f78d14a9", "type": "github" }, "original": { "owner": "agda", - "ref": "v2.6.4", + "ref": "v2.6.4.1", "repo": "agda", "type": "github" } @@ -45,11 +45,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1694529238, - "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", "owner": "numtide", "repo": "flake-utils", - "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", "type": "github" }, "original": { @@ -60,11 +60,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1696757521, - "narHash": "sha256-cfgtLNCBLFx2qOzRLI6DHfqTdfWI+UbvsKYa3b3fvaA=", + "lastModified": 1705883077, + "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "2646b294a146df2781b1ca49092450e8a32814e1", + "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9", "type": "github" }, "original": { From 946138ef87372c42faaec413f892115685ddd9f7 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 8 Feb 2024 16:00:54 +0100 Subject: [PATCH 11/14] fix --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 39b5335528..4d6d8be583 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -31,7 +31,7 @@ check-whitespace: .PHONY : check-everythings check-everythings: - $(EVERYTHINGS) check-except Experiments + $(EVERYTHINGS) check-except .PHONY : gen-everythings gen-everythings: From bd3a04fba42980ee663c5a03bcb5c244bb4a8808 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sun, 11 Feb 2024 20:40:28 +0100 Subject: [PATCH 12/14] add default max heap size --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 4d6d8be583..92830cce3f 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -2,7 +2,7 @@ AGDA_BIN?=agda AGDA_FLAGS?=-W error AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS) FIX_WHITESPACE?=fix-whitespace -RTS_OPTIONS= +RTS_OPTIONS=+RTS -M32G -RTS AGDA=$(AGDA_EXEC) $(RTS_OPTIONS) RUNHASKELL?=runhaskell EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs From 1181fccef7d3787709480d8a47e616a9b93a33f1 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Sun, 11 Feb 2024 21:53:51 +0100 Subject: [PATCH 13/14] set release date to today --- CITATION.cff | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CITATION.cff b/CITATION.cff index 8e12eb5483..738819cdbb 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -4,5 +4,5 @@ authors: - name: "The Agda Community" title: "Cubical Agda Library" version: 0.7 -date-released: 2024-01-22 +date-released: 2024-02-11 url: "https://github.com/agda/cubical" From 08b0bb55c464915c2f5892c9961098025f57e798 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 12 Feb 2024 09:46:07 +0100 Subject: [PATCH 14/14] set release date to today --- CITATION.cff | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CITATION.cff b/CITATION.cff index 738819cdbb..048a89cdaf 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -4,5 +4,5 @@ authors: - name: "The Agda Community" title: "Cubical Agda Library" version: 0.7 -date-released: 2024-02-11 +date-released: 2024-02-12 url: "https://github.com/agda/cubical"