Compare commits
29 commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
87281fb4a8 | ||
|
|
4a50bc87bb | ||
|
d3a2f2a2fb | ||
|
|
396e77c1f7 | ||
|
|
6bdbc99306 | ||
|
|
1b9700d516 | ||
|
|
d6d8fa2900 | ||
|
|
b9f8a1efa3 | ||
|
feccefbb57 | ||
|
|
59158d61c7 | ||
|
|
fbbd3d02da | ||
|
|
f36c6423e5 | ||
|
|
1a9af345c2 | ||
|
|
1a1cd5d1e6 | ||
|
|
5031cf6fd6 | ||
|
|
90aee6980b | ||
|
|
be456d7df5 | ||
|
|
7f51bce47f | ||
|
|
abfe655f51 | ||
|
|
ec32a41fe6 | ||
|
|
96753cfc99 | ||
|
|
6c97ffba9c | ||
|
|
077d4357e7 | ||
|
|
1a0b9834e3 | ||
|
|
f086758742 | ||
|
|
6100f35886 | ||
|
|
123e0ac5ea | ||
|
|
e298cd0fb9 | ||
|
|
9185a5a148 |
5 changed files with 1989 additions and 884 deletions
22
.gitignore
vendored
22
.gitignore
vendored
|
|
@ -29,3 +29,25 @@
|
|||
/murmur-hash-0.1.0.10.tar.gz
|
||||
/Agda-2.6.2.2.tar.gz
|
||||
/geniplate-mirror-0.7.9.tar.gz
|
||||
/Agda-2.6.3.tar.gz
|
||||
/vector-hashtables-0.1.1.3.tar.gz
|
||||
/Agda-2.6.4.tar.gz
|
||||
/peano-0.1.0.1.tar.gz
|
||||
/Agda-2.6.4.1.tar.gz
|
||||
/peano-0.1.0.2.tar.gz
|
||||
/vector-hashtables-0.1.1.4.tar.gz
|
||||
/Agda-2.6.4.3.tar.gz
|
||||
/vector-hashtables-0.1.2.0.tar.gz
|
||||
/Agda-2.7.0.1.tar.gz
|
||||
/pqueue-1.5.0.0.tar.gz
|
||||
/murmur-hash-0.1.0.11.tar.gz
|
||||
/Agda-2.8.0.tar.gz
|
||||
/ListLike-4.7.8.3.tar.gz
|
||||
/ap-normalize-0.1.0.1.tar.gz
|
||||
/fmlist-0.9.4.tar.gz
|
||||
/generic-data-1.1.0.2.tar.gz
|
||||
/nonempty-containers-0.3.5.0.tar.gz
|
||||
/nonempty-vector-0.2.4.tar.gz
|
||||
/process-extras-0.7.4.tar.gz
|
||||
/show-combinators-0.2.0.0.tar.gz
|
||||
/vector-hashtables-0.1.2.1.tar.gz
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
896
Agda-2.7.0.1.cabal
Normal file
896
Agda-2.7.0.1.cabal
Normal file
|
|
@ -0,0 +1,896 @@
|
|||
cabal-version: 2.4
|
||||
name: Agda
|
||||
version: 2.7.0.1
|
||||
x-revision: 2
|
||||
build-type: Custom
|
||||
license: MIT
|
||||
license-file: LICENSE
|
||||
copyright: (c) 2005-2024 The Agda Team.
|
||||
author: The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
|
||||
maintainer: The Agda Team
|
||||
homepage: https://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).
|
||||
|
||||
tested-with:
|
||||
GHC == 9.10.1
|
||||
GHC == 9.8.2
|
||||
GHC == 9.6.6
|
||||
GHC == 9.4.8
|
||||
GHC == 9.2.8
|
||||
GHC == 9.0.2
|
||||
GHC == 8.10.7
|
||||
GHC == 8.8.4
|
||||
GHC == 8.6.5
|
||||
|
||||
extra-doc-files:
|
||||
CHANGELOG.md
|
||||
README.md
|
||||
doc/user-manual/agda.svg
|
||||
doc/release-notes/2.6.4.3.md
|
||||
doc/release-notes/2.6.4.2.md
|
||||
doc/release-notes/2.6.4.1.md
|
||||
doc/release-notes/2.6.4.md
|
||||
doc/release-notes/2.6.3.md
|
||||
doc/release-notes/2.6.2.2.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
|
||||
|
||||
extra-source-files:
|
||||
stack-9.10.1.yaml
|
||||
stack-9.8.2.yaml
|
||||
stack-9.6.6.yaml
|
||||
stack-9.4.8.yaml
|
||||
stack-9.2.8.yaml
|
||||
stack-9.0.2.yaml
|
||||
stack-8.10.7.yaml
|
||||
stack-8.8.4.yaml
|
||||
|
||||
data-dir:
|
||||
src/data
|
||||
|
||||
data-files:
|
||||
emacs-mode/*.el
|
||||
html/Agda.css
|
||||
html/highlight-hover.js
|
||||
JS/agda-rts.js
|
||||
JS/agda-rts.amd.js
|
||||
latex/agda.sty
|
||||
latex/postprocess-latex.pl
|
||||
lib/prim/agda-builtins.agda-lib
|
||||
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/Equiv.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.7.0.1
|
||||
|
||||
-- Build flags
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
flag debug
|
||||
default: False
|
||||
manual: True
|
||||
description:
|
||||
Enable debug printing. This makes Agda slightly slower, and
|
||||
building Agda slower as well. The --verbose=N option only
|
||||
has an effect when Agda was built with this flag.
|
||||
|
||||
flag debug-serialisation
|
||||
default: False
|
||||
manual: True
|
||||
description:
|
||||
Enable debug mode in serialisation. This makes serialisation slower.
|
||||
|
||||
flag debug-parsing
|
||||
default: False
|
||||
manual: True
|
||||
description:
|
||||
Enable debug mode in parsing. This makes parsing slower.
|
||||
|
||||
flag enable-cluster-counting
|
||||
default: False
|
||||
manual: True
|
||||
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
|
||||
manual: True
|
||||
description:
|
||||
Enable some expensive optimisations when compiling Agda.
|
||||
|
||||
-- Setup
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
custom-setup
|
||||
setup-depends:
|
||||
, base >= 4.12.0.0 && < 4.21
|
||||
, Cabal >= 2.4.0.1 && < 3.13
|
||||
, directory >= 1.3.3.0 && < 1.4
|
||||
, filepath >= 1.4.2.1 && < 1.6
|
||||
, process >= 1.6.3.0 && < 1.7
|
||||
|
||||
-- Common stanzas
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
common language
|
||||
|
||||
if flag(optimise-heavily)
|
||||
cpp-options:
|
||||
-DOPTIMISE_HEAVILY
|
||||
ghc-options:
|
||||
-fexpose-all-unfoldings
|
||||
-fspecialise-aggressively
|
||||
|
||||
ghc-options:
|
||||
-- ASR (2022-05-31). Workaround to Issue #5932.
|
||||
-Wwarn
|
||||
-Wwarn=cpp-undef
|
||||
-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=inaccessible-code
|
||||
-Wwarn=inline-rule-shadowing
|
||||
-Wwarn=missing-fields
|
||||
-Wwarn=missing-home-modules
|
||||
-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=redundant-constraints
|
||||
-Wwarn=simplifiable-class-constraints
|
||||
-Wwarn=star-binder
|
||||
-Wwarn=star-is-type
|
||||
-Wwarn=tabs
|
||||
-Wwarn=typed-holes
|
||||
-Wwarn=unbanged-strict-patterns
|
||||
-Wwarn=unrecognised-pragmas
|
||||
-Wwarn=unrecognised-warning-flags
|
||||
-Wwarn=unticked-promoted-constructors
|
||||
-Wwarn=unused-do-bind
|
||||
-Wwarn=unused-foralls
|
||||
-Wwarn=warnings-deprecations
|
||||
-Wwarn=wrong-do-bind
|
||||
|
||||
-- The following warning is an error in GHC >= 8.10.
|
||||
if impl(ghc < 8.10)
|
||||
ghc-options:
|
||||
-Wwarn=implicit-kind-vars
|
||||
-- #6623: Turn off this (nameless) warning:
|
||||
-- "Pattern match checker exceeded (2000000) iterations in a case alternative."
|
||||
-- See: https://gitlab.haskell.org/ghc/ghc/-/issues/13464
|
||||
-Wno-incomplete-patterns
|
||||
-Wno-overlapping-patterns
|
||||
|
||||
if impl(ghc < 9.10)
|
||||
ghc-options:
|
||||
-Wwarn=semigroup
|
||||
-- The semigroup warning is deprecated in GHC 9.10
|
||||
|
||||
if impl(ghc >= 8.8)
|
||||
ghc-options:
|
||||
-Wwarn=missed-extra-shared-lib
|
||||
|
||||
if impl(ghc >= 8.10)
|
||||
ghc-options:
|
||||
-Wwarn=compat-unqualified-imports
|
||||
-Wwarn=deriving-defaults
|
||||
-Wwarn=redundant-record-wildcards
|
||||
-Wwarn=unused-packages
|
||||
-Wwarn=unused-record-wildcards
|
||||
|
||||
if impl(ghc >= 9.0)
|
||||
ghc-options:
|
||||
-Wwarn=invalid-haddock
|
||||
-- #6137: coverage checker works only sufficiently well from GHC 9.0
|
||||
-Wwarn=incomplete-patterns
|
||||
-Wwarn=incomplete-record-updates
|
||||
-Wwarn=overlapping-patterns
|
||||
|
||||
-- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed
|
||||
-- from 9.2.1 and added back in 9.2.2.
|
||||
if impl(ghc == 9.0.2 || >= 9.2.2)
|
||||
ghc-options:
|
||||
-Wwarn=unicode-bidirectional-format-characters
|
||||
|
||||
if impl(ghc >= 9.2)
|
||||
ghc-options:
|
||||
-Wwarn=operator-whitespace
|
||||
-Wwarn=redundant-bang-patterns
|
||||
|
||||
if impl(ghc >= 9.4)
|
||||
ghc-options:
|
||||
-Wwarn=type-equality-out-of-scope
|
||||
|
||||
if impl(ghc >= 9.4 && < 9.10)
|
||||
ghc-options:
|
||||
-Wwarn=forall-identifier
|
||||
-- The forall-identifier warning is deprecated in GHC 9.10
|
||||
|
||||
default-language: Haskell2010
|
||||
|
||||
-- NOTE: If adding or removing default extensions, also change:
|
||||
-- .hlint.yaml
|
||||
default-extensions:
|
||||
BangPatterns
|
||||
BlockArguments
|
||||
ConstraintKinds
|
||||
--L-T Chen (2019-07-15):
|
||||
-- Enabling DataKinds only locally makes the compile time
|
||||
-- slightly shorter, see PR #3920.
|
||||
-- DataKinds
|
||||
DefaultSignatures
|
||||
DeriveFoldable
|
||||
DeriveFunctor
|
||||
DeriveGeneric
|
||||
DeriveTraversable
|
||||
DerivingStrategies
|
||||
ExistentialQuantification
|
||||
FlexibleContexts
|
||||
FlexibleInstances
|
||||
FunctionalDependencies
|
||||
GADTs
|
||||
GeneralizedNewtypeDeriving
|
||||
InstanceSigs
|
||||
LambdaCase
|
||||
MultiParamTypeClasses
|
||||
MultiWayIf
|
||||
NamedFieldPuns
|
||||
OverloadedStrings
|
||||
PatternSynonyms
|
||||
RankNTypes
|
||||
RecordWildCards
|
||||
ScopedTypeVariables
|
||||
StandaloneDeriving
|
||||
TupleSections
|
||||
TypeFamilies
|
||||
TypeOperators
|
||||
TypeSynonymInstances
|
||||
ViewPatterns
|
||||
|
||||
other-extensions:
|
||||
CPP
|
||||
DeriveAnyClass
|
||||
PartialTypeSignatures
|
||||
|
||||
|
||||
-- Agda library
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
library
|
||||
import: language
|
||||
|
||||
hs-source-dirs: src/full
|
||||
|
||||
-- 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.
|
||||
--
|
||||
-- An exceptions are packages that are only needed for certain configurations,
|
||||
-- like for flags, Windows, etc.
|
||||
|
||||
if flag(debug)
|
||||
cpp-options: -DDEBUG
|
||||
|
||||
if flag(debug-serialisation)
|
||||
cpp-options: -DDEBUG_SERIALISATION
|
||||
|
||||
if flag(debug-parsing)
|
||||
cpp-options: -DDEBUG_PARSING
|
||||
|
||||
if flag(enable-cluster-counting)
|
||||
cpp-options: -DCOUNT_CLUSTERS
|
||||
build-depends: text-icu >= 0.7.1.0
|
||||
|
||||
if os(windows)
|
||||
build-depends: Win32 >= 2.6.1.0 && < 2.15
|
||||
|
||||
-- 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
|
||||
|
||||
-- For libraries that come with GHC, we take the shipped version as default lower bound.
|
||||
build-depends:
|
||||
-- Please keep in alphabetical order!
|
||||
, aeson >= 1.1.2.0 && < 2.3
|
||||
, ansi-terminal >= 0.9 && < 1.2
|
||||
, array >= 0.5.2.0 && < 0.6
|
||||
, async >= 2.2 && < 2.3
|
||||
, base >= 4.12.0.0 && < 4.21
|
||||
, binary >= 0.8.6.0 && < 0.9
|
||||
, blaze-html >= 0.8 && < 0.10
|
||||
, boxes >= 0.1.3 && < 0.2
|
||||
, bytestring >= 0.10.8.2 && < 0.13
|
||||
, case-insensitive >= 1.2.0.4 && < 1.3
|
||||
, containers >= 0.6.0.1 && < 0.8
|
||||
, data-hash >= 0.2.0.0 && < 0.3
|
||||
, deepseq >= 1.4.4.0 && < 1.6
|
||||
, directory >= 1.3.3.0 && < 1.4
|
||||
, dlist >= 0.8 && < 1.1
|
||||
, 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.2.1 && < 1.6
|
||||
, ghc-compact == 0.1.*
|
||||
, gitrev >= 1.3.1 && < 2
|
||||
-- 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.6
|
||||
, haskeline >= 0.7.4.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.4
|
||||
, murmur-hash >= 0.1 && < 0.2
|
||||
, parallel >= 3.2.2.0 && < 3.3
|
||||
, peano >= 0.1.0.1 && < 0.2
|
||||
, pqueue >= 1.4.1.2 && < 1.6
|
||||
, pretty >= 1.1.3.3 && < 1.2
|
||||
, process >= 1.6.3.0 && < 1.7
|
||||
, regex-tdfa >= 1.3.1.0 && < 1.4
|
||||
, split >= 0.2.0.0 && < 0.3
|
||||
, stm >= 2.4.4 && < 2.6
|
||||
, STMonadTrans >= 0.4.3 && < 0.5
|
||||
, strict >= 0.4.0.1 && < 0.6
|
||||
, text >= 1.2.3.1 && < 2.2
|
||||
, time >= 1.9.2 && < 1.15
|
||||
, transformers >= 0.5.5.0 && < 0.7
|
||||
, unordered-containers >= 0.2.9.0 && < 0.3
|
||||
-- unordered-containers < 0.2.9 need base < 4.11
|
||||
, uri-encode >= 1.5.0.4 && < 1.6
|
||||
, vector >= 0.12 && < 0.14
|
||||
, vector-hashtables >= 0.1.1.1 && < 0.2
|
||||
, zlib >= 0.6 && < 0.8
|
||||
|
||||
build-tool-depends:
|
||||
, alex:alex >= 3.2.3 && < 4
|
||||
-- alex-3.2.3 is packaged with Ubuntu 18.04
|
||||
, happy:happy >= 1.19.8 && < 2.1.1 || >= 2.1.2 && < 3
|
||||
-- happy-1.19.8 is packaged with Ubuntu 18.04
|
||||
-- Build failure with happy-2.1.1, issue #7585
|
||||
|
||||
exposed-modules:
|
||||
Agda.Benchmarking
|
||||
Agda.Compiler.Backend
|
||||
Agda.Compiler.Backend.Base
|
||||
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.Output
|
||||
Agda.Interaction.Response
|
||||
Agda.Interaction.Response.Base
|
||||
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.Mimer.Mimer
|
||||
Agda.Mimer.Options
|
||||
Agda.Syntax.Abstract.Name
|
||||
Agda.Syntax.Abstract.Pattern
|
||||
Agda.Syntax.Abstract.PatternSynonyms
|
||||
Agda.Syntax.Abstract.Pretty
|
||||
Agda.Syntax.Abstract.UsedNames
|
||||
Agda.Syntax.Abstract.Views
|
||||
Agda.Syntax.Abstract
|
||||
Agda.Syntax.Builtin
|
||||
Agda.Syntax.Common
|
||||
Agda.Syntax.Common.Aspect
|
||||
Agda.Syntax.Common.KeywordRange
|
||||
Agda.Syntax.Common.Pretty
|
||||
Agda.Syntax.Common.Pretty.ANSI
|
||||
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.Internal.Univ
|
||||
Agda.Syntax.Literal
|
||||
Agda.Syntax.Notation
|
||||
Agda.Syntax.Parser.Alex
|
||||
Agda.Syntax.Parser.Comments
|
||||
Agda.Syntax.Parser.Helpers
|
||||
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.Flat
|
||||
Agda.Syntax.Scope.Monad
|
||||
Agda.Syntax.TopLevelModuleName
|
||||
Agda.Syntax.TopLevelModuleName.Boot
|
||||
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.Coverage.SplitClause
|
||||
Agda.TypeChecking.Coverage.Cubical
|
||||
Agda.TypeChecking.Datatypes
|
||||
Agda.TypeChecking.DeadCode
|
||||
Agda.TypeChecking.DisplayForm
|
||||
Agda.TypeChecking.DropArgs
|
||||
Agda.TypeChecking.DiscrimTree
|
||||
Agda.TypeChecking.DiscrimTree.Types
|
||||
Agda.TypeChecking.Empty
|
||||
Agda.TypeChecking.EtaContract
|
||||
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.Modalities
|
||||
Agda.TypeChecking.Monad.Base
|
||||
Agda.TypeChecking.Monad.Base.Types
|
||||
Agda.TypeChecking.Monad.Base.Warning
|
||||
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.Modality
|
||||
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.Opacity
|
||||
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.Primitive.Cubical.Id
|
||||
Agda.TypeChecking.Primitive.Cubical.Glue
|
||||
Agda.TypeChecking.Primitive.Cubical.Base
|
||||
Agda.TypeChecking.Primitive.Cubical.HCompU
|
||||
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.LHS.Unify.Types
|
||||
Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
|
||||
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.Pretty
|
||||
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.Boolean
|
||||
Agda.Utils.BoolSet
|
||||
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.HashTable
|
||||
Agda.Utils.Haskell.Syntax
|
||||
Agda.Utils.IArray
|
||||
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.ProfileOptions
|
||||
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.Unsafe
|
||||
Agda.Utils.Update
|
||||
Agda.Utils.VarSet
|
||||
Agda.Utils.Warshall
|
||||
Agda.Utils.WithDefault
|
||||
Agda.Utils.Zipper
|
||||
Agda.Version
|
||||
Agda.VersionCommit
|
||||
|
||||
autogen-modules:
|
||||
Paths_Agda
|
||||
|
||||
other-modules:
|
||||
Paths_Agda
|
||||
-- Need not export submodules if parent module reexports them.
|
||||
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
|
||||
|
||||
-- Agda binary
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
executable agda
|
||||
hs-source-dirs: src/main
|
||||
main-is: Main.hs
|
||||
build-depends:
|
||||
, Agda
|
||||
-- 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=-I0
|
||||
|
||||
-- agda-mode executable
|
||||
---------------------------------------------------------------------------
|
||||
|
||||
executable agda-mode
|
||||
hs-source-dirs: src/agda-mode
|
||||
main-is: Main.hs
|
||||
autogen-modules: Paths_Agda
|
||||
other-modules: Paths_Agda
|
||||
build-depends:
|
||||
, base >= 4.12.0.0 && < 4.21
|
||||
, directory >= 1.3.3.0 && < 1.4
|
||||
, filepath >= 1.4.2.1 && < 1.6
|
||||
, process >= 1.6.3.0 && < 1.7
|
||||
default-language: Haskell2010
|
||||
271
Agda.spec
271
Agda.spec
|
|
@ -1,55 +1,64 @@
|
|||
# generated by cabal-rpm-2.1.0 --subpackage
|
||||
# generated by cabal-rpm-2.3.1 --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}
|
||||
%{?haskell_setup}
|
||||
|
||||
%global geniplatemirror geniplate-mirror-0.7.9
|
||||
%global murmurhash murmur-hash-0.1.0.10
|
||||
%global subpkgs %{geniplatemirror} %{murmurhash}
|
||||
#%%bcond clustercounting %%[0%%{?fedora} >= 43]
|
||||
|
||||
%global ListLike ListLike-4.7.8.3
|
||||
%global apnormalize ap-normalize-0.1.0.1
|
||||
%global fmlist fmlist-0.9.4
|
||||
%global genericdata generic-data-1.1.0.2
|
||||
%global murmurhash murmur-hash-0.1.0.11
|
||||
%global nonemptycontainers nonempty-containers-0.3.5.0
|
||||
%global nonemptyvector nonempty-vector-0.2.4
|
||||
%global peano peano-0.1.0.2
|
||||
%global pqueue pqueue-1.5.0.0
|
||||
%global processextras process-extras-0.7.4
|
||||
%global showcombinators show-combinators-0.2.0.0
|
||||
%global vectorhashtables vector-hashtables-0.1.2.1
|
||||
|
||||
%global subpkgs %{apnormalize} %{fmlist} %{ListLike} %{murmurhash} %{nonemptyvector} %{nonemptycontainers} %{peano} %{pqueue} %{processextras} %{showcombinators} %{genericdata} %{vectorhashtables}
|
||||
|
||||
Name: %{pkg_name}
|
||||
Version: 2.6.2.2
|
||||
Version: 2.8.0
|
||||
# can only be reset when all subpkgs bumped
|
||||
Release: 38%{?dist}
|
||||
Release: 57%{?dist}
|
||||
Summary: A dependently typed functional programming language and proof assistant
|
||||
|
||||
License: MIT and BSD-3-Clause
|
||||
Url: https://hackage.haskell.org/package/%{name}
|
||||
License: MIT AND BSD-3-Clause
|
||||
URL: https://hackage.haskell.org/package/Agda
|
||||
# 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
|
||||
Source1: https://hackage.haskell.org/package/%{ListLike}/%{ListLike}.tar.gz
|
||||
Source2: https://hackage.haskell.org/package/%{apnormalize}/%{apnormalize}.tar.gz
|
||||
Source3: https://hackage.haskell.org/package/%{fmlist}/%{fmlist}.tar.gz
|
||||
Source4: https://hackage.haskell.org/package/%{genericdata}/%{genericdata}.tar.gz
|
||||
Source5: https://hackage.haskell.org/package/%{murmurhash}/%{murmurhash}.tar.gz
|
||||
Source6: https://hackage.haskell.org/package/%{nonemptycontainers}/%{nonemptycontainers}.tar.gz
|
||||
Source7: https://hackage.haskell.org/package/%{nonemptyvector}/%{nonemptyvector}.tar.gz
|
||||
Source8: https://hackage.haskell.org/package/%{peano}/%{peano}.tar.gz
|
||||
Source9: https://hackage.haskell.org/package/%{pqueue}/%{pqueue}.tar.gz
|
||||
Source10: https://hackage.haskell.org/package/%{processextras}/%{processextras}.tar.gz
|
||||
Source11: https://hackage.haskell.org/package/%{showcombinators}/%{showcombinators}.tar.gz
|
||||
Source12: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz
|
||||
# End cabal-rpm sources
|
||||
Source10: agda-mode-init.el
|
||||
Source20: 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}
|
||||
# i686:
|
||||
# [410 of 429] Compiling Agda.Compiler.MAlonzo.Compiler
|
||||
# https://bugzilla.redhat.com/show_bug.cgi?id=2244516
|
||||
# also https://gitlab.haskell.org/ghc/ghc/issues/17030 panic for prof
|
||||
ExcludeArch: %{ix86} armv7hl
|
||||
|
||||
# Begin cabal-rpm deps:
|
||||
BuildRequires: dos2unix
|
||||
BuildRequires: ghc-Cabal-devel
|
||||
BuildRequires: ghc-rpm-macros-extra
|
||||
BuildRequires: ghc-Cabal-devel
|
||||
BuildRequires: ghc-STMonadTrans-devel
|
||||
BuildRequires: ghc-aeson-devel
|
||||
BuildRequires: ghc-ansi-terminal-devel
|
||||
BuildRequires: ghc-array-devel
|
||||
BuildRequires: ghc-async-devel
|
||||
BuildRequires: ghc-base-devel
|
||||
|
|
@ -62,34 +71,49 @@ BuildRequires: ghc-containers-devel
|
|||
BuildRequires: ghc-data-hash-devel
|
||||
BuildRequires: ghc-deepseq-devel
|
||||
BuildRequires: ghc-directory-devel
|
||||
BuildRequires: ghc-dlist-devel
|
||||
BuildRequires: ghc-edit-distance-devel
|
||||
BuildRequires: ghc-enummapset-devel
|
||||
BuildRequires: ghc-equivalence-devel
|
||||
BuildRequires: ghc-exceptions-devel
|
||||
BuildRequires: ghc-filelock-devel
|
||||
BuildRequires: ghc-filemanip-devel
|
||||
BuildRequires: ghc-filepath-devel
|
||||
#BuildRequires: ghc-generic-data-devel
|
||||
BuildRequires: ghc-ghc-compact-devel
|
||||
BuildRequires: ghc-gitrev-devel
|
||||
BuildRequires: ghc-hashable-devel
|
||||
BuildRequires: ghc-hashtables-devel
|
||||
BuildRequires: ghc-haskeline-devel
|
||||
BuildRequires: ghc-monad-control-devel
|
||||
BuildRequires: ghc-mtl-devel
|
||||
#BuildRequires: ghc-murmur-hash-devel
|
||||
#BuildRequires: ghc-nonempty-containers-devel
|
||||
BuildRequires: ghc-parallel-devel
|
||||
#BuildRequires: ghc-peano-devel
|
||||
#BuildRequires: ghc-pqueue-devel
|
||||
BuildRequires: ghc-pretty-devel
|
||||
BuildRequires: ghc-process-devel
|
||||
#BuildRequires: ghc-process-extras-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
|
||||
%if %{with clustercounting}
|
||||
BuildRequires: ghc-text-icu-devel
|
||||
%endif
|
||||
BuildRequires: ghc-time-devel
|
||||
BuildRequires: ghc-transformers-devel
|
||||
BuildRequires: ghc-unordered-containers-devel
|
||||
BuildRequires: ghc-uri-encode-devel
|
||||
BuildRequires: ghc-vector-devel
|
||||
#BuildRequires: ghc-vector-hashtables-devel
|
||||
BuildRequires: ghc-zlib-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-STMonadTrans-prof
|
||||
BuildRequires: ghc-aeson-prof
|
||||
BuildRequires: ghc-ansi-terminal-prof
|
||||
BuildRequires: ghc-array-prof
|
||||
BuildRequires: ghc-async-prof
|
||||
BuildRequires: ghc-base-prof
|
||||
|
|
@ -102,61 +126,118 @@ BuildRequires: ghc-containers-prof
|
|||
BuildRequires: ghc-data-hash-prof
|
||||
BuildRequires: ghc-deepseq-prof
|
||||
BuildRequires: ghc-directory-prof
|
||||
BuildRequires: ghc-dlist-prof
|
||||
BuildRequires: ghc-edit-distance-prof
|
||||
BuildRequires: ghc-enummapset-prof
|
||||
BuildRequires: ghc-equivalence-prof
|
||||
BuildRequires: ghc-exceptions-prof
|
||||
BuildRequires: ghc-filelock-prof
|
||||
BuildRequires: ghc-filemanip-prof
|
||||
BuildRequires: ghc-filepath-prof
|
||||
#BuildRequires: ghc-generic-data-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-nonempty-containers-prof
|
||||
BuildRequires: ghc-parallel-prof
|
||||
#BuildRequires: ghc-peano-prof
|
||||
#BuildRequires: ghc-pqueue-prof
|
||||
BuildRequires: ghc-pretty-prof
|
||||
BuildRequires: ghc-process-prof
|
||||
#BuildRequires: ghc-process-extras-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
|
||||
%if %{with clustercounting}
|
||||
BuildRequires: ghc-text-icu-prof
|
||||
%endif
|
||||
BuildRequires: ghc-time-prof
|
||||
BuildRequires: ghc-transformers-prof
|
||||
BuildRequires: ghc-unordered-containers-prof
|
||||
BuildRequires: ghc-uri-encode-prof
|
||||
BuildRequires: ghc-vector-prof
|
||||
#BuildRequires: ghc-vector-hashtables-prof
|
||||
BuildRequires: ghc-zlib-prof
|
||||
%endif
|
||||
BuildRequires: alex
|
||||
BuildRequires: happy
|
||||
Provides: agda = %{version}-%{release}
|
||||
Requires: %{name}-common = %{version}-%{release}
|
||||
# for missing dep 'ListLike':
|
||||
BuildRequires: ghc-utf8-string-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-utf8-string-prof
|
||||
%endif
|
||||
# for missing dep 'generic-data':
|
||||
BuildRequires: ghc-base-orphans-devel
|
||||
BuildRequires: ghc-ghc-boot-th-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-base-orphans-prof
|
||||
BuildRequires: ghc-ghc-boot-th-prof
|
||||
%endif
|
||||
# for missing dep 'nonempty-containers':
|
||||
BuildRequires: ghc-comonad-devel
|
||||
BuildRequires: ghc-invariant-devel
|
||||
BuildRequires: ghc-semigroupoids-devel
|
||||
BuildRequires: ghc-these-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-comonad-prof
|
||||
BuildRequires: ghc-invariant-prof
|
||||
BuildRequires: ghc-semigroupoids-prof
|
||||
BuildRequires: ghc-these-prof
|
||||
%endif
|
||||
# for missing dep 'nonempty-vector':
|
||||
BuildRequires: ghc-primitive-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-primitive-prof
|
||||
%endif
|
||||
# for missing dep 'pqueue':
|
||||
BuildRequires: ghc-indexed-traversable-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-indexed-traversable-prof
|
||||
%endif
|
||||
# for missing dep 'process-extras':
|
||||
BuildRequires: ghc-data-default-devel
|
||||
BuildRequires: ghc-generic-deriving-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-data-default-prof
|
||||
BuildRequires: ghc-generic-deriving-prof
|
||||
%endif
|
||||
# for missing dep 'vector-hashtables':
|
||||
BuildRequires: ghc-primitive-devel
|
||||
%if %{with ghc_prof}
|
||||
BuildRequires: ghc-primitive-prof
|
||||
%endif
|
||||
# End cabal-rpm deps
|
||||
BuildRequires: emacs(bin)
|
||||
|
||||
# introduced for F23
|
||||
Obsoletes: emacs-agda-el < 2.4.2.2-5
|
||||
Provides: emacs-agda = %{version}-%{release}
|
||||
|
||||
%description
|
||||
Agda is a dependently typed functional programming language: it has
|
||||
Agda is a dependently typed functional programming language: It has
|
||||
inductive families, which are similar to Haskell's GADTs, but they can
|
||||
be indexed by values and not just types. It also has parameterized
|
||||
modules, mixfix operators, Unicode characters, and an interactive
|
||||
Emacs interface (the type checker can assist in the development of your code).
|
||||
|
||||
Agda is also a proof assistant: It is an interactive system for writing and
|
||||
checking proofs. Agda is based on intuitionistic type theory,
|
||||
a foundational system for constructive mathematics developed by
|
||||
the Swedish logician Per Martin-Löf. It has many similarities with other
|
||||
proof assistants based on dependent types, such as Coq, Epigram and NuPRL.
|
||||
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 Rocq (formerly known as Coq), Idris, Lean and NuPRL.
|
||||
|
||||
This package includes both a command-line program (agda) and an Emacs mode.
|
||||
|
||||
|
||||
%package common
|
||||
Summary: %{name} common files
|
||||
License: MIT and BSD-3-Clause and BSD-2-Clause
|
||||
License: MIT AND BSD-3-Clause AND BSD-2-Clause
|
||||
BuildArch: noarch
|
||||
|
||||
%description common
|
||||
|
|
@ -209,8 +290,18 @@ This package provides the Haskell %{name} profiling library.
|
|||
%global main_version %{version}
|
||||
|
||||
%if %{defined ghclibdir}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{geniplatemirror}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{ListLike}
|
||||
%ghc_lib_subpackage -l MIT %{apnormalize}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{fmlist}
|
||||
%ghc_lib_subpackage -l MIT %{genericdata}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{murmurhash}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{nonemptycontainers}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{nonemptyvector}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{peano}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{pqueue}
|
||||
%ghc_lib_subpackage -l MIT %{processextras}
|
||||
%ghc_lib_subpackage -l MIT %{showcombinators}
|
||||
%ghc_lib_subpackage -l BSD-3-Clause %{vectorhashtables}
|
||||
%endif
|
||||
|
||||
%global version %{main_version}
|
||||
|
|
@ -218,9 +309,20 @@ This package provides the Haskell %{name} profiling library.
|
|||
|
||||
%prep
|
||||
# Begin cabal-rpm setup:
|
||||
%setup -q -a1 -a2
|
||||
dos2unix -k -n %{SOURCE3} %{name}.cabal
|
||||
%setup -q -a1 -a2 -a3 -a4 -a5 -a6 -a7 -a8 -a9 -a10 -a11 -a12
|
||||
# End cabal-rpm setup
|
||||
%if %{with clustercounting}
|
||||
#cabal-tweak-flag enable-cluster-counting True
|
||||
%endif
|
||||
(
|
||||
cd %{pqueue}
|
||||
cabal-tweak-dep-ver base '< 4.19' '< 4.20'
|
||||
cabal-tweak-dep-ver deepseq '< 1.5' '< 1.6'
|
||||
)
|
||||
(
|
||||
cd %{showcombinators}
|
||||
cabal-tweak-dep-ver base '< 4.14' '< 4.20'
|
||||
)
|
||||
|
||||
# check the Agda version in the emacs mode
|
||||
if ! grep -q \"%{version}\" src/data/emacs-mode/agda2-mode.el; then
|
||||
|
|
@ -245,10 +347,6 @@ done
|
|||
|
||||
# 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
|
||||
|
||||
|
|
@ -277,7 +375,7 @@ for i in src/data/emacs-mode/*; do
|
|||
done
|
||||
|
||||
mkdir -p %{buildroot}%{_emacs_sitestartdir}
|
||||
install -p -m 0644 %SOURCE10 %{buildroot}%{_emacs_sitestartdir}
|
||||
install -p -m 0644 %SOURCE20 %{buildroot}%{_emacs_sitestartdir}
|
||||
|
||||
rm %{buildroot}%{_bindir}/agda-mode
|
||||
rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode
|
||||
|
|
@ -319,6 +417,73 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode
|
|||
|
||||
|
||||
%changelog
|
||||
* Fri Jan 16 2026 Fedora Release Engineering <releng@fedoraproject.org> - 2.8.0-57
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
|
||||
|
||||
* Wed Jul 23 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.8.0-56
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
|
||||
|
||||
* Sun Jul 06 2025 Jens Petersen <petersen@redhat.com> - 2.8.0-55
|
||||
- https://hackage.haskell.org/package/Agda-2.8.0/changelog
|
||||
- many new deps
|
||||
|
||||
* Sun Mar 30 2025 Jens Petersen <petersen@redhat.com> - 2.7.0.1-54
|
||||
- https://hackage.haskell.org/package/Agda-2.7.0.1/changelog
|
||||
- add pqueue
|
||||
|
||||
* Mon Jan 20 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.3-53
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
|
||||
|
||||
* Thu Jan 16 2025 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.3-52
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
|
||||
|
||||
* Mon Dec 09 2024 Pete Walter <pwalter@fedoraproject.org> - 2.6.4.3-51
|
||||
- Rebuild for ICU 76
|
||||
|
||||
* Sun Jul 21 2024 Jens Petersen <petersen@redhat.com> - 2.6.4.3-50
|
||||
- update vector-hashtables to 0.1.2.0
|
||||
|
||||
* Wed Jul 17 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.3-49
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
|
||||
|
||||
* Sat May 18 2024 Jens Petersen <petersen@redhat.com> - 2.6.4.3-48
|
||||
- update to 2.6.4.3
|
||||
- https://hackage.haskell.org/package/Agda-2.6.4.2/changelog
|
||||
- https://hackage.haskell.org/package/Agda-2.6.4.3/changelog
|
||||
|
||||
* Tue Feb 20 2024 Jens Petersen <petersen@redhat.com> - 2.6.4.1-47
|
||||
- rawhide: enable-cluster-counting with text-icu
|
||||
- update vector-hashtables to 0.1.1.4
|
||||
|
||||
* Mon Jan 22 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.1-46
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
|
||||
|
||||
* Fri Jan 19 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.1-45
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
|
||||
|
||||
* Thu Jan 18 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4.1-44
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
|
||||
|
||||
* Thu Dec 7 2023 Jens Petersen <petersen@redhat.com> - 2.6.4.1-43
|
||||
- https://hackage.haskell.org/package/Agda-2.6.4.1/changelog
|
||||
- update peano to 0.1.0.2
|
||||
|
||||
* Tue Oct 17 2023 Jens Petersen <petersen@redhat.com> - 2.6.4-42
|
||||
- F40: enable optimise-heavily flag
|
||||
|
||||
* Mon Oct 09 2023 Jens Petersen <petersen@redhat.com> - 2.6.4-41
|
||||
- update to 2.6.4
|
||||
- https://hackage.haskell.org/package/Agda-2.6.4/changelog
|
||||
|
||||
* Sat Jul 29 2023 Jens Petersen <petersen@redhat.com> - 2.6.3-40
|
||||
- https://hackage.haskell.org/package/Agda-2.6.3/changelog
|
||||
|
||||
* Wed Jul 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2.2-39
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
|
||||
|
||||
* Tue Jul 11 2023 Jens Petersen <petersen@redhat.com>
|
||||
- drop geniplate-mirror: not needed since 2.6.2
|
||||
|
||||
* 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
|
||||
|
|
|
|||
16
sources
16
sources
|
|
@ -1,3 +1,13 @@
|
|||
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
|
||||
SHA512 (Agda-2.8.0.tar.gz) = 53ae24c9759c271251c3c487a27b8600ba55d39391a186684731a1495a744c18ccd4d3deb5e5231f72abb1be95fa8dac2dac8f257612bc32c6f51d2071ae8273
|
||||
SHA512 (ListLike-4.7.8.3.tar.gz) = 99f3e8c2a72161a51710c63a38c381d5c109872b039bafdf97d8d029cca13ed7ad7125cba365609336ed6013bfb0b06781325ed78615ca632485e030ee924eef
|
||||
SHA512 (ap-normalize-0.1.0.1.tar.gz) = 8566f61303238c8e8d27badf851403a8e2419b06149c25b5236ee2de17f0733eaaf912af2edd9c72dfed5cffd2169e07d2efd584e2bf3a903c1b21cca20b1d5f
|
||||
SHA512 (fmlist-0.9.4.tar.gz) = 68b36503cd895bff5f25f2d24422972537b5ba68439714de257441c14194656b0b84137fa9c45235cdb9291e8a2d132e66e9a1d45f66f91142eef65f07d8c5dc
|
||||
SHA512 (generic-data-1.1.0.2.tar.gz) = 4140892965083032cc2fbe361d39a5bd59b94802e23a2ab202a3d86e212e17c9fbfc2cd3958dda3666a5ac2324538bf08ee45d39702a0c7be66a77665b0d356a
|
||||
SHA512 (murmur-hash-0.1.0.11.tar.gz) = 9ff9ac2c749cc590bcb195f873d6319abaaea1e728423b95fa281a9b21da6a1257e08b485915bb59d540e8fab2ad8bdcfe924eea4e93ae3d75dc9ac3bba7aba0
|
||||
SHA512 (nonempty-containers-0.3.5.0.tar.gz) = caa977b0028d10d0713fa4716a0498ff56a5beee3513e8d6331d6cccdcd3f12fc3371fa69d67283e80f79b8fc2b90228260791200b3f7149a26c4311daa790b9
|
||||
SHA512 (nonempty-vector-0.2.4.tar.gz) = 9c10794b12a503092bb5d3a53bfdedf99303edf697415b04dc94488e766126fc97de3a99564e84424606b9d813509600442e7fcbe2aa8552ab33ad2a43bc066a
|
||||
SHA512 (peano-0.1.0.2.tar.gz) = 1fbdb2d82674da7c4350797f2557c58b5302396b68f3debaae0c255e1c22d2c766b1da6c38e9b5ba673e823e5511b7bf9a3107bcabcbd375a325c736c9e9908d
|
||||
SHA512 (pqueue-1.5.0.0.tar.gz) = 9d15ecb0b877524a3b38a37c5c1029e4c20330f303f90dce6fee25f416ec6c8f019c811cef451e5b7aa20b4bd5265c1b186feffb4a7fc51f3d2f3fe68367de0b
|
||||
SHA512 (process-extras-0.7.4.tar.gz) = 4747b4bd920796b7b4ddf32d0e72a3af556c9db66c828b725ac7a7467442dad2b0dc85aa66e03d7a8c5afdb02658611e64d390b6c71219b380a986e245495536
|
||||
SHA512 (show-combinators-0.2.0.0.tar.gz) = 6d9bd0b788c8c4733e3e48ebd8f76a01caa2e6fecf8942f5d00de4e46231f972d4bf23435d0a432c2795fa30b11717c6ebc3f55709138d7a3c15ead4c1779369
|
||||
SHA512 (vector-hashtables-0.1.2.1.tar.gz) = 247ee368982dcac9d4b66df72df4df16a90b61c6bdad3f2ffa2c07c7e1f5638f6579c1baae84e92ab22fb44a8eaffed1914adb4419f9fc5426bdb9eb7b67194f
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue