Skip to content

Commit b150186

Browse files
felixwellenncfavier
felixwellen
and
ncfavier
authored
Release for Agda 2.8.0 (#1222)
* comment/remove references to Everything.agda * try new makefile and ci-action * whitespace * add guardedness flag for now to see if the ci works * perform release ritual, remove obsoleted * update agda and cubical version in flake.nix * fix Nix build * reminder to remove --guardedness again * remove README.agda, since it does not seem to have a purpose now * Evan's suggestions * encourage lagda.md, update date * nix: use upstream Agda overlay The overlay was fixed after the 2.8.0 release. * update makefile * add --safe to the library flags and remove the option everywhere by now, --safe is compatible with --guardedness, so we can just add --safe to the library flags * workaround for html generation: simple bash script that generates a Everything.agda * update date --------- Co-authored-by: Naïm Camille Favier <n@monade.li>
1 parent 1f2af52 commit b150186

File tree

1,105 files changed

+290
-1383
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,105 files changed

+290
-1383
lines changed

‎.github/workflows/ci-ubuntu.yml

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ on:
4242
########################################################################
4343

4444
env:
45-
AGDA_BRANCH: v2.7.0.1
45+
AGDA_BRANCH: v2.8.0
4646
GHC_VERSION: 9.10.2
4747
CABAL_VERSION: 3.12.1.0
4848
CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
@@ -114,7 +114,7 @@ jobs:
114114
id: cache-library-restore
115115
with:
116116
path: ./_build
117-
key: library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-${{ hashFiles('Cubical/**', 'cubical.agda-lib', 'Everythings.hs') }}
117+
key: library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-${{ hashFiles('Cubical/**', 'cubical.agda-lib') }}
118118
restore-keys: |
119119
library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-
120120
@@ -125,8 +125,7 @@ jobs:
125125
run: |
126126
make test \
127127
AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
128-
FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \
129-
EVERYTHINGS='cabal run Everythings'
128+
FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace'
130129
131130
- name: Save library cache
132131
if: steps.cache-library-restore.outputs.cache-hit != 'true'
@@ -145,8 +144,7 @@ jobs:
145144
run: |
146145
make listings \
147146
AGDA_EXEC='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
148-
FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace' \
149-
EVERYTHINGS='cabal run Everythings'
147+
FIX_WHITESPACE='~/.local/fix-whitespace/bin/fix-whitespace'
150148
151149
- name: Deploy to GitHub Pages
152150
if: github.event_name == 'push' && github.ref_name == 'master'

‎.gitignore

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,4 @@
22
*~
33
\.*#*
44
\#*
5-
Cubical/*/Everything.agda
6-
!Cubical/Codata/Everything.agda
5+
/Cubical/Everything.agda

‎CITATION.cff

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
33
authors:
44
- name: "The Agda Community"
55
title: "Cubical Agda Library"
6-
version: 0.8
7-
date-released: 2025-05-09
6+
version: 0.9
7+
date-released: 2025-07-30
88
url: "https://github.com/agda/cubical"

‎Cubical/Algebra/AbGroup.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup where
32

43
open import Cubical.Algebra.AbGroup.Base public

‎Cubical/Algebra/AbGroup/Base.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Base where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DiffInt.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
-- It is recommended to use Cubical.Algebra.CommRing.Instances.Int
22
-- instead of this file.
33

4-
{-# OPTIONS --safe #-}
54
module Cubical.Algebra.AbGroup.Instances.DiffInt where
65

76
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DirectProduct.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectProduct where
32

43
open import Cubical.Data.Sigma

‎Cubical/Algebra/AbGroup/Instances/DirectSumFun.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectSumFun where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/DirectSumHIT.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-# OPTIONS --safe #-}
21
module Cubical.Algebra.AbGroup.Instances.DirectSumHIT where
32

43
open import Cubical.Foundations.Prelude

‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# OPTIONS --safe --lossy-unification #-}
1+
{-# OPTIONS --lossy-unification #-}
22
module Cubical.Algebra.AbGroup.Instances.FreeAbGroup where
33

44
open import Cubical.Foundations.Prelude

0 commit comments

Comments
 (0)