Switch to Agda 2.8.0-rc3 by merging experimental into master (#2755)

* agda/agda#7674 eta-expand fields in record expression

Agda PR #7674 requires some implicit arguments explicitly in some record
expression given since variance info got refined (invariant to
non-variant) and hence solutions are no longer unique.

* Workaround for Agda 2.7.0 (and lower, I suppose)

* Correct option --warn to --warning for agda/agda#7966

The official name of the option is `--warning` and the prefix `--warn` is only
accepted because we have no options like `--warner` or
`--warner-brothers-owns-us`, but we might have so in the future.

* Update README and CI for v2.8.0-rc3

---------

Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>

Author: MatthewDaggitt

.github/workflows/ci-ubuntu.yml

@@ -76,11 +76,11 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=ef912c68fd329ad3046d156e3c1a70a7fec19ba1" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.7.0.1" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.8.0-rc3" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 

CHANGELOG/v1.3.md

@@ -226,7 +226,7 @@ Deprecated modules
 
 * A warning is now raised whenever you import a deprecated module. This should
   aid the transition to the new modules. These warnings can be disabled locally
-  by adding the pragma `{-# OPTIONS --warn=noUserWarning #-}` to the top of a module.
+  by adding the pragma `{-# OPTIONS --warning=noUserWarning #-}` to the top of a module.
 
 The following modules have been renamed as part of a drive to improve
 consistency across the library. The deprecated modules still exist and

README.md

@@ -2,6 +2,8 @@
 
 [![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg?branch=experimental)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml)
 
+**Note**: The library is currently tracking Agda 2.8.0 release candidate 3 in preparation for the release of Agda 2.8.0 and version 2.3 of the library. You will need to have the release candidate installed in order to type-check it.
+
 The Agda standard library
 =========================
 

src/Algebra/Construct/Initial.agda

@@ -75,10 +75,10 @@ rawMagma = record { ℤero }
 -- Structures
 
 isEquivalence : IsEquivalence _≈_
-isEquivalence = record { ℤero }
+isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} → trans {k = k} }
 
 isMagma : IsMagma _≈_ _∙_
-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {u = u} {v = v} → ∙-cong {y = y} {v = v} }
 
 isSemigroup : IsSemigroup _≈_ _∙_
 isSemigroup = record { isMagma = isMagma ; assoc = λ () }

src/Algebra/Operations/Semiring.agda

@@ -8,7 +8,7 @@
 
 -- Disabled to prevent warnings from deprecated
 -- Algebra.Operations.CommutativeMonoid
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra
 import Algebra.Operations.CommutativeMonoid as MonoidOperations

src/Algebra/Properties/BooleanAlgebra.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 -- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra.Lattice.Bundles
 

src/Algebra/Properties/DistributiveLattice.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 -- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra.Lattice.Bundles
 open import Algebra.Lattice.Structures.Biased

src/Data/Fin/Induction.agda

@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
 
 module Data.Fin.Induction where
 

src/Data/Fin/Properties.agda

@@ -6,7 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
 
 module Data.Fin.Properties where
 

src/Data/List.agda

@@ -8,7 +8,7 @@
 -- lists.
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans
 
 module Data.List where