Compare commits
89 Commits
| Author | SHA1 | Date |
|---|---|---|
Jens Petersen
|
659376cb02 | |
|
Jens Petersen
|
cd72da1b95 | |
|
Jens Petersen
|
938a3e810b | |
|
Jens Petersen
|
ccdfcab907 | |
Fedora Release Engineering
|
6a1a838a85 | |
|
Jens Petersen
|
5383d0287c | |
|
Jens Petersen
|
31a616d83e | |
|
Jens Petersen
|
f6f1c37003 | |
|
Jens Petersen
|
f21a1029c6 | |
|
Fedora Release Engineering
|
24e46c692e | |
Miro Hrončok
|
ff1d99479b | |
|
Jens Petersen
|
af39028c46 | |
|
Jens Petersen
|
5d5c715600 | |
|
Jens Petersen
|
7625567586 | |
|
Jens Petersen
|
3e99f24800 | |
|
Jens Petersen
|
99d2241eeb | |
|
Jens Petersen
|
14d6c0b37e | |
|
Jens Petersen
|
63734cebf1 | |
|
Fedora Release Engineering
|
33b2b4d0b9 | |
|
Fedora Release Engineering
|
300a13f672 | |
|
Fedora Release Engineering
|
1786c87680 | |
Jeff Law
|
c9ed43346d | |
|
Jens Petersen
|
147e1019eb | |
|
Jens Petersen
|
2869a2b3a9 | |
|
Fedora Release Engineering
|
e0dc3e1641 | |
|
Jeff Law
|
89dbda77ba | |
|
Fedora Release Engineering
|
ac21eaf931 | |
|
Jens Petersen
|
8b113d48b1 | |
|
Jens Petersen
|
02a60d692c | |
|
Jens Petersen
|
a122f588a5 | |
|
Jens Petersen
|
36e744de86 | |
|
Jens Petersen
|
c4c53b3fea | |
|
Jens Petersen
|
0c769109ae | |
|
Fedora Release Engineering
|
f23bc8455f | |
|
Jens Petersen
|
2c0f7876b1 | |
|
Jens Petersen
|
d98367819a | |
|
Jens Petersen
|
55fb1c20ea | |
|
Jens Petersen
|
900142581b | |
|
Jens Petersen
|
6365bc309c | |
|
Jens Petersen
|
13455a7ccc | |
|
Jens Petersen
|
93c549754b | |
|
Fedora Release Engineering
|
64d8785d63 | |
|
Jens Petersen
|
31025ad40c | |
|
Jens Petersen
|
9e6df6678b | |
|
Fedora Release Engineering
|
381aecc283 | |
|
Jens Petersen
|
054a111019 | |
|
Jens Petersen
|
fcada7d934 | |
|
Jens Petersen
|
42213812a5 | |
|
Fedora Release Engineering
|
168de37e16 | |
|
Fedora Release Engineering
|
a9910c7a85 | |
|
Jens Petersen
|
8243be8dc8 | |
|
Jens Petersen
|
803ef2a83d | |
|
Jens Petersen
|
377de8fb8c | |
|
Jens Petersen
|
c450966ea6 | |
|
Jens Petersen
|
413d9c1463 | |
|
Jens Petersen
|
423f8f8744 | |
|
Jens Petersen
|
e2ed4b024d | |
|
Jens Petersen
|
253d8eaad6 | |
|
Jens Petersen
|
5bc04f5759 | |
|
Jens Petersen
|
56bc32af70 | |
|
Jens Petersen
|
e8fe124f84 | |
|
Fedora Release Engineering
|
df02d5a6af | |
|
Fedora Release Engineering
|
77178c0167 | |
|
Jens Petersen
|
04232b3527 | |
|
Jens Petersen
|
d5e4024144 | |
|
Jens Petersen
|
8982741ffc | |
|
Jens Petersen
|
4e6c542e8f | |
|
Jens Petersen
|
1d4dc8f354 | |
|
Jens Petersen
|
7d30bcc63e | |
|
Jens Petersen
|
64f09036ec | |
|
Jens Petersen
|
1072e25653 | |
|
Jens Petersen
|
4feb7091aa | |
|
Fedora Release Engineering
|
63da85a065 | |
|
Jens Petersen
|
d76f81bcf8 | |
|
Jens Petersen
|
108650930d | |
|
Jens Petersen
|
1bb4e49a1c | |
|
Jens Petersen
|
540194fe1a | |
|
Jens Petersen
|
7be71ac292 | |
|
Jens Petersen
|
4f10ceb221 | |
|
Jens Petersen
|
c4dd38eef5 | |
|
Jens Petersen
|
ac0a36269a | |
|
Jens Petersen
|
afe3c95527 | |
|
Jens Petersen
|
6ceb8aa2fd | |
|
Jens Petersen
|
42b7c9e446 | |
|
Jens Petersen
|
12a5988583 | |
|
Jens Petersen
|
8b9cf04092 | |
Jens Petersen
|
2219348db1 | |
|
Jens Petersen
|
290b41f098 | |
Dennis Gilmore
|
ec50775e58 |
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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ö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
|
||||
|
|
@ -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ö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
|
||||
|
|
@ -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
393
Agda.spec
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
4
sources
4
sources
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue