From c05cc5b7d3d34874ef0e0449ce0f957123b7521b Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Fri, 14 Jun 2013 18:46:35 +0900 Subject: [PATCH] Agda hackage (ghc-Agda) replaces deprecated Agda-executable --- .gitignore | 1 + Agda.spec | 264 ++++++++++++++++++++++++++++++++++++++++++++++------- sources | 2 +- 3 files changed, 231 insertions(+), 36 deletions(-) diff --git a/.gitignore b/.gitignore index 235ea33..eca3548 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ /Agda-executable-2.3.0.1.tar.gz +/Agda-2.3.2.1.tar.gz diff --git a/Agda.spec b/Agda.spec index 8abcaea..f53d2f8 100644 --- a/Agda.spec +++ b/Agda.spec @@ -1,74 +1,268 @@ # https://fedoraproject.org/wiki/Packaging:Haskell -# https://fedoraproject.org/wiki/PackagingDrafts/Haskell -%global pkg_name Agda-executable +%global pkg_name Agda -Name: Agda -Version: 2.3.0.1 -Release: 8%{?dist} -Summary: Command-line program for type-checking and compiling Agda programs +Name: %{pkg_name} +Version: 2.3.2.1 +Release: 1%{?dist} +Summary: A dependently typed functional programming language and proof assistant -License: MIT -URL: http://hackage.haskell.org/package/%{pkg_name} -Source0: http://hackage.haskell.org/packages/archive/%{pkg_name}/%{version}/%{pkg_name}-%{version}.tar.gz +License: MIT and BSD +URL: http://hackage.haskell.org/package/%{name} +Source0: http://hackage.haskell.org/packages/archive/%{name}/%{version}/%{name}-%{version}.tar.gz +Source1: agda-mode-init.el BuildRequires: ghc-Cabal-devel BuildRequires: ghc-rpm-macros -BuildRequires: ghc-Agda-devel = %{version} +# Begin cabal-rpm deps: +BuildRequires: ghc-QuickCheck-devel +BuildRequires: ghc-array-devel +BuildRequires: ghc-binary-devel +BuildRequires: ghc-bytestring-devel +BuildRequires: ghc-containers-devel +BuildRequires: ghc-deepseq-devel +BuildRequires: ghc-directory-devel +BuildRequires: ghc-filepath-devel +BuildRequires: ghc-geniplate-devel +BuildRequires: ghc-hashable-devel +BuildRequires: ghc-hashtables-devel +BuildRequires: ghc-haskeline-devel +BuildRequires: ghc-haskell-src-exts-devel +BuildRequires: ghc-mtl-devel +BuildRequires: ghc-old-time-devel +BuildRequires: ghc-parallel-devel +BuildRequires: ghc-pretty-devel +BuildRequires: ghc-process-devel +BuildRequires: ghc-text-devel +BuildRequires: ghc-unordered-containers-devel +BuildRequires: ghc-xhtml-devel +BuildRequires: ghc-zlib-devel +BuildRequires: alex +BuildRequires: happy +# End cabal-rpm deps +BuildRequires: chrpath +BuildRequires: emacs-haskell-mode +Requires: ghc-%{name}-devel = %{version}-%{release} +Requires: emacs-agda = %{version}-%{release} %description -This package provides a command-line program for type-checking and -compiling Agda programs. The program can also generate hyperlinked, -highlighted HTML files from Agda sources. +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). -For the interactive environment please install emacs-agda instead. +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 -n ghc-%{name} +Summary: Haskell %{name} library + +%description -n ghc-%{name} +This package provides the Haskell %{name} shared library. + + +%package -n ghc-%{name}-devel +Summary: Haskell %{name} library development files +Requires: ghc-compiler = %{ghc_version} +Requires(post): ghc-compiler = %{ghc_version} +Requires(postun): ghc-compiler = %{ghc_version} +Requires: ghc-%{name} = %{version}-%{release} +Obsoletes: Agda < 2.3.1 + +%description -n ghc-%{name}-devel +This package provides the Haskell %{name} library development files. + + +%package -n emacs-agda +Summary: Emacs mode for the Agda language +Group: Applications/Editors +License: MIT +Requires: ghc-%{pkg_name}-devel = %{version}-%{release} +Requires: emacs-haskell-mode +Requires: emacs(bin) >= %{_emacs_version} + +%description -n emacs-agda +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 +License: MIT +Requires: emacs-agda = %{version}-%{release} + +%description -n emacs-agda-el +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 -%setup -q -n %{pkg_name}-%{version} +%setup -q + +# tweak the Agda version in the emacs mode +if ! grep -q \"%{version}\" src/data/emacs-mode/agda2-mode.el; then + echo "agda2-version in src/data/emacs-mode/agda2-mode.el out of sync!" + exit 1 +fi %build -%ghc_bin_build +%ghc_lib_build + +%define elisp_files eri.el agda-input.el annotation.el agda2-highlight.el agda2-abbrevs.el agda2-mode.el agda2.el + +# el6 macro does not add "." to load-path +%if %{defined el6} +%define _emacs_bytecompile /usr/bin/emacs -batch --no-init-file --no-site-file --eval '(progn (setq load-path (cons "." load-path)))' -f batch-byte-compile +%endif + +cd src/data/emacs-mode +for i in %elisp_files; do + %{_emacs_bytecompile} $i +done +cd - %install -%ghc_bin_install +%ghc_lib_install + +%ghc_fix_dynamic_rpath agda + +mkdir -p %{buildroot}%{_emacs_sitelispdir}/agda +for i in src/data/emacs-mode/*; do + install -p -m 0644 $i %{buildroot}%{_emacs_sitelispdir}/agda +done + +mkdir -p %{buildroot}%{_emacs_sitestartdir} +install -p -m 0644 %SOURCE1 %{buildroot}%{_emacs_sitestartdir} + +rm %{buildroot}%{_bindir}/agda-mode +rm -r %{buildroot}%{_datadir}/%{pkg_name}-%{version}/EpicInclude +rm -r %{buildroot}%{_datadir}/%{pkg_name}-%{version}/emacs-mode + + +%post -n ghc-%{name}-devel +%ghc_pkg_recache + + +%postun -n ghc-%{name}-devel +%ghc_pkg_recache %files + + +%files -n ghc-%{name} -f %{name}.files %doc LICENSE -%attr(755,root,root) %{_bindir}/agda +%{_datadir}/%{name}-%{version} + + +%files -n ghc-%{name}-devel -f %{name}-devel.files +%doc doc/release-notes +%{_bindir}/agda + + +%files -n emacs-agda +%defattr(-,root,root,-) +%doc README +%dir %{_emacs_sitelispdir}/agda +%{_emacs_sitelispdir}/agda/*.elc +%{_emacs_sitestartdir}/*.el + + +%files -n emacs-agda-el +%defattr(-,root,root,-) +%{_emacs_sitelispdir}/agda/*.el %changelog -* Mon Mar 25 2013 Jens Petersen - 2.3.0.1-8 +* Tue Jun 11 2013 Jens Petersen - 2.3.2.1-1 +- rename src package from ghc-Agda to Agda +- update to 2.3.2.1 +- update to new simplified Haskell Packaging Guidelines +- agda command-line tool in devel subpackage + +* Fri Jun 07 2013 Jens Petersen +- update to new simplified Haskell Packaging Guidelines + +* Mon Mar 25 2013 Jens Petersen - 2.3.0.1-12 - rebuild -* Fri Mar 22 2013 Jens Petersen - 2.3.0.1-7 -- rebuild +* Tue Mar 19 2013 Jens Petersen - 2.3.0.1-11 +- allow haskeline-0.7 -* Wed Feb 13 2013 Fedora Release Engineering - 2.3.0.1-6 +* Wed Feb 13 2013 Fedora Release Engineering - 2.3.0.1-10 - Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild -* Tue Dec 25 2012 Jens Petersen - 2.3.0.1-5 -- rebuild +* Wed Dec 12 2012 Jens Petersen - 2.3.0.1-9 +- update QuickCheck-2.5 patch following upstream 2.3.2 +- for epel6 redefine newer _emacs_bytecompile +- own datadir correctly -* Thu Dec 6 2012 Jens Petersen - 2.3.0.1-4 -- remove ExclusiveArch ghc_arches_with_ghci +* Fri Nov 9 2012 Jens Petersen - 2.3.0.1-8 +- build with QuickCheck 2.5 -* Sat Nov 17 2012 Jens Petersen - 2.3.0.1-3 -- rebuild - -* Wed Jul 18 2012 Fedora Release Engineering - 2.3.0.1-2 +* Thu Jul 19 2012 Fedora Release Engineering - 2.3.0.1-7 - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild -* Tue Jul 10 2012 Jens Petersen - 2.3.0.1-1 -- update to 2.3.0.1 and cabal2spec-0.25 +* Mon Jul 16 2012 Jens Petersen - 2.3.0.1-6 +- change prof BRs to devel -* Fri Jun 3 2011 Jens Petersen - 2.2.10-1 +* Wed Jul 11 2012 Jens Petersen - 2.3.0.1-5 +- fix agda2-version in agda2-mode.el + +* Thu Jun 21 2012 Jens Petersen - 2.3.0.1-4 +- upstream patch for building with haskell-src-exts-1.13 +- use new cabal-tweak-dep-ver script to change mtl and haskell-src-exts bounds + +* Mon Jun 11 2012 Jens Petersen - 2.3.0.1-3 +- allow building with mtl-2.1 + +* Thu May 31 2012 Jens Petersen - 2.3.0.1-2 +- library license is also BSD (#710031) +- move release notes to devel subpackage + +* Tue Apr 10 2012 Jens Petersen - 2.3.0.1-1 +- update to 2.3.0.1 for ghc-7.4.1 + +* Tue Feb 14 2012 Jens Petersen - 2.3.0-1 +- update to 2.3.0 +- update to cabal2spec-0.25 +- new depends on hashtables + +* Fri Jun 3 2011 Jens Petersen - 2.2.10-2 +- also BR alex, happy, and emacs-haskell-mode + +* Thu Jun 2 2011 Jens Petersen - 2.2.10-1 - MIT license -- BR ghc-Agda-devel +- add deps and description +- emacs mode subpackages -* Fri Jun 3 2011 Fedora Haskell SIG - 2.2.10-0 +* Thu Jun 2 2011 Fedora Haskell SIG - 2.2.10-0 - initial packaging for Fedora automatically generated by cabal2spec-0.23 diff --git a/sources b/sources index 0e5e838..8b39e03 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -a9c803f0a829cf54d35b1a82f0ba6181 Agda-executable-2.3.0.1.tar.gz +b3549b00b8643426a09e94461764cf26 Agda-2.3.2.1.tar.gz