Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package ghc-dec for openSUSE:Factory checked in at 2022-10-13 15:41:43 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/ghc-dec (Old) and /work/SRC/openSUSE:Factory/.ghc-dec.new.2275 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "ghc-dec" Thu Oct 13 15:41:43 2022 rev:5 rq:1008454 version:0.0.5 Changes: -------- --- /work/SRC/openSUSE:Factory/ghc-dec/ghc-dec.changes 2022-02-11 23:10:41.195167590 +0100 +++ /work/SRC/openSUSE:Factory/.ghc-dec.new.2275/ghc-dec.changes 2022-10-13 15:41:50.678702722 +0200 @@ -1,0 +2,10 @@ +Sun Aug 21 11:41:26 UTC 2022 - Peter Simons <[email protected]> + +- Update dec to version 0.0.5. + ## 0.0.5 + + - Add `boringYes` and `absurdNo`. + - Add `Decidable a => Boring (Dec a)` instance. + - Add `Decidable ()`, `Decidable Void`, `Decidable (a, b)` instances. + +------------------------------------------------------------------- Old: ---- dec-0.0.4.tar.gz dec.cabal New: ---- dec-0.0.5.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ ghc-dec.spec ++++++ --- /var/tmp/diff_new_pack.GRu7e8/_old 2022-10-13 15:41:51.422704173 +0200 +++ /var/tmp/diff_new_pack.GRu7e8/_new 2022-10-13 15:41:51.430704189 +0200 @@ -1,7 +1,7 @@ # # spec file for package ghc-dec # -# Copyright (c) 2021 SUSE LLC +# Copyright (c) 2022 SUSE LLC # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -18,14 +18,14 @@ %global pkg_name dec Name: ghc-%{pkg_name} -Version: 0.0.4 +Version: 0.0.5 Release: 0 Summary: Decidable propositions License: BSD-3-Clause URL: https://hackage.haskell.org/package/%{pkg_name} Source0: https://hackage.haskell.org/package/%{pkg_name}-%{version}/%{pkg_name}-%{version}.tar.gz -Source1: https://hackage.haskell.org/package/%{pkg_name}-%{version}/revision/1.cabal#/%{pkg_name}.cabal BuildRequires: ghc-Cabal-devel +BuildRequires: ghc-boring-devel BuildRequires: ghc-rpm-macros ExcludeArch: %{ix86} @@ -48,7 +48,6 @@ %prep %autosetup -n %{pkg_name}-%{version} -cp -p %{SOURCE1} %{pkg_name}.cabal %build %ghc_lib_build ++++++ dec-0.0.4.tar.gz -> dec-0.0.5.tar.gz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dec-0.0.4/ChangeLog.md new/dec-0.0.5/ChangeLog.md --- old/dec-0.0.4/ChangeLog.md 2001-09-09 03:46:40.000000000 +0200 +++ new/dec-0.0.5/ChangeLog.md 2001-09-09 03:46:40.000000000 +0200 @@ -1,5 +1,11 @@ # Revision history for dec +## 0.0.5 + +- Add `boringYes` and `absurdNo`. +- Add `Decidable a => Boring (Dec a)` instance. +- Add `Decidable ()`, `Decidable Void`, `Decidable (a, b)` instances. + ## 0.0.4 - Mark module as explicitly `Safe`. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dec-0.0.4/dec.cabal new/dec-0.0.5/dec.cabal --- old/dec-0.0.4/dec.cabal 2001-09-09 03:46:40.000000000 +0200 +++ new/dec-0.0.5/dec.cabal 2001-09-09 03:46:40.000000000 +0200 @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: dec -version: 0.0.4 +version: 0.0.5 synopsis: Decidable propositions. category: Data, Dependent Types description: @@ -31,25 +31,28 @@ || ==8.4.4 || ==8.6.5 || ==8.8.4 - || ==8.10.3 - || ==9.0.1 + || ==8.10.4 + || ==9.0.2 + || ==9.2.4 + || ==9.4.1 source-repository head type: git - location: https://github.com/phadej/vec.git - subdir: dec + location: https://github.com/phadej/dec.git library default-language: Haskell2010 hs-source-dirs: src ghc-options: -Wall -fprint-explicit-kinds exposed-modules: Data.Type.Dec - build-depends: base >=4.7 && <4.16 + build-depends: + base >=4.7 && <4.18 + , boring >=0.2 && <0.3 if !impl(ghc >=7.10) build-depends: void >=0.7.3 && <0.8 - if impl(ghc >= 9.0) + if impl(ghc >=9.0) -- these flags may abort compilation with GHC-8.10 -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295 ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/dec-0.0.4/src/Data/Type/Dec.hs new/dec-0.0.5/src/Data/Type/Dec.hs --- old/dec-0.0.4/src/Data/Type/Dec.hs 2001-09-09 03:46:40.000000000 +0200 +++ new/dec-0.0.5/src/Data/Type/Dec.hs 2001-09-09 03:46:40.000000000 +0200 @@ -1,4 +1,5 @@ {-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} module Data.Type.Dec ( -- * Types Neg, @@ -14,9 +15,15 @@ decShow, decToMaybe, decToBool, + + -- * Boring + -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'. + boringYes, + absurdNo, ) where import Data.Void (Void) +import Data.Boring (Absurd (..), Boring (..)) -- | Intuitionistic negation. type Neg a = a -> Void @@ -38,6 +45,32 @@ decide :: Dec a ------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +-- | @()@ is truth. +-- +-- @since 0.0.5 +instance Decidable () where + decide = Yes () + +-- | 'Void' is falsehood. +-- +-- @since 0.0.5 +instance Decidable Void where + decide = No id + +-- | Products of decidable propositions are decidable +-- +-- @since 0.0.5 +instance (Decidable a, Decidable b) => Decidable (a, b) where + decide = case decide :: Dec a of + No nx -> No (\c -> nx (fst c)) + Yes x -> case decide :: Dec b of + No ny -> No (\c -> ny (snd c)) + Yes y -> Yes (x, y) + +------------------------------------------------------------------------------- -- Neg combinators ------------------------------------------------------------------------------- @@ -106,3 +139,25 @@ decToBool :: Dec a -> Bool decToBool (Yes _) = True decToBool (No _) = False + +------------------------------------------------------------------------------- +-- Boring +------------------------------------------------------------------------------- + +-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense. +-- +-- @since 0.0.5 +instance Decidable a => Boring (Dec a) where + boring = decide + +-- | 'Yes', it's 'boring'. +-- +-- @since 0.0.5 +boringYes :: Boring a => Dec a +boringYes = Yes boring + +-- | 'No', it's 'absurd'. +-- +-- @since 0.0.5 +absurdNo :: Absurd a => Dec a +absurdNo = No absurd
