Fix deprecated modules (#2224)

* Fix deprecated modules

* [ ci ] Also build deprecated modules

* [ ci ] ignore user warnings in test

* [ ci ] fix filtering logic

Deprecation and safety are not the same thing

---------

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

Author: 2 people

.github/workflows/ci-ubuntu.yml

@@ -151,10 +151,19 @@ jobs:
 
       - name: Test stdlib
         run: |
+          # Including deprecated modules purely for testing
+          cabal run GenerateEverything -- --include-deprecated
+          ${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda
+          ${{ env.AGDA }} -WnoUserWarning Everything.agda
+
+      - name: Prepare HTML index
+        run: |
+          # Regenerating the Everything files without the deprecated modules
           cabal run GenerateEverything
           cp .github/tooling/* .
           ./index.sh
           ${{ env.AGDA }} --safe EverythingSafe.agda
+          ${{ env.AGDA }} Everything.agda
           ${{ env.AGDA }} index.agda
 
       - name: Golden testing
@@ -177,7 +186,6 @@ jobs:
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.html
           rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
           ${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
-
           cp .github/tooling/* .
           ./landing.sh
 

GenerateEverything.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE MultiWayIf #-}
 
 import Control.Applicative
 import Control.Monad
@@ -227,10 +228,10 @@ extractHeader mod = extract
 
 -- | A crude classifier looking for lines containing options
 
-data Status = Deprecated | Unsafe | Safe
-  deriving (Eq)
+data Safety = Unsafe | Safe deriving (Eq)
+data Status = Deprecated | Active deriving (Eq)
 
-classify :: FilePath -> [String] -> [String] -> Exc Status
+classify :: FilePath -> [String] -> [String] -> Exc (Safety, Status)
 classify fp hd ls
   -- We start with sanity checks
   | isUnsafe && safe          = throwError $ fp ++ contradiction "unsafe" "safe"
@@ -239,11 +240,12 @@ classify fp hd ls
   | isWithK && not withK      = throwError $ fp ++ missingWithK
   | not (isWithK || cubicalC) = throwError $ fp ++ uncategorized "as relying on K" "cubical-compatible"
   -- And then perform the actual classification
-  | deprecated                = pure $ Deprecated
-  | isUnsafe                  = pure $ Unsafe
-  | safe                      = pure $ Safe
-  -- We know that @not (isUnsafe || safe)@, all cases are covered
-  | otherwise                 = error "IMPOSSIBLE"
+  | otherwise = do
+      let safety = if | safe -> Safe
+                      | isUnsafe -> Unsafe
+                      | otherwise -> error "IMPOSSIBLE"
+      let status = if deprecated then Deprecated else Active
+      pure (safety, status)
 
   where
 
@@ -280,18 +282,20 @@ classify fp hd ls
 data LibraryFile = LibraryFile
   { filepath   :: FilePath -- ^ FilePath of the source file
   , header     :: [String] -- ^ All lines in the headers are already prefixed with \"-- \".
-  , status     :: Status   -- ^ Safety options used by the module
+  , safety     :: Safety
+  , status     :: Status   -- ^ Deprecation status options used by the module
   }
 
 analyse :: FilePath -> IO LibraryFile
 analyse fp = do
   ls <- lines <$> readFileUTF8 fp
   hd <- runExc $ extractHeader fp ls
-  cl <- runExc $ classify fp hd ls
+  (sf, st) <- runExc $ classify fp hd ls
   return $ LibraryFile
-    { filepath   = fp
-    , header     = hd
-    , status     = cl
+    { filepath = fp
+    , header   = hd
+    , safety   = sf
+    , status   = st
     }
 
 checkFilePaths :: String -> [FilePath] -> IO ()
@@ -356,7 +360,7 @@ main = do
     unlines [ header
             , "{-# OPTIONS --safe --guardedness #-}\n"
             , mkModule safeOutputFile
-            , format $ filter ((Unsafe /=) . status) libraryfiles
+            , format $ filter ((Unsafe /=) . safety) libraryfiles
             ]
 
 -- | Usage info.

src/Algebra/Operations/Semiring.agda

@@ -26,6 +26,6 @@ open Semiring S
 -- Re-exports
 
 open MonoidOperations +-commutativeMonoid public
-open import Algebra.Properties.Semiring.Exponentiation S public
-open import Algebra.Properties.Semiring.Multiplication S public
-  using (×1-homo-*; ×′1-homo-*)
+open import Algebra.Properties.Semiring.Exp S public
+open import Algebra.Properties.Semiring.Mult S public
+  using (×1-homo-*)

src/Algebra/Properties/BooleanAlgebra.agda

@@ -28,8 +28,7 @@ import Algebra.Properties.DistributiveLattice as DistribLatticeProperties
 
 open import Algebra.Structures _≈_
 open import Relation.Binary
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Equivalence using (_⇔_; module Equivalence)
+open import Function.Bundles using (module Equivalence; _⇔_)
 open import Data.Product.Base using (_,_)
 
 ------------------------------------------------------------------------
@@ -47,9 +46,9 @@ replace-equality {_≈′_} ≈⇔≈′ = record
   { isBooleanAlgebra = record
     { isDistributiveLattice = DistributiveLattice.isDistributiveLattice
         (DistribLatticeProperties.replace-equality distributiveLattice ≈⇔≈′)
-    ; ∨-complement          = ((λ x → to ⟨$⟩ ∨-complementˡ x) , λ x → to ⟨$⟩ ∨-complementʳ x)
-    ; ∧-complement          = ((λ x → to ⟨$⟩ ∧-complementˡ x) , λ x → to ⟨$⟩ ∧-complementʳ x)
-    ; ¬-cong                = λ i≈j → to ⟨$⟩ ¬-cong (from ⟨$⟩ i≈j)
+    ; ∨-complement          = ((λ x → to (∨-complementˡ x)) , λ x → to (∨-complementʳ x))
+    ; ∧-complement          = ((λ x → to (∧-complementˡ x)) , λ x → to (∧-complementʳ x))
+    ; ¬-cong                = λ i≈j → to (¬-cong (from i≈j))
     }
   } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
 {-# WARNING_ON_USAGE replace-equality

src/Algebra/Properties/DistributiveLattice.agda

@@ -12,8 +12,7 @@
 open import Algebra.Lattice.Bundles
 open import Algebra.Lattice.Structures.Biased
 open import Relation.Binary
-open import Function.Equality
-open import Function.Equivalence
+open import Function.Bundles using (module Equivalence; _⇔_)
 import Algebra.Construct.Subst.Equality as SubstEq
 
 module Algebra.Properties.DistributiveLattice
@@ -44,7 +43,7 @@ replace-equality {_≈′_} ≈⇔≈′ = record
   { isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record
     { isLattice    = Lattice.isLattice
                        (LatticeProperties.replace-equality lattice ≈⇔≈′)
-    ; ∨-distribʳ-∧ = λ x y z → to ⟨$⟩ ∨-distribʳ-∧ x y z
+    ; ∨-distribʳ-∧ = λ x y z → to (∨-distribʳ-∧ x y z)
     })
   } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
 {-# WARNING_ON_USAGE replace-equality

src/Data/Fin/Substitution/Example.agda

@@ -20,7 +20,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality.Core as PropEq
+open import Relation.Binary.PropositionalEquality as PropEq
   using (_≡_; refl; sym; cong; cong₂)
 open PropEq.≡-Reasoning
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive