Compare commits

..

89 Commits
f23 ... rawhide

Author SHA1 Message Date
Jens Petersen
659376cb02 bump release 2023-02-18 00:53:34 +08:00
Jens Petersen
cd72da1b95 SPDX migration 2023-01-29 22:44:58 +08:00
Jens Petersen
938a3e810b bump geniplate-mirror to 0.7.9 2023-01-29 22:44:09 +08:00
Jens Petersen
ccdfcab907 refresh to cabal-rpm-2.1.0 2023-01-21 16:44:24 +08:00
Fedora Release Engineering
6a1a838a85 Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2022-07-20 18:26:00 +00:00
Jens Petersen
5383d0287c add Provides agda 2022-06-20 13:57:27 +08:00
Jens Petersen
31a616d83e disable i686 (#2098425) 2022-06-19 14:58:13 +08:00
Jens Petersen
f6f1c37003 2.6.2.2 2022-06-07 16:05:14 +08:00
Jens Petersen
f21a1029c6 update to 2.6.2.1 2022-03-07 13:13:30 +08:00
Fedora Release Engineering
24e46c692e - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2022-01-19 19:12:40 +00:00
Miro Hrončok
ff1d99479b Rebuilt for https://fedoraproject.org/wiki/Changes/LIBFFI34 2022-01-08 11:06:18 +01:00
Jens Petersen
af39028c46 disable armv7hl: out of memory (#73471404) 2021-08-09 02:11:36 +08:00
Jens Petersen
5d5c715600 update to 2.6.2 2021-08-08 05:55:53 +08:00
Jens Petersen
7625567586 add reference to #991929 to armv7 -O0 condition 2021-08-05 00:42:11 +08:00
Jens Petersen
3e99f24800 cabal-rpm-2.0.9 2021-08-05 00:42:11 +08:00
Jens Petersen
99d2241eeb update to 2.6.1.3 2021-08-05 00:42:06 +08:00
Jens Petersen
14d6c0b37e move libs and data files to common subpackage again 2021-08-04 22:29:35 +08:00
Jens Petersen
63734cebf1 update geniplate-mirror to 0.7.7 2021-08-04 22:29:35 +08:00
Fedora Release Engineering
33b2b4d0b9 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2021-07-21 15:38:18 +00:00
Fedora Release Engineering
300a13f672 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2021-07-21 10:43:54 +00:00
Fedora Release Engineering
1786c87680 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2021-01-25 22:15:28 +00:00
Jeff Law
c9ed43346d Re-enable LTO 2020-10-11 18:52:28 -06:00
Jens Petersen
147e1019eb remove uri-encode from sources 2020-09-03 15:50:43 +08:00
Jens Petersen
2869a2b3a9 uri-encode has been packaged 2020-09-01 14:00:51 +08:00
Fedora Release Engineering
e0dc3e1641 - Second attempt - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2020-07-31 23:50:46 +00:00
Jeff Law
89dbda77ba Disable LTO on s390 2020-07-27 18:38:59 -06:00
Fedora Release Engineering
ac21eaf931 - Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2020-07-27 10:12:31 +00:00
Jens Petersen
8b113d48b1 enable armv7hl with -O0 (#991929) 2020-07-20 13:21:15 +08:00
Jens Petersen
02a60d692c refresh to cabal-rpm-2.0.6 2020-06-19 16:53:20 +08:00
Jens Petersen
a122f588a5 update to 2.6.1 2020-06-07 23:43:51 +08:00
Jens Petersen
36e744de86 refresh to cabal-rpm-2.0.5 2020-06-04 19:24:44 +08:00
Jens Petersen
c4c53b3fea move agda and data to base package, dropping common 2020-05-27 02:08:28 +08:00
Jens Petersen
0c769109ae refresh to cabal-rpm-2.0.2 2020-02-20 10:17:05 +08:00
Fedora Release Engineering
f23bc8455f - Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2020-01-28 09:10:44 +00:00
Jens Petersen
2c0f7876b1 really really disable i686 prof 2019-08-06 14:46:41 +08:00
Jens Petersen
d98367819a really disable i686 prof 2019-08-06 13:06:43 +08:00
Jens Petersen
55fb1c20ea prof panics on i686 2019-08-06 12:33:14 +08:00
Jens Petersen
900142581b subpkg deps need to be prof too 2019-08-06 10:01:49 +08:00
Jens Petersen
6365bc309c BR prof for lib and static for executable 2019-08-05 18:26:47 +08:00
Jens Petersen
13455a7ccc update to 2.6.0.1 2019-07-29 14:33:02 +00:00
Jens Petersen
93c549754b refresh to cabal-rpm-1.0.0: lib doc/prof subpkgs and bin static BRs 2019-07-25 06:17:11 +00:00
Fedora Release Engineering
64d8785d63 - Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2019-07-24 15:39:30 +00:00
Jens Petersen
31025ad40c update to 2.5.4.2 2019-02-25 10:27:50 +08:00
Jens Petersen
9e6df6678b refresh to cabal-rpm-0.13 2019-02-17 22:41:51 +08:00
Fedora Release Engineering
381aecc283 - Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2019-01-31 11:22:11 +00:00
Jens Petersen
054a111019 update sources 2018-07-31 17:35:02 +09:00
Jens Petersen
fcada7d934 add revised .cabal file 2018-07-29 10:57:12 +09:00
Jens Petersen
42213812a5 newline for easier patching 2018-07-19 13:33:15 +09:00
Fedora Release Engineering
168de37e16 - Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2018-07-12 18:54:31 +00:00
Fedora Release Engineering
a9910c7a85 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2018-02-07 00:24:22 +00:00
Jens Petersen
8243be8dc8 drop ldconfig scriptlets 2018-02-04 01:00:25 +09:00
Jens Petersen
803ef2a83d rpath tweaks for modules build 2018-01-26 09:09:03 +01:00
Jens Petersen
377de8fb8c refresh to cabal-rpm-0.12.1 2018-01-24 14:01:40 +01:00
Jens Petersen
c450966ea6 uri-encode needs network-uri 2018-01-12 17:59:51 +09:00
Jens Petersen
413d9c1463 uri-encode needs utf8-string 2018-01-12 16:22:50 +09:00
Jens Petersen
423f8f8744 add uri-encode source 2018-01-12 13:45:23 +09:00
Jens Petersen
e2ed4b024d update to 2.5.3 2018-01-02 18:54:29 +08:00
Jens Petersen
253d8eaad6 ieee754 is now a separate package 2017-12-26 10:58:59 +01:00
Jens Petersen
5bc04f5759 gitrev is now packaged 2017-11-15 12:44:12 +09:00
Jens Petersen
56bc32af70 gitrev now needs base-compat 2017-11-10 21:10:29 +09:00
Jens Petersen
e8fe124f84 update gitrev and geniplate-mirror 2017-11-10 16:57:10 +09:00
Fedora Release Engineering
df02d5a6af - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild 2017-08-02 16:46:42 +00:00
Fedora Release Engineering
77178c0167 - Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild 2017-07-26 01:38:45 +00:00
Jens Petersen
04232b3527 rebuild 2017-03-13 12:15:19 +09:00
Jens Petersen
d5e4024144 set LD_LIBRARY_PATH for compiling .agda files 2017-03-12 16:37:49 +09:00
Jens Petersen
8982741ffc compile .agda files are buildtime 2017-03-12 13:51:31 +09:00
Jens Petersen
4e6c542e8f armv7hl still fails (#991929) 2017-03-10 20:28:55 +09:00
Jens Petersen
1d4dc8f354 EdisonCore needs QuickCheck 2017-03-10 14:37:29 +09:00
Jens Petersen
7d30bcc63e add tarballs 2017-03-10 14:30:32 +09:00
Jens Petersen
64f09036ec subpackage EdisonAPI, EdisonCore, gitrev, ieee754, monadplus, murmur-hash
- add agda2-mode-pkg.el
- allow newer ieee754
- try building on arm again
2017-03-10 13:44:52 +09:00
Jens Petersen
1072e25653 update to 2.5.2 2017-02-27 07:49:02 +09:00
Jens Petersen
4feb7091aa refresh packaging 2017-02-24 13:43:01 +09:00
Fedora Release Engineering
63da85a065 - Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild 2017-02-10 04:58:58 +00:00
Jens Petersen
d76f81bcf8 build subpackage inside main package 2017-02-09 13:09:00 +09:00
Jens Petersen
108650930d drop build topdir 2017-01-29 14:23:51 +01:00
Jens Petersen
1bb4e49a1c use cabal-tweak-dep-ver to bump cpphs 2017-01-28 22:07:09 +01:00
Jens Petersen
540194fe1a disable dynlink on aarch64 2016-10-07 10:58:49 +09:00
Jens Petersen
7be71ac292 disable armv7hl again (#991929) 2016-10-06 19:06:57 +09:00
Jens Petersen
4f10ceb221 final build fixes
EpicInclude is gone
2016-10-06 16:22:37 +09:00
Jens Petersen
c4dd38eef5 mention enable arm in changelog 2016-10-06 15:08:06 +09:00
Jens Petersen
ac0a36269a add patch for HashMap 2016-10-06 14:30:37 +09:00
Jens Petersen
afe3c95527 apply cpphs patch 2016-10-06 12:23:24 +09:00
Jens Petersen
6ceb8aa2fd allow cpphs-1.20 2016-10-06 12:19:22 +09:00
Jens Petersen
42b7c9e446 update to 2.4.2.5
subpackage new dep geniplate-mirror
2016-10-06 11:01:47 +09:00
Jens Petersen
12a5988583 use %license 2016-09-28 18:22:39 +09:00
Jens Petersen
8b9cf04092 no longer remove license 2016-09-27 18:32:07 +09:00
Jens Petersen
2219348db1 drop redundant exclusivearch %ghc_arches_with_ghci 2016-03-07 22:55:21 +09:00
Jens Petersen
290b41f098 drop %ghc_arches_with_ghci 2016-03-07 22:54:00 +09:00
Dennis Gilmore
ec50775e58 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild 2016-02-03 15:18:58 +00:00
6 changed files with 2020 additions and 63 deletions

26
.gitignore vendored
View File

@ -3,3 +3,29 @@
/Agda-2.3.2.2.tar.gz
/Agda-2.4.2.tar.gz
/Agda-2.4.2.2.tar.gz
/geniplate-mirror-0.7.4.tar.gz
/Agda-2.4.2.5.tar.gz
/Agda-2.5.2.tar.gz
/EdisonAPI-1.3.1.tar.gz
/murmur-hash-0.1.0.9.tar.gz
/monadplus-1.4.2.tar.gz
/ieee754-0.8.0.tar.gz
/gitrev-1.2.0.tar.gz
/EdisonCore-1.3.1.1.tar.gz
/geniplate-mirror-0.7.5.tar.gz
/Agda-2.5.3.tar.gz
/gitrev-1.3.1.tar.gz
/uri-encode-1.5.0.5.tar.gz
/EdisonCore-1.3.2.1.tar.gz
/geniplate-mirror-0.7.6.tar.gz
/Agda-2.5.4.2.tar.gz
/Agda-2.6.0.1.tar.gz
/Agda-2.6.1.tar.gz
/Agda-2.6.1.3.tar.gz
/geniplate-mirror-0.7.7.tar.gz
/Agda-2.6.2.tar.gz
/geniplate-mirror-0.7.8.tar.gz
/Agda-2.6.2.1.tar.gz
/murmur-hash-0.1.0.10.tar.gz
/Agda-2.6.2.2.tar.gz
/geniplate-mirror-0.7.9.tar.gz

821
Agda-2.6.2.1.cabal Normal file
View File

@ -0,0 +1,821 @@
name: Agda
version: 2.6.2.1
x-revision: 4
cabal-version: >= 1.10
build-type: Custom
license: OtherLicense
license-file: LICENSE
copyright: (c) 2005-2021 The Agda Team.
author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
maintainer: The Agda Team
homepage: http://wiki.portal.chalmers.se/agda/
bug-reports: https://github.com/agda/agda/issues
category: Dependent types
synopsis: A dependently typed functional programming language and proof assistant
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
parameterised 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&#xf6;f. It has many
similarities with other proof assistants based on dependent types,
such as Coq, Epigram and NuPRL.
.
This package includes both a command-line program (agda) and an
Emacs mode. If you want to use the Emacs mode you can set it up by
running @agda-mode setup@ (see the README).
.
Note that the Agda package does not follow the package versioning
policy, because it is not intended to be used by third-party
packages.
tested-with: GHC == 8.0.2
GHC == 8.2.2
GHC == 8.4.4
GHC == 8.6.5
GHC == 8.8.4
GHC == 8.10.7
GHC == 9.0.1
GHC == 9.2.1
extra-source-files: CHANGELOG.md
README.md
doc/release-notes/2.6.2.md
doc/release-notes/2.6.1.3.md
doc/release-notes/2.6.1.2.md
doc/release-notes/2.6.1.1.md
doc/release-notes/2.6.1.md
doc/release-notes/2.6.0.1.md
doc/release-notes/2.6.0.md
doc/release-notes/2.5.4.2.md
doc/release-notes/2.5.4.1.md
doc/release-notes/2.5.4.md
doc/release-notes/2.5.3.md
doc/release-notes/2.5.2.md
doc/release-notes/2.5.1.2.md
doc/release-notes/2.5.1.1.md
doc/release-notes/2.5.1.md
doc/release-notes/2.4.2.5.md
doc/release-notes/2.4.2.4.md
doc/release-notes/2.4.2.3.md
doc/release-notes/2.4.2.2.md
doc/release-notes/2.4.2.1.md
doc/release-notes/2.4.2.md
doc/release-notes/2.4.0.2.md
doc/release-notes/2.4.0.1.md
doc/release-notes/2.4.0.md
doc/release-notes/2.3.2.2.md
doc/release-notes/2.3.2.1.md
doc/release-notes/2.3.2.md
doc/release-notes/2.3.0.md
doc/release-notes/2.2.10.md
doc/release-notes/2.2.8.md
doc/release-notes/2.2.6.md
doc/release-notes/2.2.2.md
doc/release-notes/2.2.4.md
doc/release-notes/2.2.0.md
-- Liang-Ting (2019-11-26): See Issues #4216
-- doc/user-manual.pdf
stack-8.0.2.yaml
stack-8.2.2.yaml
stack-8.4.4.yaml
stack-8.6.5.yaml
stack-8.8.4.yaml
stack-8.10.7.yaml
stack-9.0.1.yaml
stack-9.2.1.yaml
data-dir: src/data
data-files: emacs-mode/*.el
html/Agda.css
html/highlight-hover.js
JS/agda-rts.js
latex/agda.sty
latex/postprocess-latex.pl
lib/prim/Agda/Builtin/Bool.agda
lib/prim/Agda/Builtin/Char.agda
lib/prim/Agda/Builtin/Char/Properties.agda
lib/prim/Agda/Builtin/Coinduction.agda
lib/prim/Agda/Builtin/Cubical/Path.agda
lib/prim/Agda/Builtin/Cubical/Id.agda
lib/prim/Agda/Builtin/Cubical/Sub.agda
lib/prim/Agda/Builtin/Cubical/Glue.agda
lib/prim/Agda/Builtin/Cubical/HCompU.agda
lib/prim/Agda/Builtin/Equality.agda
lib/prim/Agda/Builtin/Equality/Erase.agda
lib/prim/Agda/Builtin/Equality/Rewrite.agda
lib/prim/Agda/Builtin/Float.agda
lib/prim/Agda/Builtin/Float/Properties.agda
lib/prim/Agda/Builtin/FromNat.agda
lib/prim/Agda/Builtin/FromNeg.agda
lib/prim/Agda/Builtin/FromString.agda
lib/prim/Agda/Builtin/IO.agda
lib/prim/Agda/Builtin/Int.agda
lib/prim/Agda/Builtin/List.agda
lib/prim/Agda/Builtin/Maybe.agda
lib/prim/Agda/Builtin/Nat.agda
lib/prim/Agda/Builtin/Reflection.agda
lib/prim/Agda/Builtin/Reflection/External.agda
lib/prim/Agda/Builtin/Reflection/Properties.agda
lib/prim/Agda/Builtin/Sigma.agda
lib/prim/Agda/Builtin/Size.agda
lib/prim/Agda/Builtin/Strict.agda
lib/prim/Agda/Builtin/String.agda
lib/prim/Agda/Builtin/String/Properties.agda
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
lib/prim/Agda/Builtin/Word.agda
lib/prim/Agda/Builtin/Word/Properties.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.agda
MAlonzo/src/MAlonzo/*.hs
MAlonzo/src/MAlonzo/RTE/*.hs
source-repository head
type: git
location: https://github.com/agda/agda.git
source-repository this
type: git
location: https://github.com/agda/agda.git
tag: v2.6.2.1
flag cpphs
default: False
manual: True
description: Use cpphs instead of cpp.
flag debug
default: False
manual: True
description:
Enable debugging features that may slow Agda down.
flag enable-cluster-counting
default: False
description:
Enable the --count-clusters flag. (If enable-cluster-counting is
False, then the --count-clusters flag triggers an error message.)
flag optimise-heavily
default: False
description:
Enable some expensive optimisations when compiling Agda.
custom-setup
setup-depends: base >= 4.9.0.0 && < 4.17
, Cabal >= 1.24.0.0 && < 3.7
, directory >= 1.2.6.2 && < 1.4
, filepath >= 1.4.1.0 && < 1.5
, process >= 1.4.2.0 && < 1.7
library
hs-source-dirs: src/full
if flag(cpphs)
-- We don't write an upper bound for cpphs because the
-- `build-tools` field can not be modified in Hackage.
build-tools: cpphs >= 1.20.9
ghc-options: -pgmP cpphs -optP --cpp
if flag(debug)
cpp-options: -DDEBUG
if flag(enable-cluster-counting)
cpp-options: -DCOUNT_CLUSTERS
build-depends: text-icu >= 0.7.1.0
if os(windows)
build-depends: Win32 >= 2.3.1.1 && < 2.13
-- Agda cannot be built with GHC 8.6.1 due to a compiler bug, see
-- Agda Issue #3344.
if impl(ghc == 8.6.1)
buildable: False
-- Agda cannot be built with Windows and GHC 8.6.3 due to a compiler
-- bug, see Agda Issue #3657.
if os(windows) && impl(ghc == 8.6.3)
buildable: False
build-depends: aeson >= 1.1.2.0 && < 2.1
, array >= 0.5.1.1 && < 0.6
, async >= 2.2 && < 2.3
, base >= 4.9.0.0 && < 4.17
, binary >= 0.8.3.0 && < 0.9
, blaze-html >= 0.8 && < 0.10
, boxes >= 0.1.3 && < 0.2
, bytestring >= 0.10.8.1 && < 0.11.2
, case-insensitive >= 1.2.0.4 && < 1.3
-- containers-0.5.11.0 is the first to contain IntSet.intersection
, containers >= 0.5.11.0 && < 0.7
, data-hash >= 0.2.0.0 && < 0.3
, deepseq >= 1.4.2.0 && < 1.5
, directory >= 1.2.6.2 && < 1.4
, edit-distance >= 0.2.1.2 && < 0.3
, equivalence >= 0.3.2 && < 0.5
-- exceptions-0.8 instead of 0.10 because of stack
, exceptions >= 0.8 && < 0.11
, filepath >= 1.4.1.0 && < 1.5
, gitrev >= 1.3.1 && < 2.0
-- hashable 1.2.0.10 makes library-test 10x
-- slower. The issue was fixed in hashable 1.2.1.0.
-- https://github.com/tibbe/hashable/issues/57.
, hashable >= 1.2.1.0 && < 1.5
-- There is a "serious bug"
-- (https://hackage.haskell.org/package/hashtables-1.2.0.2/changelog)
-- in hashtables 1.2.0.0/1.2.0.1. This bug seems to
-- have made Agda much slower (infinitely slower?) in
-- some cases.
, hashtables >= 1.2.0.2 && < 1.4
, haskeline >= 0.7.2.3 && < 0.9
-- monad-control-1.0.1.0 is the first to contain liftThrough
, monad-control >= 1.0.1.0 && < 1.1
-- mtl-2.1 contains a severe bug.
--
-- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
-- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+)
, mtl >= 2.2.1 && < 2.4
, murmur-hash >= 0.1 && < 0.2
, parallel >= 3.2.2.0 && < 3.3
, pretty >= 1.1.3.3 && < 1.2
, process >= 1.4.2.0 && < 1.7
, regex-tdfa >= 1.3.1.0 && < 1.4
, split >= 0.2.0.0 && < 0.2.4
, stm >= 2.4.4 && < 2.6
, strict >= 0.3.2 && < 0.5
, template-haskell >= 2.11.0.0 && < 2.19
, text >= 1.2.3.0 && < 2.1
, time >= 1.6.0.1 && < 1.13
, transformers >= 0.5 && < 0.6
-- build failure with transformers-0.6
, unordered-containers >= 0.2.5.0 && < 0.3
, uri-encode >= 1.5.0.4 && < 1.6
, zlib == 0.6.*
-- Andreas, 2021-03-10:
-- All packages we depend upon should be mentioned in an unconditional
-- build-depends field, but additional restrictions on their
-- version for specific GHCs may be placed in conditionals.
--
-- The goal is to be able to make (e.g. when a new GHC comes out)
-- revisions on hackage, e.g. relaxing upper bounds. This process
-- currently does not support revising conditionals.
-- ASR (2018-10-16).
-- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and
-- 8.4.3. See Issue #3277.
-- The other GHC versions can be restricted to >= 1.2.3.1.
if impl(ghc < 8.4.1) || impl(ghc > 8.4.3)
build-depends: text >= 1.2.3.1
if impl(ghc >= 8.4)
build-depends: ghc-compact == 0.1.*
-- We don't write upper bounds for Alex nor Happy because the
-- `build-tools` field can not be modified in Hackage. Agda doesn't
-- build with Alex 3.2.0 and segfaults with 3.2.2.
build-tools: alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3
, happy >= 1.19.4
exposed-modules: Agda.Auto.Auto
Agda.Auto.Options
Agda.Auto.CaseSplit
Agda.Auto.Convert
Agda.Auto.NarrowingSearch
Agda.Auto.SearchControl
Agda.Auto.Syntax
Agda.Auto.Typecheck
Agda.Benchmarking
Agda.Compiler.Backend
Agda.Compiler.Builtin
Agda.Compiler.CallCompiler
Agda.Compiler.Common
Agda.Compiler.JS.Compiler
Agda.Compiler.JS.Syntax
Agda.Compiler.JS.Substitution
Agda.Compiler.JS.Pretty
Agda.Compiler.MAlonzo.Coerce
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
Agda.Compiler.MAlonzo.HaskellTypes
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pragmas
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.Compiler.MAlonzo.Strict
Agda.Compiler.ToTreeless
Agda.Compiler.Treeless.AsPatterns
Agda.Compiler.Treeless.Builtin
Agda.Compiler.Treeless.Compare
Agda.Compiler.Treeless.EliminateDefaults
Agda.Compiler.Treeless.EliminateLiteralPatterns
Agda.Compiler.Treeless.Erase
Agda.Compiler.Treeless.GuardsToPrims
Agda.Compiler.Treeless.Identity
Agda.Compiler.Treeless.NormalizeNames
Agda.Compiler.Treeless.Pretty
Agda.Compiler.Treeless.Simplify
Agda.Compiler.Treeless.Subst
Agda.Compiler.Treeless.Uncase
Agda.Compiler.Treeless.Unused
Agda.ImpossibleTest
Agda.Interaction.AgdaTop
Agda.Interaction.Base
Agda.Interaction.BasicOps
Agda.Interaction.SearchAbout
Agda.Interaction.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.EmacsTop
Agda.Interaction.ExitCode
Agda.Interaction.JSONTop
Agda.Interaction.JSON
Agda.Interaction.FindFile
Agda.Interaction.Highlighting.Common
Agda.Interaction.Highlighting.Dot
Agda.Interaction.Highlighting.Emacs
Agda.Interaction.Highlighting.FromAbstract
Agda.Interaction.Highlighting.Generate
Agda.Interaction.Highlighting.HTML
Agda.Interaction.Highlighting.JSON
Agda.Interaction.Highlighting.Precise
Agda.Interaction.Highlighting.Range
Agda.Interaction.Highlighting.Vim
Agda.Interaction.Highlighting.LaTeX
Agda.Interaction.Imports
Agda.Interaction.InteractionTop
Agda.Interaction.Response
Agda.Interaction.MakeCase
Agda.Interaction.Monad
Agda.Interaction.Library
Agda.Interaction.Library.Base
Agda.Interaction.Library.Parse
Agda.Interaction.Options
Agda.Interaction.Options.Help
Agda.Interaction.Options.Lenses
Agda.Interaction.Options.Warnings
Agda.Main
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pattern
Agda.Syntax.Abstract.PatternSynonyms
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.Views
Agda.Syntax.Abstract
Agda.Syntax.Builtin
Agda.Syntax.Common
Agda.Syntax.Concrete.Attribute
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Definitions.Errors
Agda.Syntax.Concrete.Definitions.Monad
Agda.Syntax.Concrete.Definitions.Types
Agda.Syntax.Concrete.Fixity
Agda.Syntax.Concrete.Generic
Agda.Syntax.Concrete.Glyph
Agda.Syntax.Concrete.Name
Agda.Syntax.Concrete.Operators.Parser
Agda.Syntax.Concrete.Operators.Parser.Monad
Agda.Syntax.Concrete.Operators
Agda.Syntax.Concrete.Pattern
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Concrete
Agda.Syntax.DoNotation
Agda.Syntax.Fixity
Agda.Syntax.IdiomBrackets
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Blockers
Agda.Syntax.Internal.Defs
Agda.Syntax.Internal.Elim
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.MetaVars
Agda.Syntax.Internal.Names
Agda.Syntax.Internal.Pattern
Agda.Syntax.Internal.SanityCheck
Agda.Syntax.Literal
Agda.Syntax.Notation
Agda.Syntax.Parser.Alex
Agda.Syntax.Parser.Comments
Agda.Syntax.Parser.Layout
Agda.Syntax.Parser.LexActions
Agda.Syntax.Parser.Lexer
Agda.Syntax.Parser.Literate
Agda.Syntax.Parser.LookAhead
Agda.Syntax.Parser.Monad
Agda.Syntax.Parser.Parser
Agda.Syntax.Parser.StringLiterals
Agda.Syntax.Parser.Tokens
Agda.Syntax.Parser
Agda.Syntax.Position
Agda.Syntax.Reflected
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
Agda.Syntax.Translation.ReflectedToAbstract
Agda.Syntax.Treeless
Agda.Termination.CallGraph
Agda.Termination.CallMatrix
Agda.Termination.CutOff
Agda.Termination.Monad
Agda.Termination.Order
Agda.Termination.RecCheck
Agda.Termination.SparseMatrix
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.TheTypeChecker
Agda.TypeChecking.Abstract
Agda.TypeChecking.CheckInternal
Agda.TypeChecking.CompiledClause
Agda.TypeChecking.CompiledClause.Compile
Agda.TypeChecking.CompiledClause.Match
Agda.TypeChecking.Constraints
Agda.TypeChecking.Conversion
Agda.TypeChecking.Conversion.Pure
Agda.TypeChecking.Coverage
Agda.TypeChecking.Coverage.Match
Agda.TypeChecking.Coverage.SplitTree
Agda.TypeChecking.Datatypes
Agda.TypeChecking.DeadCode
Agda.TypeChecking.DisplayForm
Agda.TypeChecking.DropArgs
Agda.TypeChecking.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.EtaExpand
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Free.Precompute
Agda.TypeChecking.Free.Reduce
Agda.TypeChecking.Forcing
Agda.TypeChecking.Functions
Agda.TypeChecking.Generalize
Agda.TypeChecking.IApplyConfluence
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
Agda.TypeChecking.Inlining
Agda.TypeChecking.InstanceArguments
Agda.TypeChecking.Irrelevance
Agda.TypeChecking.Level
Agda.TypeChecking.LevelConstraints
Agda.TypeChecking.Lock
Agda.TypeChecking.Level.Solve
Agda.TypeChecking.MetaVars
Agda.TypeChecking.MetaVars.Mention
Agda.TypeChecking.MetaVars.Occurs
Agda.TypeChecking.Monad.Base
Agda.TypeChecking.Monad.Benchmark
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Caching
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
Agda.TypeChecking.Monad.Debug
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Pure
Agda.TypeChecking.Monad.Signature
Agda.TypeChecking.Monad.SizedTypes
Agda.TypeChecking.Monad.State
Agda.TypeChecking.Monad.Statistics
Agda.TypeChecking.Monad.Trace
Agda.TypeChecking.Monad
Agda.TypeChecking.Names
Agda.TypeChecking.Patterns.Abstract
Agda.TypeChecking.Patterns.Internal
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Positivity.Occurrence
Agda.TypeChecking.Pretty
Agda.TypeChecking.Pretty.Call
Agda.TypeChecking.Pretty.Constraint
Agda.TypeChecking.Pretty.Warning
Agda.TypeChecking.Primitive
Agda.TypeChecking.Primitive.Base
Agda.TypeChecking.Primitive.Cubical
Agda.TypeChecking.ProjectionLike
Agda.TypeChecking.Quote
Agda.TypeChecking.ReconstructParameters
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
Agda.TypeChecking.Reduce.Fast
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Rewriting
Agda.TypeChecking.Rewriting.Clause
Agda.TypeChecking.Rewriting.Confluence
Agda.TypeChecking.Rewriting.NonLinMatch
Agda.TypeChecking.Rewriting.NonLinPattern
Agda.TypeChecking.Rules.Application
Agda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Builtin.Coinduction
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.Display
Agda.TypeChecking.Rules.LHS
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Problem
Agda.TypeChecking.Rules.LHS.ProblemRest
Agda.TypeChecking.Rules.LHS.Unify
Agda.TypeChecking.Rules.Record
Agda.TypeChecking.Rules.Term
Agda.TypeChecking.Serialise
Agda.TypeChecking.Serialise.Base
Agda.TypeChecking.Serialise.Instances
Agda.TypeChecking.Serialise.Instances.Abstract
Agda.TypeChecking.Serialise.Instances.Common
Agda.TypeChecking.Serialise.Instances.Compilers
Agda.TypeChecking.Serialise.Instances.Highlighting
Agda.TypeChecking.Serialise.Instances.Internal
Agda.TypeChecking.Serialise.Instances.Errors
Agda.TypeChecking.SizedTypes
Agda.TypeChecking.SizedTypes.Solve
Agda.TypeChecking.SizedTypes.Syntax
Agda.TypeChecking.SizedTypes.Utils
Agda.TypeChecking.SizedTypes.WarshallSolver
Agda.TypeChecking.Sort
Agda.TypeChecking.Substitute
Agda.TypeChecking.Substitute.Class
Agda.TypeChecking.Substitute.DeBruijn
Agda.TypeChecking.SyntacticEquality
Agda.TypeChecking.Telescope
Agda.TypeChecking.Telescope.Path
Agda.TypeChecking.Unquote
Agda.TypeChecking.Warnings
Agda.TypeChecking.With
Agda.Utils.AffineHole
Agda.Utils.Applicative
Agda.Utils.AssocList
Agda.Utils.Bag
Agda.Utils.Benchmark
Agda.Utils.BiMap
Agda.Utils.CallStack
Agda.Utils.Char
Agda.Utils.Cluster
Agda.Utils.Empty
Agda.Utils.Environment
Agda.Utils.Either
Agda.Utils.Fail
Agda.Utils.Favorites
Agda.Utils.FileName
Agda.Utils.Float
Agda.Utils.Functor
Agda.Utils.Function
Agda.Utils.Graph.AdjacencyMap.Unidirectional
Agda.Utils.Graph.TopSort
Agda.Utils.Hash
Agda.Utils.Haskell.Syntax
Agda.Utils.Impossible
Agda.Utils.IndexedList
Agda.Utils.IntSet.Infinite
Agda.Utils.IO
Agda.Utils.IO.Binary
Agda.Utils.IO.Directory
Agda.Utils.IO.TempFile
Agda.Utils.IO.UTF8
Agda.Utils.IORef
Agda.Utils.Lens
Agda.Utils.Lens.Examples
Agda.Utils.List
Agda.Utils.List1
Agda.Utils.List2
Agda.Utils.ListT
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Memo
Agda.Utils.Monad
Agda.Utils.Monoid
Agda.Utils.Null
Agda.Utils.Parser.MemoisedCPS
Agda.Utils.PartialOrd
Agda.Utils.Permutation
Agda.Utils.Pointer
Agda.Utils.POMonoid
Agda.Utils.Pretty
Agda.Utils.RangeMap
Agda.Utils.SemiRing
Agda.Utils.Semigroup
Agda.Utils.Singleton
Agda.Utils.Size
Agda.Utils.SmallSet
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.Three
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.TypeLevel
Agda.Utils.TypeLits
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.Warshall
Agda.Utils.WithDefault
Agda.Utils.Zipper
Agda.Version
Agda.VersionCommit
other-modules: Paths_Agda
Agda.Interaction.Highlighting.Dot.Backend
Agda.Interaction.Highlighting.Dot.Base
Agda.Interaction.Highlighting.HTML.Backend
Agda.Interaction.Highlighting.HTML.Base
Agda.Interaction.Highlighting.LaTeX.Backend
Agda.Interaction.Highlighting.LaTeX.Base
Agda.Interaction.Options.Base
Agda.Interaction.Options.HasOptions
Agda.Utils.CallStack.Base
Agda.Utils.CallStack.Pretty
if flag(optimise-heavily)
ghc-options: -fexpose-all-unfoldings
-fspecialise-aggressively
-- NOTE: If adding flags, also add to `.ghci-8.0`
if impl(ghc <= 8.0.2)
ghc-options: -fprint-potential-instances
-- Initially, we disable all the warnings.
-w
-Wwarn
-- This option must be the first one after disabling the
-- warnings. See Issue #2094.
-Wunrecognised-warning-flags
-Wdeprecated-flags
-Wderiving-typeable
-Wdodgy-exports
-Wdodgy-foreign-imports
-Wdodgy-imports
-Wduplicate-exports
-Wempty-enumerations
-Widentities
-Wincomplete-patterns
-Winline-rule-shadowing
-Wmissing-fields
-Wmissing-methods
-Wmissing-pattern-synonym-signatures
-Wmissing-signatures
-Wnoncanonical-monad-instances
-Wnoncanonical-monoid-instances
-Woverflowed-literals
-Woverlapping-patterns
-Wsemigroup
-Wtabs
-Wtyped-holes
-Wunrecognised-pragmas
-Wunticked-promoted-constructors
-Wunused-do-bind
-Wunused-foralls
-Wwarnings-deprecations
-Wwrong-do-bind
else
ghc-options: -fprint-potential-instances
-Wwarn=unrecognised-warning-flags
-Wwarn=deprecated-flags
-Wwarn=deriving-typeable
-Wwarn=dodgy-exports
-Wwarn=dodgy-foreign-imports
-Wwarn=dodgy-imports
-Wwarn=duplicate-exports
-Wwarn=empty-enumerations
-Wwarn=identities
-Wwarn=incomplete-patterns
-Wwarn=inline-rule-shadowing
-Wwarn=missing-fields
-Wwarn=missing-methods
-Wwarn=missing-pattern-synonym-signatures
-Wwarn=missing-signatures
-Wwarn=noncanonical-monad-instances
-Wwarn=noncanonical-monoid-instances
-Wwarn=overflowed-literals
-Wwarn=overlapping-patterns
-Wwarn=semigroup
-Wwarn=tabs
-Wwarn=typed-holes
-Wwarn=unrecognised-pragmas
-Wwarn=unticked-promoted-constructors
-Wwarn=unused-do-bind
-Wwarn=unused-foralls
-Wwarn=warnings-deprecations
-Wwarn=wrong-do-bind
-- NOTE: If adding or removing flags, also change `.ghci-8.2`
if impl(ghc >= 8.2)
ghc-options: -Wcpp-undef
-- ASR TODO (2017-07-23): `make haddock` fails when
-- this flag is on.
-- -Wmissing-home-modules
-Wwarn=simplifiable-class-constraints
-Wwarn=unbanged-strict-patterns
-- NOTE: If adding or removing flags, also change `.ghci-8.6`
if impl(ghc >= 8.6)
ghc-options: -Wwarn=inaccessible-code
-Wwarn=star-binder
-Wwarn=star-is-type
-- The following warning is an error in GHC >= 8.10.
if impl(ghc >= 8.6) && impl(ghc < 8.10)
ghc-options: -Wwarn=implicit-kind-vars
-- NOTE: If adding or removing flags, also change `.ghci-8.8`
if impl(ghc >= 8.8)
ghc-options: -Wwarn=missed-extra-shared-lib
-- NOTE: If adding or removing flags, also change `.ghci-8.10`
if impl(ghc >= 8.10)
ghc-options: -Wwarn=deriving-defaults
-Wwarn=redundant-record-wildcards
-Wwarn=unused-packages
-Wwarn=unused-record-wildcards
-- NOTE: If adding or removing flags, also change `.ghci-9.0`
if impl(ghc >= 9.0)
ghc-options: -Wwarn=invalid-haddock
default-language: Haskell2010
-- NOTE: If adding or removing default extensions, also change:
-- .ghci-8.0
-- .hlint.yaml
-- This should also use the same extensions as the `test-suite` target below.
default-extensions: BangPatterns
, ConstraintKinds
--L-T Chen (2019-07-15):
-- Enabling DataKinds only locally makes the compile time
-- slightly shorter, see PR #3920.
--, DataKinds
, DefaultSignatures
, DeriveDataTypeable
, DeriveFoldable
, DeriveFunctor
, DeriveGeneric
, DeriveTraversable
, ExistentialQuantification
, FlexibleContexts
, FlexibleInstances
, FunctionalDependencies
, GeneralizedNewtypeDeriving
, InstanceSigs
, LambdaCase
, MultiParamTypeClasses
, MultiWayIf
, NamedFieldPuns
, OverloadedStrings
, PatternSynonyms
, RankNTypes
, RecordWildCards
, ScopedTypeVariables
, StandaloneDeriving
, TupleSections
, TypeFamilies
, TypeSynonymInstances
executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends: Agda
-- A version range on Agda generates a warning with
-- some versions of Cabal and GHC
-- (e.g. cabal-install version 1.24.0.2 compiled
-- using version 1.24.2.0 of the Cabal library and
-- GHC 8.2.1 RC1).
-- Nothing is used from the following package,
-- except for the prelude.
, base >= 4.9.0.0 && < 6
default-language: Haskell2010
-- If someone installs Agda with the setuid bit set, then the
-- presence of +RTS may be a security problem (see GHC bug #3910).
-- However, we sometimes recommend people to use +RTS to control
-- Agda's memory usage, so we want this functionality enabled by
-- default.
-- The threaded RTS by default starts a major GC after a program has
-- been idle for 0.3 s. This feature turned out to be annoying, so
-- the idle GC is now by default turned off (-I0).
ghc-options: -threaded -rtsopts
"-with-rtsopts=-M3.5G -I0"
executable agda-mode
hs-source-dirs: src/agda-mode
main-is: Main.hs
other-modules: Paths_Agda
build-depends: base >= 4.9.0.0 && < 4.17
, directory >= 1.2.6.2 && < 1.4
, filepath >= 1.4.1.0 && < 1.5
, process >= 1.4.2.0 && < 1.7
default-language: Haskell2010

828
Agda-2.6.2.2.cabal Normal file
View File

@ -0,0 +1,828 @@
name: Agda
version: 2.6.2.2
x-revision: 2
cabal-version: >= 1.10
build-type: Custom
license: OtherLicense
license-file: LICENSE
copyright: (c) 2005-2022 The Agda Team.
author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
maintainer: The Agda Team
homepage: http://wiki.portal.chalmers.se/agda/
bug-reports: https://github.com/agda/agda/issues
category: Dependent types
synopsis: A dependently typed functional programming language and proof assistant
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
parameterised 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&#xf6;f. It has many
similarities with other proof assistants based on dependent types,
such as Coq, Idris, Lean and NuPRL.
.
This package includes both a command-line program (agda) and an
Emacs mode. If you want to use the Emacs mode you can set it up by
running @agda-mode setup@ (see the README).
.
Note that the Agda package does not follow the package versioning
policy, because it is not intended to be used by third-party
packages.
tested-with: GHC == 8.0.2
GHC == 8.2.2
GHC == 8.4.4
GHC == 8.6.5
GHC == 8.8.4
GHC == 8.10.7
GHC == 9.0.2
GHC == 9.2.4
GHC == 9.4.1
extra-source-files: CHANGELOG.md
README.md
doc/release-notes/2.6.2.1.md
doc/release-notes/2.6.2.md
doc/release-notes/2.6.1.3.md
doc/release-notes/2.6.1.2.md
doc/release-notes/2.6.1.1.md
doc/release-notes/2.6.1.md
doc/release-notes/2.6.0.1.md
doc/release-notes/2.6.0.md
doc/release-notes/2.5.4.2.md
doc/release-notes/2.5.4.1.md
doc/release-notes/2.5.4.md
doc/release-notes/2.5.3.md
doc/release-notes/2.5.2.md
doc/release-notes/2.5.1.2.md
doc/release-notes/2.5.1.1.md
doc/release-notes/2.5.1.md
doc/release-notes/2.4.2.5.md
doc/release-notes/2.4.2.4.md
doc/release-notes/2.4.2.3.md
doc/release-notes/2.4.2.2.md
doc/release-notes/2.4.2.1.md
doc/release-notes/2.4.2.md
doc/release-notes/2.4.0.2.md
doc/release-notes/2.4.0.1.md
doc/release-notes/2.4.0.md
doc/release-notes/2.3.2.2.md
doc/release-notes/2.3.2.1.md
doc/release-notes/2.3.2.md
doc/release-notes/2.3.0.md
doc/release-notes/2.2.10.md
doc/release-notes/2.2.8.md
doc/release-notes/2.2.6.md
doc/release-notes/2.2.2.md
doc/release-notes/2.2.4.md
doc/release-notes/2.2.0.md
-- Liang-Ting (2019-11-26): See Issues #4216
-- doc/user-manual.pdf
stack-8.0.2.yaml
stack-8.2.2.yaml
stack-8.4.4.yaml
stack-8.6.5.yaml
stack-8.8.4.yaml
stack-8.10.7.yaml
stack-9.0.1.yaml
stack-9.0.2.yaml
stack-9.2.1.yaml
stack-9.2.2.yaml
data-dir: src/data
data-files: emacs-mode/*.el
html/Agda.css
html/highlight-hover.js
JS/agda-rts.js
latex/agda.sty
latex/postprocess-latex.pl
lib/prim/Agda/Builtin/Bool.agda
lib/prim/Agda/Builtin/Char.agda
lib/prim/Agda/Builtin/Char/Properties.agda
lib/prim/Agda/Builtin/Coinduction.agda
lib/prim/Agda/Builtin/Cubical/Path.agda
lib/prim/Agda/Builtin/Cubical/Id.agda
lib/prim/Agda/Builtin/Cubical/Sub.agda
lib/prim/Agda/Builtin/Cubical/Glue.agda
lib/prim/Agda/Builtin/Cubical/HCompU.agda
lib/prim/Agda/Builtin/Equality.agda
lib/prim/Agda/Builtin/Equality/Erase.agda
lib/prim/Agda/Builtin/Equality/Rewrite.agda
lib/prim/Agda/Builtin/Float.agda
lib/prim/Agda/Builtin/Float/Properties.agda
lib/prim/Agda/Builtin/FromNat.agda
lib/prim/Agda/Builtin/FromNeg.agda
lib/prim/Agda/Builtin/FromString.agda
lib/prim/Agda/Builtin/IO.agda
lib/prim/Agda/Builtin/Int.agda
lib/prim/Agda/Builtin/List.agda
lib/prim/Agda/Builtin/Maybe.agda
lib/prim/Agda/Builtin/Nat.agda
lib/prim/Agda/Builtin/Reflection.agda
lib/prim/Agda/Builtin/Reflection/External.agda
lib/prim/Agda/Builtin/Reflection/Properties.agda
lib/prim/Agda/Builtin/Sigma.agda
lib/prim/Agda/Builtin/Size.agda
lib/prim/Agda/Builtin/Strict.agda
lib/prim/Agda/Builtin/String.agda
lib/prim/Agda/Builtin/String/Properties.agda
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
lib/prim/Agda/Builtin/Word.agda
lib/prim/Agda/Builtin/Word/Properties.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.agda
MAlonzo/src/MAlonzo/*.hs
MAlonzo/src/MAlonzo/RTE/*.hs
source-repository head
type: git
location: https://github.com/agda/agda.git
source-repository this
type: git
location: https://github.com/agda/agda.git
tag: v2.6.2.2
flag cpphs
default: False
manual: True
description: Use cpphs instead of cpp.
flag debug
default: False
manual: True
description:
Enable debugging features that may slow Agda down.
flag enable-cluster-counting
default: False
description:
Enable the --count-clusters flag. (If enable-cluster-counting is
False, then the --count-clusters flag triggers an error message.)
flag optimise-heavily
default: False
description:
Enable some expensive optimisations when compiling Agda.
custom-setup
setup-depends: base >= 4.9.0.0 && < 4.18
, Cabal >= 1.24.0.0 && < 3.9
, directory >= 1.2.6.2 && < 1.4
, filepath >= 1.4.1.0 && < 1.5
, process >= 1.4.2.0 && < 1.7
library
hs-source-dirs: src/full
if flag(cpphs)
-- We don't write an upper bound for cpphs because the
-- `build-tools` field can not be modified in Hackage.
build-tools: cpphs >= 1.20.9
ghc-options: -pgmP cpphs -optP --cpp
if flag(debug)
cpp-options: -DDEBUG
if flag(enable-cluster-counting)
cpp-options: -DCOUNT_CLUSTERS
build-depends: text-icu >= 0.7.1.0
if os(windows)
build-depends: Win32 >= 2.3.1.1 && < 2.13
-- Agda cannot be built with GHC 8.6.1 due to a compiler bug, see
-- Agda Issue #3344.
if impl(ghc == 8.6.1)
buildable: False
-- Agda cannot be built with Windows and GHC 8.6.3 due to a compiler
-- bug, see Agda Issue #3657.
if os(windows) && impl(ghc == 8.6.3)
buildable: False
build-depends: aeson >= 1.1.2.0 && < 2.2
, array >= 0.5.1.1 && < 0.6
, async >= 2.2 && < 2.3
, base >= 4.9.0.0 && < 4.18
, binary >= 0.8.3.0 && < 0.9
, blaze-html >= 0.8 && < 0.10
, boxes >= 0.1.3 && < 0.2
, bytestring >= 0.10.8.1 && < 0.12
, case-insensitive >= 1.2.0.4 && < 1.3
-- containers-0.5.11.0 is the first to contain IntSet.intersection
, containers >= 0.5.11.0 && < 0.7
, data-hash >= 0.2.0.0 && < 0.3
, deepseq >= 1.4.2.0 && < 1.5
, directory >= 1.2.6.2 && < 1.4
, edit-distance >= 0.2.1.2 && < 0.3
, equivalence >= 0.3.2 && < 0.5
-- exceptions-0.8 instead of 0.10 because of stack
, exceptions >= 0.8 && < 0.11
, filepath >= 1.4.1.0 && < 1.5
, gitrev >= 1.3.1 && < 2.0
-- hashable 1.2.0.10 makes library-test 10x
-- slower. The issue was fixed in hashable 1.2.1.0.
-- https://github.com/tibbe/hashable/issues/57.
, hashable >= 1.2.1.0 && < 1.5
-- There is a "serious bug"
-- (https://hackage.haskell.org/package/hashtables-1.2.0.2/changelog)
-- in hashtables 1.2.0.0/1.2.0.1. This bug seems to
-- have made Agda much slower (infinitely slower?) in
-- some cases.
, hashtables >= 1.2.0.2 && < 1.4
, haskeline >= 0.7.2.3 && < 0.9
-- monad-control-1.0.1.0 is the first to contain liftThrough
, monad-control >= 1.0.1.0 && < 1.1
-- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
-- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+)
, mtl >= 2.2.1 && < 2.4
, murmur-hash >= 0.1 && < 0.2
, parallel >= 3.2.2.0 && < 3.3
, pretty >= 1.1.3.3 && < 1.2
, process >= 1.4.2.0 && < 1.7
, regex-tdfa >= 1.3.1.0 && < 1.4
, split >= 0.2.0.0 && < 0.2.4
, stm >= 2.4.4 && < 2.6
, strict >= 0.3.2 && < 0.5
, template-haskell >= 2.11.0.0 && < 2.20
, text >= 1.2.3.0 && < 2.1
, time >= 1.6.0.1 && < 1.13
, transformers >= 0.5 && < 0.7
, unordered-containers >= 0.2.5.0 && < 0.3
, uri-encode >= 1.5.0.4 && < 1.6
, zlib == 0.6.*
-- Andreas, 2022-02-02, issue #5659:
-- Build failure with transformers-0.6.0.{0,1,2} and GHC 8.6.
-- Transformers-0.6.0.3 might restored GHC 8.6 buildability.
if impl(ghc == 8.6.*)
build-depends: transformers < 0.6 || >= 0.6.0.3
-- Andreas, 2021-03-10:
-- All packages we depend upon should be mentioned in an unconditional
-- build-depends field, but additional restrictions on their
-- version for specific GHCs may be placed in conditionals.
--
-- The goal is to be able to make (e.g. when a new GHC comes out)
-- revisions on hackage, e.g. relaxing upper bounds. This process
-- currently does not support revising conditionals.
-- ASR (2018-10-16).
-- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and
-- 8.4.3. See Issue #3277.
-- The other GHC versions can be restricted to >= 1.2.3.1.
if impl(ghc < 8.4.1) || impl(ghc > 8.4.3)
build-depends: text >= 1.2.3.1
if impl(ghc >= 8.4)
build-depends: ghc-compact == 0.1.*
-- We don't write upper bounds for Alex nor Happy because the
-- `build-tools` field can not be modified in Hackage. Agda doesn't
-- build with Alex 3.2.0 and segfaults with 3.2.2.
build-tools: alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3
, happy >= 1.19.4
exposed-modules: Agda.Auto.Auto
Agda.Auto.Options
Agda.Auto.CaseSplit
Agda.Auto.Convert
Agda.Auto.NarrowingSearch
Agda.Auto.SearchControl
Agda.Auto.Syntax
Agda.Auto.Typecheck
Agda.Benchmarking
Agda.Compiler.Backend
Agda.Compiler.Builtin
Agda.Compiler.CallCompiler
Agda.Compiler.Common
Agda.Compiler.JS.Compiler
Agda.Compiler.JS.Syntax
Agda.Compiler.JS.Substitution
Agda.Compiler.JS.Pretty
Agda.Compiler.MAlonzo.Coerce
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
Agda.Compiler.MAlonzo.HaskellTypes
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pragmas
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.Compiler.MAlonzo.Strict
Agda.Compiler.ToTreeless
Agda.Compiler.Treeless.AsPatterns
Agda.Compiler.Treeless.Builtin
Agda.Compiler.Treeless.Compare
Agda.Compiler.Treeless.EliminateDefaults
Agda.Compiler.Treeless.EliminateLiteralPatterns
Agda.Compiler.Treeless.Erase
Agda.Compiler.Treeless.GuardsToPrims
Agda.Compiler.Treeless.Identity
Agda.Compiler.Treeless.NormalizeNames
Agda.Compiler.Treeless.Pretty
Agda.Compiler.Treeless.Simplify
Agda.Compiler.Treeless.Subst
Agda.Compiler.Treeless.Uncase
Agda.Compiler.Treeless.Unused
Agda.ImpossibleTest
Agda.Interaction.AgdaTop
Agda.Interaction.Base
Agda.Interaction.BasicOps
Agda.Interaction.SearchAbout
Agda.Interaction.CommandLine
Agda.Interaction.EmacsCommand
Agda.Interaction.EmacsTop
Agda.Interaction.ExitCode
Agda.Interaction.JSONTop
Agda.Interaction.JSON
Agda.Interaction.FindFile
Agda.Interaction.Highlighting.Common
Agda.Interaction.Highlighting.Dot
Agda.Interaction.Highlighting.Emacs
Agda.Interaction.Highlighting.FromAbstract
Agda.Interaction.Highlighting.Generate
Agda.Interaction.Highlighting.HTML
Agda.Interaction.Highlighting.JSON
Agda.Interaction.Highlighting.Precise
Agda.Interaction.Highlighting.Range
Agda.Interaction.Highlighting.Vim
Agda.Interaction.Highlighting.LaTeX
Agda.Interaction.Imports
Agda.Interaction.InteractionTop
Agda.Interaction.Response
Agda.Interaction.MakeCase
Agda.Interaction.Monad
Agda.Interaction.Library
Agda.Interaction.Library.Base
Agda.Interaction.Library.Parse
Agda.Interaction.Options
Agda.Interaction.Options.Help
Agda.Interaction.Options.Lenses
Agda.Interaction.Options.Warnings
Agda.Main
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pattern
Agda.Syntax.Abstract.PatternSynonyms
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.Views
Agda.Syntax.Abstract
Agda.Syntax.Builtin
Agda.Syntax.Common
Agda.Syntax.Concrete.Attribute
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Definitions.Errors
Agda.Syntax.Concrete.Definitions.Monad
Agda.Syntax.Concrete.Definitions.Types
Agda.Syntax.Concrete.Fixity
Agda.Syntax.Concrete.Generic
Agda.Syntax.Concrete.Glyph
Agda.Syntax.Concrete.Name
Agda.Syntax.Concrete.Operators.Parser
Agda.Syntax.Concrete.Operators.Parser.Monad
Agda.Syntax.Concrete.Operators
Agda.Syntax.Concrete.Pattern
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Concrete
Agda.Syntax.DoNotation
Agda.Syntax.Fixity
Agda.Syntax.IdiomBrackets
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Blockers
Agda.Syntax.Internal.Defs
Agda.Syntax.Internal.Elim
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.MetaVars
Agda.Syntax.Internal.Names
Agda.Syntax.Internal.Pattern
Agda.Syntax.Internal.SanityCheck
Agda.Syntax.Literal
Agda.Syntax.Notation
Agda.Syntax.Parser.Alex
Agda.Syntax.Parser.Comments
Agda.Syntax.Parser.Layout
Agda.Syntax.Parser.LexActions
Agda.Syntax.Parser.Lexer
Agda.Syntax.Parser.Literate
Agda.Syntax.Parser.LookAhead
Agda.Syntax.Parser.Monad
Agda.Syntax.Parser.Parser
Agda.Syntax.Parser.StringLiterals
Agda.Syntax.Parser.Tokens
Agda.Syntax.Parser
Agda.Syntax.Position
Agda.Syntax.Reflected
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
Agda.Syntax.Translation.ReflectedToAbstract
Agda.Syntax.Treeless
Agda.Termination.CallGraph
Agda.Termination.CallMatrix
Agda.Termination.CutOff
Agda.Termination.Monad
Agda.Termination.Order
Agda.Termination.RecCheck
Agda.Termination.SparseMatrix
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.TheTypeChecker
Agda.TypeChecking.Abstract
Agda.TypeChecking.CheckInternal
Agda.TypeChecking.CompiledClause
Agda.TypeChecking.CompiledClause.Compile
Agda.TypeChecking.CompiledClause.Match
Agda.TypeChecking.Constraints
Agda.TypeChecking.Conversion
Agda.TypeChecking.Conversion.Pure
Agda.TypeChecking.Coverage
Agda.TypeChecking.Coverage.Match
Agda.TypeChecking.Coverage.SplitTree
Agda.TypeChecking.Datatypes
Agda.TypeChecking.DeadCode
Agda.TypeChecking.DisplayForm
Agda.TypeChecking.DropArgs
Agda.TypeChecking.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.EtaExpand
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Free.Lazy
Agda.TypeChecking.Free.Precompute
Agda.TypeChecking.Free.Reduce
Agda.TypeChecking.Forcing
Agda.TypeChecking.Functions
Agda.TypeChecking.Generalize
Agda.TypeChecking.IApplyConfluence
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
Agda.TypeChecking.Inlining
Agda.TypeChecking.InstanceArguments
Agda.TypeChecking.Irrelevance
Agda.TypeChecking.Level
Agda.TypeChecking.LevelConstraints
Agda.TypeChecking.Lock
Agda.TypeChecking.Level.Solve
Agda.TypeChecking.MetaVars
Agda.TypeChecking.MetaVars.Mention
Agda.TypeChecking.MetaVars.Occurs
Agda.TypeChecking.Monad.Base
Agda.TypeChecking.Monad.Benchmark
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Caching
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
Agda.TypeChecking.Monad.Debug
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Pure
Agda.TypeChecking.Monad.Signature
Agda.TypeChecking.Monad.SizedTypes
Agda.TypeChecking.Monad.State
Agda.TypeChecking.Monad.Statistics
Agda.TypeChecking.Monad.Trace
Agda.TypeChecking.Monad
Agda.TypeChecking.Names
Agda.TypeChecking.Patterns.Abstract
Agda.TypeChecking.Patterns.Internal
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Positivity.Occurrence
Agda.TypeChecking.Pretty
Agda.TypeChecking.Pretty.Call
Agda.TypeChecking.Pretty.Constraint
Agda.TypeChecking.Pretty.Warning
Agda.TypeChecking.Primitive
Agda.TypeChecking.Primitive.Base
Agda.TypeChecking.Primitive.Cubical
Agda.TypeChecking.ProjectionLike
Agda.TypeChecking.Quote
Agda.TypeChecking.ReconstructParameters
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
Agda.TypeChecking.Reduce.Fast
Agda.TypeChecking.Reduce.Monad
Agda.TypeChecking.Rewriting
Agda.TypeChecking.Rewriting.Clause
Agda.TypeChecking.Rewriting.Confluence
Agda.TypeChecking.Rewriting.NonLinMatch
Agda.TypeChecking.Rewriting.NonLinPattern
Agda.TypeChecking.Rules.Application
Agda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Builtin.Coinduction
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.Display
Agda.TypeChecking.Rules.LHS
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Problem
Agda.TypeChecking.Rules.LHS.ProblemRest
Agda.TypeChecking.Rules.LHS.Unify
Agda.TypeChecking.Rules.Record
Agda.TypeChecking.Rules.Term
Agda.TypeChecking.Serialise
Agda.TypeChecking.Serialise.Base
Agda.TypeChecking.Serialise.Instances
Agda.TypeChecking.Serialise.Instances.Abstract
Agda.TypeChecking.Serialise.Instances.Common
Agda.TypeChecking.Serialise.Instances.Compilers
Agda.TypeChecking.Serialise.Instances.Highlighting
Agda.TypeChecking.Serialise.Instances.Internal
Agda.TypeChecking.Serialise.Instances.Errors
Agda.TypeChecking.SizedTypes
Agda.TypeChecking.SizedTypes.Solve
Agda.TypeChecking.SizedTypes.Syntax
Agda.TypeChecking.SizedTypes.Utils
Agda.TypeChecking.SizedTypes.WarshallSolver
Agda.TypeChecking.Sort
Agda.TypeChecking.Substitute
Agda.TypeChecking.Substitute.Class
Agda.TypeChecking.Substitute.DeBruijn
Agda.TypeChecking.SyntacticEquality
Agda.TypeChecking.Telescope
Agda.TypeChecking.Telescope.Path
Agda.TypeChecking.Unquote
Agda.TypeChecking.Warnings
Agda.TypeChecking.With
Agda.Utils.AffineHole
Agda.Utils.Applicative
Agda.Utils.AssocList
Agda.Utils.Bag
Agda.Utils.Benchmark
Agda.Utils.BiMap
Agda.Utils.CallStack
Agda.Utils.Char
Agda.Utils.Cluster
Agda.Utils.Empty
Agda.Utils.Environment
Agda.Utils.Either
Agda.Utils.Fail
Agda.Utils.Favorites
Agda.Utils.FileName
Agda.Utils.Float
Agda.Utils.Functor
Agda.Utils.Function
Agda.Utils.Graph.AdjacencyMap.Unidirectional
Agda.Utils.Graph.TopSort
Agda.Utils.Hash
Agda.Utils.Haskell.Syntax
Agda.Utils.Impossible
Agda.Utils.IndexedList
Agda.Utils.IntSet.Infinite
Agda.Utils.IO
Agda.Utils.IO.Binary
Agda.Utils.IO.Directory
Agda.Utils.IO.TempFile
Agda.Utils.IO.UTF8
Agda.Utils.IORef
Agda.Utils.Lens
Agda.Utils.Lens.Examples
Agda.Utils.List
Agda.Utils.List1
Agda.Utils.List2
Agda.Utils.ListT
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Maybe.Strict
Agda.Utils.Memo
Agda.Utils.Monad
Agda.Utils.Monoid
Agda.Utils.Null
Agda.Utils.Parser.MemoisedCPS
Agda.Utils.PartialOrd
Agda.Utils.Permutation
Agda.Utils.Pointer
Agda.Utils.POMonoid
Agda.Utils.Pretty
Agda.Utils.RangeMap
Agda.Utils.SemiRing
Agda.Utils.Semigroup
Agda.Utils.Singleton
Agda.Utils.Size
Agda.Utils.SmallSet
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.Three
Agda.Utils.Time
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.TypeLevel
Agda.Utils.TypeLits
Agda.Utils.Update
Agda.Utils.VarSet
Agda.Utils.Warshall
Agda.Utils.WithDefault
Agda.Utils.Zipper
Agda.Version
Agda.VersionCommit
other-modules: Paths_Agda
Agda.Interaction.Highlighting.Dot.Backend
Agda.Interaction.Highlighting.Dot.Base
Agda.Interaction.Highlighting.HTML.Backend
Agda.Interaction.Highlighting.HTML.Base
Agda.Interaction.Highlighting.LaTeX.Backend
Agda.Interaction.Highlighting.LaTeX.Base
Agda.Interaction.Options.Base
Agda.Interaction.Options.HasOptions
Agda.Utils.CallStack.Base
Agda.Utils.CallStack.Pretty
if flag(optimise-heavily)
ghc-options: -fexpose-all-unfoldings
-fspecialise-aggressively
-- NOTE: If adding flags, also add to `.ghci-8.0`
if impl(ghc <= 8.0.2)
ghc-options: -fprint-potential-instances
-- Initially, we disable all the warnings.
-w
-Wwarn
-- This option must be the first one after disabling the
-- warnings. See Issue #2094.
-Wunrecognised-warning-flags
-Wdeprecated-flags
-Wderiving-typeable
-Wdodgy-exports
-Wdodgy-foreign-imports
-Wdodgy-imports
-Wduplicate-exports
-Wempty-enumerations
-Widentities
-Wincomplete-patterns
-Winline-rule-shadowing
-Wmissing-fields
-Wmissing-methods
-Wmissing-pattern-synonym-signatures
-Wmissing-signatures
-Wnoncanonical-monad-instances
-Wnoncanonical-monoid-instances
-Woverflowed-literals
-Woverlapping-patterns
-Wsemigroup
-Wtabs
-Wtyped-holes
-Wunrecognised-pragmas
-Wunticked-promoted-constructors
-Wunused-do-bind
-Wunused-foralls
-Wwarnings-deprecations
-Wwrong-do-bind
else
ghc-options: -fprint-potential-instances
-Wwarn=unrecognised-warning-flags
-Wwarn=deprecated-flags
-Wwarn=deriving-typeable
-Wwarn=dodgy-exports
-Wwarn=dodgy-foreign-imports
-Wwarn=dodgy-imports
-Wwarn=duplicate-exports
-Wwarn=empty-enumerations
-Wwarn=identities
-Wwarn=incomplete-patterns
-Wwarn=inline-rule-shadowing
-Wwarn=missing-fields
-Wwarn=missing-methods
-Wwarn=missing-pattern-synonym-signatures
-Wwarn=missing-signatures
-Wwarn=noncanonical-monad-instances
-Wwarn=noncanonical-monoid-instances
-Wwarn=overflowed-literals
-Wwarn=overlapping-patterns
-Wwarn=semigroup
-Wwarn=tabs
-Wwarn=typed-holes
-Wwarn=unrecognised-pragmas
-Wwarn=unticked-promoted-constructors
-Wwarn=unused-do-bind
-Wwarn=unused-foralls
-Wwarn=warnings-deprecations
-Wwarn=wrong-do-bind
-- NOTE: If adding or removing flags, also change `.ghci-8.2`
if impl(ghc >= 8.2)
ghc-options: -Wcpp-undef
-- ASR TODO (2017-07-23): `make haddock` fails when
-- this flag is on.
-- -Wmissing-home-modules
-Wwarn=simplifiable-class-constraints
-Wwarn=unbanged-strict-patterns
-- NOTE: If adding or removing flags, also change `.ghci-8.6`
if impl(ghc >= 8.6)
ghc-options: -Wwarn=inaccessible-code
-Wwarn=star-binder
-Wwarn=star-is-type
-- The following warning is an error in GHC >= 8.10.
if impl(ghc >= 8.6) && impl(ghc < 8.10)
ghc-options: -Wwarn=implicit-kind-vars
-- NOTE: If adding or removing flags, also change `.ghci-8.8`
if impl(ghc >= 8.8)
ghc-options: -Wwarn=missed-extra-shared-lib
-- NOTE: If adding or removing flags, also change `.ghci-8.10`
if impl(ghc >= 8.10)
ghc-options: -Wwarn=deriving-defaults
-Wwarn=redundant-record-wildcards
-Wwarn=unused-packages
-Wwarn=unused-record-wildcards
-- NOTE: If adding or removing flags, also change `.ghci-9.0`
if impl(ghc >= 9.0)
ghc-options: -Wwarn=invalid-haddock
default-language: Haskell2010
-- NOTE: If adding or removing default extensions, also change:
-- .ghci-8.0
-- .hlint.yaml
-- This should also use the same extensions as the `test-suite` target below.
default-extensions: BangPatterns
, ConstraintKinds
--L-T Chen (2019-07-15):
-- Enabling DataKinds only locally makes the compile time
-- slightly shorter, see PR #3920.
--, DataKinds
, DefaultSignatures
, DeriveDataTypeable
, DeriveFoldable
, DeriveFunctor
, DeriveGeneric
, DeriveTraversable
, ExistentialQuantification
, FlexibleContexts
, FlexibleInstances
, FunctionalDependencies
, GeneralizedNewtypeDeriving
, InstanceSigs
, LambdaCase
, MultiParamTypeClasses
, MultiWayIf
, NamedFieldPuns
, OverloadedStrings
, PatternSynonyms
, RankNTypes
, RecordWildCards
, ScopedTypeVariables
, StandaloneDeriving
, TupleSections
, TypeFamilies
, TypeSynonymInstances
executable agda
hs-source-dirs: src/main
main-is: Main.hs
build-depends: Agda
-- A version range on Agda generates a warning with
-- some versions of Cabal and GHC
-- (e.g. cabal-install version 1.24.0.2 compiled
-- using version 1.24.2.0 of the Cabal library and
-- GHC 8.2.1 RC1).
-- Nothing is used from the following package,
-- except for the Prelude.
, base
default-language: Haskell2010
-- If someone installs Agda with the setuid bit set, then the
-- presence of +RTS may be a security problem (see GHC bug #3910).
-- However, we sometimes recommend people to use +RTS to control
-- Agda's memory usage, so we want this functionality enabled by
-- default.
-- The threaded RTS by default starts a major GC after a program has
-- been idle for 0.3 s. This feature turned out to be annoying, so
-- the idle GC is now by default turned off (-I0).
ghc-options: -threaded -rtsopts
"-with-rtsopts=-M3.5G -I0"
executable agda-mode
hs-source-dirs: src/agda-mode
main-is: Main.hs
other-modules: Paths_Agda
build-depends: base >= 4.9.0.0 && < 4.18
, directory >= 1.2.6.2 && < 1.4
, filepath >= 1.4.1.0 && < 1.5
, process >= 1.4.2.0 && < 1.7
default-language: Haskell2010

11
Agda-HashMap.patch Normal file
View File

@ -0,0 +1,11 @@
--- Agda-2.4.2.5/src/full/Agda/Utils/HashMap.hs~ 2015-12-19 06:29:26.000000000 +0900
+++ Agda-2.4.2.5/src/full/Agda/Utils/HashMap.hs 2016-10-06 14:19:19.071676894 +0900
@@ -5,7 +5,7 @@
) where
import Data.Hashable
-import Data.HashMap.Strict as HashMap
+import Data.HashMap.Strict as HashMap hiding (alter, mapMaybe)
import qualified Data.Maybe as Maybe
-- | Like 'Data.Map.Strict.mapMaybe'.

393
Agda.spec
View File

@ -1,62 +1,141 @@
# https://fedoraproject.org/wiki/Packaging:Haskell
# generated by cabal-rpm-2.1.0 --subpackage
# https://docs.fedoraproject.org/en-US/packaging-guidelines/Haskell/
# https://gitlab.haskell.org/ghc/ghc/issues/17030 panic
%ifarch %{ix86}
%undefine with_ghc_prof
%endif
%global pkg_name Agda
%global pkgver %{pkg_name}-%{version}
%global geniplatemirror geniplate-mirror-0.7.9
%global murmurhash murmur-hash-0.1.0.10
%global subpkgs %{geniplatemirror} %{murmurhash}
Name: %{pkg_name}
Version: 2.4.2.2
Release: 5%{?dist}
Version: 2.6.2.2
# can only be reset when all subpkgs bumped
Release: 38%{?dist}
Summary: A dependently typed functional programming language and proof assistant
License: MIT and BSD
License: MIT and BSD-3-Clause
Url: https://hackage.haskell.org/package/%{name}
Source0: https://hackage.haskell.org/package/%{name}-%{version}/%{name}-%{version}.tar.gz
Source1: agda-mode-init.el
# Begin cabal-rpm sources:
Source0: https://hackage.haskell.org/package/%{pkgver}/%{pkgver}.tar.gz
Source1: https://hackage.haskell.org/package/%{geniplatemirror}/%{geniplatemirror}.tar.gz
Source2: https://hackage.haskell.org/package/%{murmurhash}/%{murmurhash}.tar.gz
Source3: https://hackage.haskell.org/package/%{pkgver}/%{name}.cabal#/%{pkgver}.cabal
# End cabal-rpm sources
Source10: agda-mode-init.el
# armv7hl:
#[372 of 397] Compiling Agda.Interaction.Imports
#ghc: out of memory [even with -O0]
# https://bugzilla.redhat.com/show_bug.cgi?id=1991261
#
# i686: hangs in ghc_lib_install
#Installing executable agda-mode in /builddir/build/BUILDROOT/Agda-2.6.2.2-36.fc37.i386/usr/bin
#Warning: Executable installed in
#/builddir/build/BUILDROOT/Agda-2.6.2.2-36.fc37.i386/usr/bin
#Installing library in /builddir/build/BUILDROOT/Agda-2.6.2.2-36.fc37.i386/usr/lib/ghc-8.10.7/Agda-2.6.2.2
#Installing executable agda in /builddir/build/BUILDROOT/Agda-2.6.2.2-36.fc37.i386/usr/bin
#Warning: Executable installed in
#/builddir/build/BUILDROOT/Agda-2.6.2.2-36.fc37.i386/usr/bin
# https://bugzilla.redhat.com/show_bug.cgi?id=2098425
ExcludeArch: armv7hl %{ix86}
BuildRequires: ghc-Cabal-devel
BuildRequires: ghc-rpm-macros
# Begin cabal-rpm deps:
BuildRequires: alex
BuildRequires: chrpath
BuildRequires: cpphs
BuildRequires: ghc-QuickCheck-devel >= 2.7.5
BuildRequires: ghc-STMonadTrans-devel
BuildRequires: dos2unix
BuildRequires: ghc-Cabal-devel
BuildRequires: ghc-rpm-macros-extra
BuildRequires: ghc-aeson-devel
BuildRequires: ghc-array-devel
BuildRequires: ghc-async-devel
BuildRequires: ghc-base-devel
BuildRequires: ghc-binary-devel
BuildRequires: ghc-blaze-html-devel
BuildRequires: ghc-boxes-devel
BuildRequires: ghc-bytestring-devel
BuildRequires: ghc-case-insensitive-devel
BuildRequires: ghc-containers-devel
BuildRequires: ghc-data-hash-devel
BuildRequires: ghc-deepseq-devel
BuildRequires: ghc-directory-devel
BuildRequires: ghc-edit-distance-devel
BuildRequires: ghc-equivalence-devel
BuildRequires: ghc-exceptions-devel
BuildRequires: ghc-filepath-devel
BuildRequires: ghc-geniplate-devel
BuildRequires: ghc-ghc-compact-devel
BuildRequires: ghc-gitrev-devel
BuildRequires: ghc-hashable-devel
BuildRequires: ghc-hashtables-devel
BuildRequires: ghc-haskeline-devel
BuildRequires: ghc-haskell-src-exts-devel
BuildRequires: ghc-monad-control-devel
BuildRequires: ghc-mtl-devel
#BuildRequires: ghc-murmur-hash-devel
BuildRequires: ghc-parallel-devel
BuildRequires: ghc-pretty-devel
BuildRequires: ghc-process-devel
BuildRequires: ghc-regex-tdfa-devel
BuildRequires: ghc-split-devel
BuildRequires: ghc-stm-devel
BuildRequires: ghc-strict-devel
BuildRequires: ghc-template-haskell-devel
BuildRequires: ghc-text-devel
BuildRequires: ghc-time-devel
BuildRequires: ghc-transformers-devel
BuildRequires: ghc-unordered-containers-devel
BuildRequires: ghc-xhtml-devel
BuildRequires: ghc-uri-encode-devel
BuildRequires: ghc-zlib-devel
%if %{with ghc_prof}
BuildRequires: ghc-aeson-prof
BuildRequires: ghc-array-prof
BuildRequires: ghc-async-prof
BuildRequires: ghc-base-prof
BuildRequires: ghc-binary-prof
BuildRequires: ghc-blaze-html-prof
BuildRequires: ghc-boxes-prof
BuildRequires: ghc-bytestring-prof
BuildRequires: ghc-case-insensitive-prof
BuildRequires: ghc-containers-prof
BuildRequires: ghc-data-hash-prof
BuildRequires: ghc-deepseq-prof
BuildRequires: ghc-directory-prof
BuildRequires: ghc-edit-distance-prof
BuildRequires: ghc-equivalence-prof
BuildRequires: ghc-exceptions-prof
BuildRequires: ghc-filepath-prof
BuildRequires: ghc-ghc-compact-prof
BuildRequires: ghc-gitrev-prof
BuildRequires: ghc-hashable-prof
BuildRequires: ghc-hashtables-prof
BuildRequires: ghc-haskeline-prof
BuildRequires: ghc-monad-control-prof
BuildRequires: ghc-mtl-prof
#BuildRequires: ghc-murmur-hash-prof
BuildRequires: ghc-parallel-prof
BuildRequires: ghc-pretty-prof
BuildRequires: ghc-process-prof
BuildRequires: ghc-regex-tdfa-prof
BuildRequires: ghc-split-prof
BuildRequires: ghc-stm-prof
BuildRequires: ghc-strict-prof
BuildRequires: ghc-template-haskell-prof
BuildRequires: ghc-text-prof
BuildRequires: ghc-time-prof
BuildRequires: ghc-transformers-prof
BuildRequires: ghc-unordered-containers-prof
BuildRequires: ghc-uri-encode-prof
BuildRequires: ghc-zlib-prof
%endif
BuildRequires: alex
BuildRequires: happy
ExclusiveArch: %{ghc_arches_with_ghci}
Provides: agda = %{version}-%{release}
Requires: %{name}-common = %{version}-%{release}
# End cabal-rpm deps
BuildRequires: emacs(bin)
# geniplate uses template-haskell
ExclusiveArch: %{ghc_arches_with_ghci}
# bug 991929
ExcludeArch: %{arm}
Requires: ghc-%{name}-devel = %{version}-%{release}
# introduced for F23
Obsoletes: emacs-agda-el < 2.4.2.2-5
Provides: emacs-agda = %{version}-%{release}
@ -75,8 +154,18 @@ 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 common
Summary: %{name} common files
License: MIT and BSD-3-Clause and BSD-2-Clause
BuildArch: noarch
%description common
This package provides the %{name} core libraries and runtime related files.
%package -n ghc-%{name}
Summary: Haskell %{name} library
Requires: %{name}-common = %{version}-%{release}
%description -n ghc-%{name}
This package provides the Haskell %{name} shared library.
@ -85,20 +174,55 @@ This package provides the Haskell %{name} shared library.
%package -n ghc-%{name}-devel
Summary: Haskell %{name} library development files
Provides: ghc-%{name}-static = %{version}-%{release}
Provides: ghc-%{name}-static%{?_isa} = %{version}-%{release}
%if %{defined ghc_version}
Requires: ghc-compiler = %{ghc_version}
Requires(post): ghc-compiler = %{ghc_version}
Requires(postun): ghc-compiler = %{ghc_version}
%endif
Requires: ghc-%{name}%{?_isa} = %{version}-%{release}
Obsoletes: Agda < 2.3.1
%description -n ghc-%{name}-devel
This package provides the Haskell %{name} library development files.
%prep
%setup -q
%if %{with haddock}
%package -n ghc-%{name}-doc
Summary: Haskell %{name} library documentation
BuildArch: noarch
Requires: ghc-filesystem
# tweak the Agda version in the emacs mode
%description -n ghc-%{name}-doc
This package provides the Haskell %{name} library documentation.
%endif
%if %{with ghc_prof}
%package -n ghc-%{name}-prof
Summary: Haskell %{name} profiling library
Requires: ghc-%{name}-devel%{?_isa} = %{version}-%{release}
Supplements: (ghc-%{name}-devel and ghc-prof)
%description -n ghc-%{name}-prof
This package provides the Haskell %{name} profiling library.
%endif
%global main_version %{version}
%if %{defined ghclibdir}
%ghc_lib_subpackage -l BSD-3-Clause %{geniplatemirror}
%ghc_lib_subpackage -l BSD-3-Clause %{murmurhash}
%endif
%global version %{main_version}
%prep
# Begin cabal-rpm setup:
%setup -q -a1 -a2
dos2unix -k -n %{SOURCE3} %{name}.cabal
# End cabal-rpm setup
# check 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
@ -106,9 +230,10 @@ fi
%build
%define elisp_files eri.el agda-input.el annotation.el agda2-highlight.el agda2-abbrevs.el agda2-queue.el agda2-mode.el agda2.el
%define elisp_files eri.el agda-input.el annotation.el agda2-highlight.el agda2-abbrevs.el agda2-queue.el agda2-mode.el agda2-mode-pkg.el agda2.el
# check no missing new elisp files
(
cd src/data/emacs-mode
for i in *.el; do
if ! echo %{elisp_files} | grep -q $i; then
@ -116,28 +241,35 @@ for i in *.el; do
exit 1
fi
done
cd -
)
# cpphs: src/full/Agda/Interaction/BasicOps.hs: hGetContents: invalid argument (invalid byte sequence)
LANG=en_US.utf8
%ghc_lib_build
# 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
# Begin cabal-rpm build:
%ghc_libs_build %{subpkgs}
%ifarch armv7hl
# https://bugzilla.redhat.com/show_bug.cgi?id=991929
%define cabal_configure_options --ghc-options="-O0"
%endif
%ghc_lib_build
# End cabal-rpm build
(
cd src/data/emacs-mode
for i in %elisp_files; do
%{_emacs_bytecompile} $i
done
cd -
)
%install
# Begin cabal-rpm install
%ghc_libs_install %{subpkgs}
%ghc_lib_install
mv %{buildroot}%{_ghcdocdir}{,-common}
# End cabal-rpm install
%ghc_fix_dynamic_rpath agda
for i in $(find %{buildroot}%{_datadir}/%{pkgver} -name "*.agda"); do
Agda_datadir=%{buildroot}%{_datadir}/%{pkgver} LD_LIBRARY_PATH=%{buildroot}%{_ghcdynlibdir} %{buildroot}%{_bindir}/agda $i
done
mkdir -p %{buildroot}%{_emacs_sitelispdir}/agda
for i in src/data/emacs-mode/*; do
@ -145,47 +277,184 @@ for i in src/data/emacs-mode/*; do
done
mkdir -p %{buildroot}%{_emacs_sitestartdir}
install -p -m 0644 %SOURCE1 %{buildroot}%{_emacs_sitestartdir}
install -p -m 0644 %SOURCE10 %{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
rm %{buildroot}%{_docdir}/%{name}*/LICENSE
%post -n ghc-%{name}
%{_bindir}/agda %{_datadir}/%{name}-%{version}/lib/prim/Agda/Primitive.agda || :
%post -n ghc-%{name}-devel
%ghc_pkg_recache
%postun -n ghc-%{name}-devel
%ghc_pkg_recache
rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode
%files
%doc README.md
# Begin cabal-rpm files:
%{_bindir}/agda
# End cabal-rpm files
%dir %{_emacs_sitelispdir}/agda
%{_emacs_sitelispdir}/agda/*.el
%{_emacs_sitelispdir}/agda/*.elc
%{_emacs_sitestartdir}/*.el
%files common
# Begin cabal-rpm files:
%license LICENSE
%doc CHANGELOG.md README.md
%{_datadir}/%{pkgver}
# End cabal-rpm files
%files -n ghc-%{name} -f ghc-%{name}.files
%doc LICENSE
%{_bindir}/agda
%{_datadir}/%{name}-%{version}
%ghost %{_datadir}/%{name}-%{version}/lib/prim/Agda/Primitive.agdai
%files -n ghc-%{name}-devel -f ghc-%{name}-devel.files
%doc CHANGELOG
%if %{with haddock}
%files -n ghc-%{name}-doc -f ghc-%{name}-doc.files
%license LICENSE
%endif
%if %{with ghc_prof}
%files -n ghc-%{name}-prof -f ghc-%{name}-prof.files
%endif
%changelog
* Sat Feb 18 2023 Jens Petersen <petersen@redhat.com> - 2.6.2.2-38
- refresh to cabal-rpm-2.1.0 including SPDX migration
- bump geniplate-mirror to 0.7.9
* Wed Jul 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2.2-37
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
* Mon Jun 20 2022 Jens Petersen <petersen@redhat.com>
- add Provides agda
* Tue Jun 7 2022 Jens Petersen <petersen@redhat.com> - 2.6.2.2-36
- https://hackage.haskell.org/package/Agda-2.6.2.2/changelog
- disable i686 (#2098425)
* Mon Mar 07 2022 Jens Petersen <petersen@redhat.com> - 2.6.2.1-35
- https://hackage.haskell.org/package/Agda-2.6.2.1/changelog
* Wed Jan 19 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-34
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
* Sat Jan 08 2022 Miro Hrončok <mhroncok@redhat.com> - 2.6.2-33
- Rebuilt for https://fedoraproject.org/wiki/Changes/LIBFFI34
* Thu Aug 5 2021 Jens Petersen <petersen@redhat.com> - 2.6.2-32
- update to 2.6.2
- https://hackage.haskell.org/package/Agda-2.6.2/changelog
- disable armv7hl due to out of memory (#73471404)
* Thu Aug 5 2021 Jens Petersen <petersen@redhat.com> - 2.6.1.3-32
- update to 2.6.1.3
* Wed Jul 21 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-31
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
* Mon Jan 25 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-30
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
* Sun Oct 11 2020 Jeff Law <aw@redhat.com> - 2.6.1-29
- Re-enable LTO
* Tue Sep 1 2020 Jens Petersen <petersen@redhat.com> - 2.6.1-28
- uri-encode has been packaged
* Fri Jul 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-27
- Second attempt - Rebuilt for
https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
* Mon Jul 27 2020 Jeff Law <aw@redhat.com> - 2.6.1-26
- Disable LTO on s390
* Mon Jul 27 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-25
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
* Mon Jul 20 2020 Jens Petersen <petersen@redhat.com> - 2.6.1-24
- enable armv7hl with -O0
* Sun Jun 07 2020 Jens Petersen <petersen@redhat.com> - 2.6.1-23
- update to 2.6.1
- drop EdisonCore and EdisonAPI deps
* Wed May 27 2020 Jens Petersen <petersen@redhat.com> - 2.6.0.1-22
- move statically linked /usr/bin/agda and datadir into base package
- also drop common subpackage
* Thu Feb 20 2020 Jens Petersen <petersen@redhat.com> - 2.6.0.1-21
- refresh to cabal-rpm-2.0.2
* Tue Jan 28 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0.1-20
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
* Thu Jul 25 2019 Jens Petersen <petersen@redhat.com> - 2.6.0.1-19
- update to 2.6.0.1
- disable prof for i686
* Wed Jul 24 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4.2-18
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
* Thu Feb 21 2019 Jens Petersen <petersen@redhat.com> - 2.5.4.2-17
- update to 2.5.4.2
* Sun Feb 17 2019 Jens Petersen <petersen@redhat.com> - 2.5.3-16
- refresh to cabal-rpm-0.13
* Thu Jan 31 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.3-15
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
* Thu Jul 19 2018 Jens Petersen <petersen@redhat.com> - 2.5.3-14
- update to EdisonCore-1.3.2.1 and geniplate-mirror-0.7.6
- revise .cabal file
* Thu Jul 12 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.3-13
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.3-12
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
* Tue Jan 02 2018 Jens Petersen <petersen@redhat.com> - 2.5.3-11
- update to 2.5.3
- add uri-encode subpackage
* Tue Dec 26 2017 Jens Petersen <petersen@redhat.com> - 2.5.2-10
- ieee754 is now a separate package
* Wed Nov 15 2017 Jens Petersen <petersen@redhat.com> - 2.5.2-9
- gitrev is now packaged in Fedora
* Fri Nov 10 2017 Jens Petersen <petersen@redhat.com> - 2.5.2-8
- geniplate-mirror-0.7.5
- gitrev-1.3.1 (#1511680)
* Wed Aug 02 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.2-7.1
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
* Wed Jul 26 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.2-6.1
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
* Sun Mar 12 2017 Jens Petersen <petersen@redhat.com> - 2.5.2-5
- compile .agda files at buildtime
* Fri Mar 10 2017 Jens Petersen <petersen@redhat.com> - 2.5.2-4
- update to 2.5.2
- subpackage EdisonAPI, EdisonCore, gitrev, ieee754, monadplus, murmur-hash
* Fri Feb 10 2017 Fedora Release Engineering <releng@fedoraproject.org> - 2.4.2.5-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
* Thu Feb 9 2017 Jens Petersen <petersen@redhat.com> - 2.4.2.5-2
- build subpackage inside main package
* Thu Oct 6 2016 Jens Petersen <petersen@redhat.com> - 2.4.2.5-1
- update to 2.4.2.5
- subpackage new dep geniplate-mirror
* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 2.4.2.2-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Wed Jul 22 2015 Jens Petersen <petersen@redhat.com> - 2.4.2.2-5
- drop emacs subpackages (#1234569)

View File

@ -1 +1,3 @@
3608c4305d32af66807c8189ffc719f5 Agda-2.4.2.2.tar.gz
SHA512 (Agda-2.6.2.2.tar.gz) = f54dcc0fd6dea106db4a04cc3b0b80f404f0613b5075849db17a1b4b5e176ed6d183bfdaf464fbcbc6e0807c1af0c8748f96552d48e537444109be54730685a8
SHA512 (geniplate-mirror-0.7.9.tar.gz) = b125680148ca808422ba4ddc85e0dfb8429d1906d90182ebcc8443dd4c9f02742c6fc002adcc487b3c17be811b02dca4a277485d32a57a5b581647182b04f452
SHA512 (murmur-hash-0.1.0.10.tar.gz) = d6d28fcd738de98ce4fb6c7e997b32bb15eef9efe53642cefffd2cfeccd1b56f634adbcadeec9fb94c69d1df9e675f7daf368c62806ef819dc242df947ddf70b