diff --git a/.gitignore b/.gitignore index c274d73..2e987c7 100644 --- a/.gitignore +++ b/.gitignore @@ -38,16 +38,3 @@ /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 diff --git a/Agda-2.7.0.1.cabal b/Agda-2.7.0.1.cabal deleted file mode 100644 index 0dee66a..0000000 --- a/Agda-2.7.0.1.cabal +++ /dev/null @@ -1,896 +0,0 @@ -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 diff --git a/Agda.spec b/Agda.spec index 82bdb69..3911a6b 100644 --- a/Agda.spec +++ b/Agda.spec @@ -1,51 +1,33 @@ -# generated by cabal-rpm-2.3.1 --subpackage +# generated by cabal-rpm-2.2.1 --subpackage # https://docs.fedoraproject.org/en-US/packaging-guidelines/Haskell/ %global pkg_name Agda %global pkgver %{pkg_name}-%{version} %{?haskell_setup} -#%%bcond clustercounting %%[0%%{?fedora} >= 43] +%bcond clustercounting %[0%{?fedora} >= 41] -%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 murmurhash murmur-hash-0.1.0.10 %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 vectorhashtables vector-hashtables-0.1.2.0 -%global subpkgs %{apnormalize} %{fmlist} %{ListLike} %{murmurhash} %{nonemptyvector} %{nonemptycontainers} %{peano} %{pqueue} %{processextras} %{showcombinators} %{genericdata} %{vectorhashtables} +%global subpkgs %{murmurhash} %{peano} %{vectorhashtables} Name: %{pkg_name} -Version: 2.8.0 +Version: 2.6.4.3 # can only be reset when all subpkgs bumped -Release: 57%{?dist} +Release: 50%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause -URL: https://hackage.haskell.org/package/Agda +Url: https://hackage.haskell.org/package/%{name} # Begin cabal-rpm sources: Source0: https://hackage.haskell.org/package/%{pkgver}/%{pkgver}.tar.gz -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 +Source1: https://hackage.haskell.org/package/%{murmurhash}/%{murmurhash}.tar.gz +Source2: https://hackage.haskell.org/package/%{peano}/%{peano}.tar.gz +Source3: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz # End cabal-rpm sources -Source20: agda-mode-init.el +Source10: agda-mode-init.el # i686: # [410 of 429] Compiling Agda.Compiler.MAlonzo.Compiler @@ -54,8 +36,8 @@ Source20: agda-mode-init.el ExcludeArch: %{ix86} armv7hl # Begin cabal-rpm deps: -BuildRequires: ghc-rpm-macros-extra BuildRequires: ghc-Cabal-devel +BuildRequires: ghc-rpm-macros-extra BuildRequires: ghc-STMonadTrans-devel BuildRequires: ghc-aeson-devel BuildRequires: ghc-ansi-terminal-devel @@ -73,13 +55,9 @@ 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 @@ -87,23 +65,20 @@ 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-time-compat-devel BuildRequires: ghc-transformers-devel BuildRequires: ghc-unordered-containers-devel BuildRequires: ghc-uri-encode-devel @@ -128,13 +103,9 @@ 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 @@ -142,23 +113,20 @@ 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-time-compat-prof BuildRequires: ghc-transformers-prof BuildRequires: ghc-unordered-containers-prof BuildRequires: ghc-uri-encode-prof @@ -170,46 +138,6 @@ 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} @@ -227,10 +155,10 @@ 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 Rocq (formerly known as Coq), Idris, Lean 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 Coq, Idris, Lean and NuPRL. This package includes both a command-line program (agda) and an Emacs mode. @@ -290,17 +218,8 @@ This package provides the Haskell %{name} profiling library. %global main_version %{version} %if %{defined ghclibdir} -%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 @@ -309,20 +228,14 @@ This package provides the Haskell %{name} profiling library. %prep # Begin cabal-rpm setup: -%setup -q -a1 -a2 -a3 -a4 -a5 -a6 -a7 -a8 -a9 -a10 -a11 -a12 +%setup -q -a1 -a2 -a3 # End cabal-rpm setup -%if %{with clustercounting} -#cabal-tweak-flag enable-cluster-counting True +%if 0%{?fedora} >= 40 +cabal-tweak-flag optimise-heavily True +%endif +%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 @@ -375,7 +288,7 @@ for i in src/data/emacs-mode/*; do done mkdir -p %{buildroot}%{_emacs_sitestartdir} -install -p -m 0644 %SOURCE20 %{buildroot}%{_emacs_sitestartdir} +install -p -m 0644 %SOURCE10 %{buildroot}%{_emacs_sitestartdir} rm %{buildroot}%{_bindir}/agda-mode rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode @@ -417,29 +330,6 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog -* Fri Jan 16 2026 Fedora Release Engineering - 2.8.0-57 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild - -* Wed Jul 23 2025 Fedora Release Engineering - 2.8.0-56 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild - -* Sun Jul 06 2025 Jens Petersen - 2.8.0-55 -- https://hackage.haskell.org/package/Agda-2.8.0/changelog -- many new deps - -* Sun Mar 30 2025 Jens Petersen - 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 - 2.6.4.3-53 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild - -* Thu Jan 16 2025 Fedora Release Engineering - 2.6.4.3-52 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild - -* Mon Dec 09 2024 Pete Walter - 2.6.4.3-51 -- Rebuild for ICU 76 - * Sun Jul 21 2024 Jens Petersen - 2.6.4.3-50 - update vector-hashtables to 0.1.2.0 diff --git a/sources b/sources index f12734a..4668844 100644 --- a/sources +++ b/sources @@ -1,13 +1,4 @@ -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 (Agda-2.6.4.3.tar.gz) = d6246d1550b535a3f299cbbf8e38b5b44ee469cce089bbec1d6a62a2518bca2d2900a456d6df10a179d7064982ccdc5f38a1ffc53e327c0c4c060c09f8280488 +SHA512 (murmur-hash-0.1.0.10.tar.gz) = d6d28fcd738de98ce4fb6c7e997b32bb15eef9efe53642cefffd2cfeccd1b56f634adbcadeec9fb94c69d1df9e675f7daf368c62806ef819dc242df947ddf70b 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 +SHA512 (vector-hashtables-0.1.2.0.tar.gz) = 46aa3c83936304b2a3df73f9e705ca2872a0c72e79e47156d9cc397797adfff56eec467dd60b5082e7a8c181ee8f69c51aa796fed5532720ac619e344cdb2294