[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