[ghc-Agda] update to new simplified Haskell Packaging Guidelines

Jens Petersen petersen at fedoraproject.org
Fri Jun 7 02:58:48 UTC 2013


commit 1c2f52db3279b6c21019abdb7d1c83372b01a4b3
Author: Jens Petersen <petersen at redhat.com>
Date:   Fri Jun 7 11:50:17 2013 +0900

    update to new simplified Haskell Packaging Guidelines

 ghc-Agda.spec |   87 +++++++++++++++++++++++++++++++++++++++-----------------
 1 files changed, 60 insertions(+), 27 deletions(-)
---
diff --git a/ghc-Agda.spec b/ghc-Agda.spec
index 9763567..53fc8aa 100644
--- a/ghc-Agda.spec
+++ b/ghc-Agda.spec
@@ -1,26 +1,11 @@
 # https://fedoraproject.org/wiki/Packaging:Haskell
-# https://fedoraproject.org/wiki/PackagingDrafts/Haskell
 
 %global pkg_name Agda
 
-%global common_summary A dependently typed functional programming language and proof assistant
-
-%global common_description Agda is a dependently typed functional programming language: it has\
-inductive families, which are similar to Haskell's GADTs, but they can\
-be indexed by values and not just types. It also has parameterized\
-modules, mixfix operators, Unicode characters, and an interactive\
-Emacs interface (the type checker can assist in the development of your code).\
-\
-Agda is also a proof assistant: It is an interactive system for writing and\
-checking proofs. Agda is based on intuitionistic type theory,\
-a foundational system for constructive mathematics developed by\
-the Swedish logician Per Martin-Löf. It has many similarities with other\
-proof assistants based on dependent types, such as Coq, Epigram and NuPRL.
-
 Name:           ghc-%{pkg_name}
 Version:        2.3.0.1
-Release:        12%{?dist}
-Summary:        %{common_summary}
+Release:        13%{?dist}
+Summary:        A dependently typed functional programming language and proof assistant
 
 License:        MIT and BSD
 URL:            http://hackage.haskell.org/package/%{pkg_name}
@@ -50,12 +35,34 @@ BuildRequires:  ghc-process-devel
 BuildRequires:  ghc-syb-devel
 BuildRequires:  ghc-xhtml-devel
 BuildRequires:  ghc-zlib-devel
+BuildRequires:  alex
+BuildRequires:  happy
 # End cabal-rpm deps
-BuildRequires:  happy, alex
 BuildRequires:  emacs-haskell-mode
 
 %description
-%{common_description}
+Agda is a dependently typed functional programming language: it has
+inductive families, which are similar to Haskell's GADTs, but they can
+be indexed by values and not just types. It also has parameterized
+modules, mixfix operators, Unicode characters, and an interactive
+Emacs interface (the type checker can assist in the development of your code).
+
+Agda is also a proof assistant: It is an interactive system for writing and
+checking proofs. Agda is based on intuitionistic type theory,
+a foundational system for constructive mathematics developed by
+the Swedish logician Per Martin-Löf. It has many similarities with other
+proof assistants based on dependent types, such as Coq, Epigram and NuPRL.
+
+
+%package devel
+Summary:        Haskell %{pkg_name} library development files
+Requires:       ghc-compiler = %{ghc_version}
+Requires(post): ghc-compiler = %{ghc_version}
+Requires(postun): ghc-compiler = %{ghc_version}
+Requires:       %{name} = %{version}-%{release}
+
+%description devel
+This package provides the Haskell %{pkg_name} library development files.
 
 For Emacs mode install emacs-agda.
 
@@ -72,10 +79,21 @@ Requires:       emacs-haskell-mode
 Requires:       emacs(bin) >= %{_emacs_version}
 
 %description -n emacs-agda
-%{common_description}
+Agda is a dependently typed functional programming language: it has
+inductive families, which are similar to Haskell's GADTs, but they can
+be indexed by values and not just types. It also has parameterized
+modules, mixfix operators, Unicode characters, and an interactive
+Emacs interface (the type checker can assist in the development of your code).
+
+Agda is also a proof assistant: It is an interactive system for writing and
+checking proofs. Agda is based on intuitionistic type theory,
+a foundational system for constructive mathematics developed by
+the Swedish logician Per Martin-Löf. It has many similarities with other
+proof assistants based on dependent types, such as Coq, Epigram and NuPRL.
 
 This is the interactive Emacs mode for Agda.
 
+
 %package -n emacs-agda-el
 Summary:        Elisp source files for Agda emacs mode
 Group:          Applications/Editors
@@ -83,9 +101,17 @@ License:        MIT
 Requires:       emacs-agda = %{version}-%{release}
 
 %description -n emacs-agda-el
-%{common_description}
-
-This provides the Emacs Lisp source files for the Agda interactive mode.
+Agda is a dependently typed functional programming language: it has
+inductive families, which are similar to Haskell's GADTs, but they can
+be indexed by values and not just types. It also has parameterized
+modules, mixfix operators, Unicode characters, and an interactive
+Emacs interface (the type checker can assist in the development of your code).
+
+Agda is also a proof assistant: It is an interactive system for writing and
+checking proofs. Agda is based on intuitionistic type theory,
+a foundational system for constructive mathematics developed by
+the Swedish logician Per Martin-Löf. It has many similarities with other
+proof assistants based on dependent types, such as Coq, Epigram and NuPRL.
 
 
 %prep
@@ -143,15 +169,19 @@ rm -r %{buildroot}%{_datadir}/%{pkg_name}-%{version}/emacs-mode
 %ghc_add_basepkg_file %{_datadir}/%{pkg_name}-%{version}
 
 
-%ghc_devel_package
+%post devel
+%ghc_pkg_recache
+
 
-%ghc_devel_description
+%postun devel
+%ghc_pkg_recache
 
 
-%ghc_devel_post_postun
+%files -f %{name}.files
+%doc LICENSE
 
 
-%ghc_files LICENSE
+%files devel -f %{name}-devel.files
 %doc doc/release-notes
 
 
@@ -169,6 +199,9 @@ rm -r %{buildroot}%{_datadir}/%{pkg_name}-%{version}/emacs-mode
 
 
 %changelog
+* Fri Jun 07 2013 Jens Petersen <petersen at redhat.com>
+- update to new simplified Haskell Packaging Guidelines
+
 * Mon Mar 25 2013 Jens Petersen <petersen at redhat.com> - 2.3.0.1-12
 - rebuild
 


More information about the scm-commits mailing list