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 <[email protected]>

.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