From 6e23886cffba2cadea20a59af5ce513584866f22 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Wed, 6 Dec 2023 15:17:15 +0000 Subject: [PATCH] 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 --- .github/workflows/ci-ubuntu.yml | 10 +++++- GenerateEverything.hs | 32 +++++++++++-------- src/Algebra/Operations/Semiring.agda | 6 ++-- src/Algebra/Properties/BooleanAlgebra.agda | 9 +++--- .../Properties/DistributiveLattice.agda | 5 ++- src/Data/Fin/Substitution/Example.agda | 2 +- 6 files changed, 37 insertions(+), 27 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 9ac08748df..a40fe804ad 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.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 diff --git a/GenerateEverything.hs b/GenerateEverything.hs index edea56a0f0..f6add73649 100644 --- a/GenerateEverything.hs +++ b/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. diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda index fbc6c254c2..08d55c884d 100644 --- a/src/Algebra/Operations/Semiring.agda +++ b/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-*) diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda index 2e1f148701..0445f20505 100644 --- a/src/Algebra/Properties/BooleanAlgebra.agda +++ b/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 diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda index adb6266e62..df03dfa38a 100644 --- a/src/Algebra/Properties/DistributiveLattice.agda +++ b/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 diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda index 02c98c539f..453c47d67f 100644 --- a/src/Data/Fin/Substitution/Example.agda +++ b/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