Agda hackage (ghc-Agda) replaces deprecated Agda-executable
This commit is contained in:
Jens Petersen
parent
38b458cdc8
commit
c05cc5b7d3
1
.gitignore
vendored
1
.gitignore
vendored
@ -1 +1,2 @@
|
||||
/Agda-executable-2.3.0.1.tar.gz
|
||||
/Agda-2.3.2.1.tar.gz
|
||||
|
||||
264
Agda.spec
264
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 <petersen@redhat.com> - 2.3.0.1-8
|
||||
* Tue Jun 11 2013 Jens Petersen <petersen@redhat.com> - 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 <petersen@redhat.com>
|
||||
- update to new simplified Haskell Packaging Guidelines
|
||||
|
||||
* Mon Mar 25 2013 Jens Petersen <petersen@redhat.com> - 2.3.0.1-12
|
||||
- rebuild
|
||||
|
||||
* Fri Mar 22 2013 Jens Petersen <petersen@redhat.com> - 2.3.0.1-7
|
||||
- rebuild
|
||||
* Tue Mar 19 2013 Jens Petersen <petersen@redhat.com> - 2.3.0.1-11
|
||||
- allow haskeline-0.7
|
||||
|
||||
* Wed Feb 13 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.3.0.1-6
|
||||
* Wed Feb 13 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.3.0.1-10
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
|
||||
|
||||
* Tue Dec 25 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-5
|
||||
- rebuild
|
||||
* Wed Dec 12 2012 Jens Petersen <petersen@redhat.com> - 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 <petersen@redhat.com> - 2.3.0.1-4
|
||||
- remove ExclusiveArch ghc_arches_with_ghci
|
||||
* Fri Nov 9 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-8
|
||||
- build with QuickCheck 2.5
|
||||
|
||||
* Sat Nov 17 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-3
|
||||
- rebuild
|
||||
|
||||
* Wed Jul 18 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.3.0.1-2
|
||||
* Thu Jul 19 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.3.0.1-7
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
|
||||
|
||||
* Tue Jul 10 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-1
|
||||
- update to 2.3.0.1 and cabal2spec-0.25
|
||||
* Mon Jul 16 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-6
|
||||
- change prof BRs to devel
|
||||
|
||||
* Fri Jun 3 2011 Jens Petersen <petersen@redhat.com> - 2.2.10-1
|
||||
* Wed Jul 11 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-5
|
||||
- fix agda2-version in agda2-mode.el
|
||||
|
||||
* Thu Jun 21 2012 Jens Petersen <petersen@redhat.com> - 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 <petersen@redhat.com> - 2.3.0.1-3
|
||||
- allow building with mtl-2.1
|
||||
|
||||
* Thu May 31 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-2
|
||||
- library license is also BSD (#710031)
|
||||
- move release notes to devel subpackage
|
||||
|
||||
* Tue Apr 10 2012 Jens Petersen <petersen@redhat.com> - 2.3.0.1-1
|
||||
- update to 2.3.0.1 for ghc-7.4.1
|
||||
|
||||
* Tue Feb 14 2012 Jens Petersen <petersen@redhat.com> - 2.3.0-1
|
||||
- update to 2.3.0
|
||||
- update to cabal2spec-0.25
|
||||
- new depends on hashtables
|
||||
|
||||
* Fri Jun 3 2011 Jens Petersen <petersen@redhat.com> - 2.2.10-2
|
||||
- also BR alex, happy, and emacs-haskell-mode
|
||||
|
||||
* Thu Jun 2 2011 Jens Petersen <petersen@redhat.com> - 2.2.10-1
|
||||
- MIT license
|
||||
- BR ghc-Agda-devel
|
||||
- add deps and description
|
||||
- emacs mode subpackages
|
||||
|
||||
* Fri Jun 3 2011 Fedora Haskell SIG <haskell-devel@lists.fedoraproject.org> - 2.2.10-0
|
||||
* Thu Jun 2 2011 Fedora Haskell SIG <haskell-devel@lists.fedoraproject.org> - 2.2.10-0
|
||||
- initial packaging for Fedora automatically generated by cabal2spec-0.23
|
||||
|
||||
Loading…
Reference in New Issue
Block a user