Taneb · Sep 12, 2026 · Oct 19, 2026 · Oct 19, 2026 · Oct 19, 2026 · Oct 29, 2026
diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
@@ -9,6 +9,7 @@ on:
     branches:
       - master
       - experimental
+      - v2.4-release
   merge_group:
 
 ########################################################################
@@ -76,11 +77,11 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.9.0-rc1" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.9.0-rc1" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 

diff --git a/src/Data/Erased.agda b/src/Data/Erased.agda
@@ -14,7 +14,7 @@ Use Data.Irrelevant instead."
 #-}
 
 open import Data.Irrelevant public
-  using ([_]; map; pure; _<*>_; _>>=_; zipWith)
+  using ([_]; map; pure; _<*>_; zipWith)
   renaming
   ( Irrelevant to Erased
   ; irrelevant to erased

diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
@@ -37,8 +37,8 @@ open import Agda.Builtin.Int public
   using ()
   renaming
   ( Int    to ℤ
-  ; pos    to +_      -- "+ n"      stands for "n"
-  ; negsuc to -[1+_]  -- "-[1+ n ]" stands for "- (1 + n)"
+  ; pos    to infix 8 +_  -- "+ n"      stands for "n"
+  ; negsuc to -[1+_]      -- "-[1+ n ]" stands for "- (1 + n)"
   )
 
 -- Some additional patterns that provide symmetry around 0
@@ -349,4 +349,3 @@ i % j = i %ℕ ∣ j ∣
   ; 0# = 0ℤ
   ; 1# = 1ℤ
   }
-
diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda
@@ -44,8 +44,8 @@ open Irrelevant public
 
 -- Irrelevant types are Recomputable
 
-recompute : Recomputable (Irrelevant A)
-irrelevant (recompute [ a ]) = a
+-- recompute : Recomputable (Irrelevant A)
+-- recompute [ a ] .irrelevant = a
 
 ------------------------------------------------------------------------
 -- Algebraic structure: Functor, Appplicative and Monad
@@ -60,9 +60,9 @@ infixl 4 _<*>_
 _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
 [ f ] <*> [ a ] = [ f a ]
 
-infixl 1 _>>=_
-_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
-[ a ] >>= f = recompute (f a)
+-- infixl 1 _>>=_
+-- _>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
+-- [ a ] >>= f = recompute (f a)
 
 ------------------------------------------------------------------------
 -- Other functions

diff --git a/src/Data/Record.agda b/src/Data/Record.agda
@@ -7,7 +7,7 @@
 
 -- For an example of how this module can be used, see README.Record.
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --cubical-compatible --safe -WnoUnguardedEtaRecord #-}
 
 open import Data.Bool.Base using (true; false; if_then_else_)
 open import Data.Empty using (⊥)

diff --git a/src/Data/Refinement/Base.agda b/src/Data/Refinement/Base.agda
@@ -35,7 +35,6 @@ open Refinement public
 -- It is attached to Refinement-syntax, to make it easy to import
 -- Data.Refinement without the special syntax.
 
-infix 2 Refinement-syntax
 Refinement-syntax = Refinement
 syntax Refinement-syntax A (λ x → P) = [ x ∈ A ∣ P ]
 

diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -128,7 +128,7 @@ module CastReasoning where
   -- convenient syntax for ‘equational’ reasoning
 
   infix 1 begin_
-  infixr 2 step-≃-⟩ step-≃-⟨ step-≂-⟩ step-≂-⟨ step-≈-⟩ step-≈-⟨ _≈⟨⟩_ ≈-cong
+  infixr 2 step-≃-⟩ step-≃-⟨ step-≂-⟩ step-≂-⟨ step-≈-⟩ step-≈-⟨ _≈⟨⟩_
   infix 3 _∎
 
   syntax step-≃-⟩ xs ys≡zs xs≈ys  = xs ≃⟨ xs≈ys ⟩ ys≡zs

diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
@@ -27,7 +27,6 @@ open RawApplicative AppF
 -- compute the length of the context everytime it's needed.
 record Cxt : Set where
   constructor _,_
-  pattern
   field
     len     : ℕ
     context : List (String × Arg Term)

diff --git a/src/Relation/Binary/Reasoning/Syntax.agda b/src/Relation/Binary/Reasoning/Syntax.agda
@@ -266,7 +266,7 @@ module _
       syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz
 
       -- Deprecated
-      infixr 2 step-≈ step-≈˘
+      infixr 2 step-≈˘
       step-≈ = step-≈-⟩
       {-# WARNING_ON_USAGE step-≈
       "Warning: step-≈ was deprecated in v2.0.
@@ -290,7 +290,7 @@ module _
 
 
       -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
-      infixr 2 step-≋ step-≋˘
+      infixr 2 step-≋˘
       step-≋ = step-≋-⟩
       {-# WARNING_ON_USAGE step-≋
       "Warning: step-≋ was deprecated in v2.0.
@@ -322,7 +322,7 @@ module _
       syntax step-#-⟨ x yRz y#x = x #⟨ y#x ⟨ yRz
 
       -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
-      infixr 2 step-# step-#˘
+      infixr 2 step-#˘
       step-# = step-#-⟩
       {-# WARNING_ON_USAGE step-#
       "Warning: step-# was deprecated in v2.0.
@@ -364,7 +364,7 @@ module _
 
 
       -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
-      infixr 2 step-↭ step-↭˘
+      infixr 2 step-↭˘
       step-↭ = forward
       {-# WARNING_ON_USAGE step-↭
       "Warning: step-↭ was deprecated in v2.0.
@@ -404,7 +404,7 @@ module ≡-syntax
 
 
   -- Don't remove until https://github.com/agda/agda/issues/5617 fixed.
-  infixr 2 step-≡ step-≡˘
+  infixr 2 step-≡˘
   step-≡ = step-≡-⟩
   {-# WARNING_ON_USAGE step-≡
   "Warning: step-≡ was deprecated in v2.0.
@@ -442,4 +442,3 @@ module end-syntax
 
   _∎ : ∀ x → R x x
   x ∎ = reflexive
-
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
@@ -60,8 +60,6 @@ quantₙ : (∀ {i l} {I : Set i} → (I → Set l) → Set (i ⊔ l)) →
 quantₙ Q zero     f = f
 quantₙ Q (suc n)  f = Q (λ x → quantₙ Q n (f x))
 
-infix 5 ∃⟨_⟩ Π[_] ∀[_]
-
 -- existential quantifier
 
 ∃⟨_⟩ : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))

diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
@@ -24,16 +24,11 @@ private
 
 open import Relation.Nullary.Recomputable.Core public
 
--- Irrelevant types are Recomputable
-
-open import Data.Irrelevant public
-  using () renaming (recompute to irrelevant-recompute)
-
 ------------------------------------------------------------------------
 -- Constructions
 
 ⊥-recompute : Recomputable ⊥
-⊥-recompute = irrelevant-recompute
+⊥-recompute ()
 
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
@@ -136,8 +136,6 @@ P ≐′ Q = (P ⊆′ Q) × (Q ⊆′ P)
 ------------------------------------------------------------------------
 -- Properties of sets
 
-infix 10 Satisfiable Universal IUniversal
-
 -- Emptiness - no element satisfies P.
 
 Empty : Pred A ℓ → Set _

diff --git a/src/Text/Regex/Base.agda b/src/Text/Regex/Base.agda
@@ -26,15 +26,14 @@ open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
 ------------------------------------------------------------------------
 -- Regular expressions on the alphabet A
 
-infix 10 [_] _─_
+infix 10 _─_
 data Range : Set a where
   [_] : (a : A)     → Range
   _─_ : (lb ub : A) → Range
 
 infixr 5 _∣_
 infixr 6 _∙_
 infixl 7 _⋆
-infix 10 [^_]
 
 data Exp : Set a where
   ε    : Exp