From feccefbb571bb85173935d5fa41043fcde03aac3 Mon Sep 17 00:00:00 2001 From: Pete Walter Date: Mon, 9 Dec 2024 15:48:52 +0000 Subject: [PATCH 1/9] Rebuild for ICU 76 --- Agda.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Agda.spec b/Agda.spec index 3911a6b..b004147 100644 --- a/Agda.spec +++ b/Agda.spec @@ -16,7 +16,7 @@ Name: %{pkg_name} Version: 2.6.4.3 # can only be reset when all subpkgs bumped -Release: 50%{?dist} +Release: 51%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause @@ -330,6 +330,9 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 From b9f8a1efa36726f5d229c1fb5bde7466ab232699 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Thu, 16 Jan 2025 08:23:35 +0000 Subject: [PATCH 2/9] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild --- Agda.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Agda.spec b/Agda.spec index b004147..3438850 100644 --- a/Agda.spec +++ b/Agda.spec @@ -16,7 +16,7 @@ Name: %{pkg_name} Version: 2.6.4.3 # can only be reset when all subpkgs bumped -Release: 51%{?dist} +Release: 52%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause @@ -330,6 +330,9 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 From d6d8fa2900aa11a69b355eb1583f1e45efed7977 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Mon, 20 Jan 2025 07:19:53 +0000 Subject: [PATCH 3/9] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild --- Agda.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Agda.spec b/Agda.spec index 3438850..feb54d9 100644 --- a/Agda.spec +++ b/Agda.spec @@ -16,7 +16,7 @@ Name: %{pkg_name} Version: 2.6.4.3 # can only be reset when all subpkgs bumped -Release: 52%{?dist} +Release: 53%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause @@ -330,6 +330,9 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 From 1b9700d5166ce86ab8d6eb06734e10ab9ac0466a Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Fri, 31 Jan 2025 12:24:33 +0800 Subject: [PATCH 4/9] update to 2.7.0.1; add pqueue; re-disable optimise-heavily and enable-cluster-counting in case it triggers module recompilation --- .gitignore | 3 +++ Agda.spec | 45 +++++++++++++++++++++++++++++++-------------- sources | 5 +++-- 3 files changed, 37 insertions(+), 16 deletions(-) diff --git a/.gitignore b/.gitignore index 2e987c7..725f241 100644 --- a/.gitignore +++ b/.gitignore @@ -38,3 +38,6 @@ /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 diff --git a/Agda.spec b/Agda.spec index feb54d9..9bfed77 100644 --- a/Agda.spec +++ b/Agda.spec @@ -1,31 +1,33 @@ -# generated by cabal-rpm-2.2.1 --subpackage +# generated by cabal-rpm-2.2.2 --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} >= 41] +#%%bcond clustercounting %%[0%%{?fedora} >= 43] -%global murmurhash murmur-hash-0.1.0.10 +%global murmurhash murmur-hash-0.1.0.11 %global peano peano-0.1.0.2 +%global pqueue pqueue-1.5.0.0 %global vectorhashtables vector-hashtables-0.1.2.0 -%global subpkgs %{murmurhash} %{peano} %{vectorhashtables} +%global subpkgs %{murmurhash} %{peano} %{pqueue} %{vectorhashtables} Name: %{pkg_name} -Version: 2.6.4.3 +Version: 2.7.0.1 # can only be reset when all subpkgs bumped -Release: 53%{?dist} +Release: 54%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause -Url: https://hackage.haskell.org/package/%{name} +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/%{murmurhash}/%{murmurhash}.tar.gz Source2: https://hackage.haskell.org/package/%{peano}/%{peano}.tar.gz -Source3: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz +Source3: https://hackage.haskell.org/package/%{pqueue}/%{pqueue}.tar.gz +Source4: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz # End cabal-rpm sources Source10: agda-mode-init.el @@ -67,6 +69,7 @@ BuildRequires: ghc-mtl-devel #BuildRequires: ghc-murmur-hash-devel BuildRequires: ghc-parallel-devel #BuildRequires: ghc-peano-devel +#BuildRequires: ghc-pqueue-devel BuildRequires: ghc-pretty-devel BuildRequires: ghc-process-devel BuildRequires: ghc-regex-tdfa-devel @@ -78,7 +81,6 @@ BuildRequires: ghc-text-devel 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 @@ -115,6 +117,7 @@ BuildRequires: ghc-mtl-prof #BuildRequires: ghc-murmur-hash-prof BuildRequires: ghc-parallel-prof #BuildRequires: ghc-peano-prof +#BuildRequires: ghc-pqueue-prof BuildRequires: ghc-pretty-prof BuildRequires: ghc-process-prof BuildRequires: ghc-regex-tdfa-prof @@ -126,7 +129,6 @@ BuildRequires: ghc-text-prof 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 @@ -138,6 +140,11 @@ BuildRequires: alex BuildRequires: happy Provides: agda = %{version}-%{release} Requires: %{name}-common = %{version}-%{release} +# for missing dep 'pqueue': +BuildRequires: ghc-indexed-traversable-devel +%if %{with ghc_prof} +BuildRequires: ghc-indexed-traversable-prof +%endif # for missing dep 'vector-hashtables': BuildRequires: ghc-primitive-devel %if %{with ghc_prof} @@ -220,6 +227,7 @@ This package provides the Haskell %{name} profiling library. %if %{defined ghclibdir} %ghc_lib_subpackage -l BSD-3-Clause %{murmurhash} %ghc_lib_subpackage -l BSD-3-Clause %{peano} +%ghc_lib_subpackage -l BSD-3-Clause %{pqueue} %ghc_lib_subpackage -l BSD-3-Clause %{vectorhashtables} %endif @@ -228,14 +236,19 @@ This package provides the Haskell %{name} profiling library. %prep # Begin cabal-rpm setup: -%setup -q -a1 -a2 -a3 +%setup -q -a1 -a2 -a3 -a4 # End cabal-rpm setup -%if 0%{?fedora} >= 40 -cabal-tweak-flag optimise-heavily True +%if %{defined fedora} +#cabal-tweak-flag optimise-heavily True %endif %if %{with clustercounting} -cabal-tweak-flag enable-cluster-counting True +#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' +) # check the Agda version in the emacs mode if ! grep -q \"%{version}\" src/data/emacs-mode/agda2-mode.el; then @@ -330,6 +343,10 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 diff --git a/sources b/sources index 4668844..e6a6625 100644 --- a/sources +++ b/sources @@ -1,4 +1,5 @@ -SHA512 (Agda-2.6.4.3.tar.gz) = d6246d1550b535a3f299cbbf8e38b5b44ee469cce089bbec1d6a62a2518bca2d2900a456d6df10a179d7064982ccdc5f38a1ffc53e327c0c4c060c09f8280488 -SHA512 (murmur-hash-0.1.0.10.tar.gz) = d6d28fcd738de98ce4fb6c7e997b32bb15eef9efe53642cefffd2cfeccd1b56f634adbcadeec9fb94c69d1df9e675f7daf368c62806ef819dc242df947ddf70b +SHA512 (Agda-2.7.0.1.tar.gz) = ebe4aca950c045726aca1c96364a1b83c8447442b0fccd3fddcd7a8829161e6e6e4827e292efffb57c69f02664e59322e65d8c22a7cab64a4feffb187fedc28f +SHA512 (murmur-hash-0.1.0.11.tar.gz) = 9ff9ac2c749cc590bcb195f873d6319abaaea1e728423b95fa281a9b21da6a1257e08b485915bb59d540e8fab2ad8bdcfe924eea4e93ae3d75dc9ac3bba7aba0 SHA512 (peano-0.1.0.2.tar.gz) = 1fbdb2d82674da7c4350797f2557c58b5302396b68f3debaae0c255e1c22d2c766b1da6c38e9b5ba673e823e5511b7bf9a3107bcabcbd375a325c736c9e9908d +SHA512 (pqueue-1.5.0.0.tar.gz) = 9d15ecb0b877524a3b38a37c5c1029e4c20330f303f90dce6fee25f416ec6c8f019c811cef451e5b7aa20b4bd5265c1b186feffb4a7fc51f3d2f3fe68367de0b SHA512 (vector-hashtables-0.1.2.0.tar.gz) = 46aa3c83936304b2a3df73f9e705ca2872a0c72e79e47156d9cc397797adfff56eec467dd60b5082e7a8c181ee8f69c51aa796fed5532720ac619e344cdb2294 From 6bdbc993061989ae9a6f0e16e4d083ef6de8ac28 Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Sat, 1 Feb 2025 16:23:48 +0800 Subject: [PATCH 5/9] add revision --- Agda-2.7.0.1.cabal | 896 +++++++++++++++++++++++++++++++++++++++++++++ Agda.spec | 3 + 2 files changed, 899 insertions(+) create mode 100644 Agda-2.7.0.1.cabal diff --git a/Agda-2.7.0.1.cabal b/Agda-2.7.0.1.cabal new file mode 100644 index 0000000..0dee66a --- /dev/null +++ b/Agda-2.7.0.1.cabal @@ -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 diff --git a/Agda.spec b/Agda.spec index 9bfed77..e8119b9 100644 --- a/Agda.spec +++ b/Agda.spec @@ -28,6 +28,7 @@ Source1: https://hackage.haskell.org/package/%{murmurhash}/%{murmurhash}. Source2: https://hackage.haskell.org/package/%{peano}/%{peano}.tar.gz Source3: https://hackage.haskell.org/package/%{pqueue}/%{pqueue}.tar.gz Source4: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz +Source5: https://hackage.haskell.org/package/%{pkgver}/%{name}.cabal#/%{pkgver}.cabal # End cabal-rpm sources Source10: agda-mode-init.el @@ -38,6 +39,7 @@ Source10: agda-mode-init.el ExcludeArch: %{ix86} armv7hl # Begin cabal-rpm deps: +BuildRequires: dos2unix BuildRequires: ghc-Cabal-devel BuildRequires: ghc-rpm-macros-extra BuildRequires: ghc-STMonadTrans-devel @@ -237,6 +239,7 @@ This package provides the Haskell %{name} profiling library. %prep # Begin cabal-rpm setup: %setup -q -a1 -a2 -a3 -a4 +dos2unix -k -n %{SOURCE5} %{name}.cabal # End cabal-rpm setup %if %{defined fedora} #cabal-tweak-flag optimise-heavily True From 396e77c1f7fd5b355ff016bd828f3cff4441a4bb Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Sun, 23 Feb 2025 20:39:55 +0800 Subject: [PATCH 6/9] cabal-rpm-2.3.0 --- Agda.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Agda.spec b/Agda.spec index e8119b9..c9a4873 100644 --- a/Agda.spec +++ b/Agda.spec @@ -1,4 +1,4 @@ -# generated by cabal-rpm-2.2.2 --subpackage +# generated by cabal-rpm-2.3.0 --subpackage # https://docs.fedoraproject.org/en-US/packaging-guidelines/Haskell/ %global pkg_name Agda @@ -21,7 +21,7 @@ Release: 54%{?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/Agda # Begin cabal-rpm sources: Source0: https://hackage.haskell.org/package/%{pkgver}/%{pkgver}.tar.gz Source1: https://hackage.haskell.org/package/%{murmurhash}/%{murmurhash}.tar.gz From d3a2f2a2fb57ae30f71e9c32b48abee1ecaad955 Mon Sep 17 00:00:00 2001 From: Jens Petersen Date: Tue, 22 Jul 2025 22:11:37 +0800 Subject: [PATCH 7/9] https://hackage.haskell.org/package/Agda-2.8.0/changelog many new deps --- .gitignore | 10 +++++ Agda.spec | 121 +++++++++++++++++++++++++++++++++++++++++++---------- sources | 12 +++++- 3 files changed, 118 insertions(+), 25 deletions(-) diff --git a/.gitignore b/.gitignore index 725f241..c274d73 100644 --- a/.gitignore +++ b/.gitignore @@ -41,3 +41,13 @@ /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.spec b/Agda.spec index c9a4873..c4fe758 100644 --- a/Agda.spec +++ b/Agda.spec @@ -1,4 +1,4 @@ -# generated by cabal-rpm-2.3.0 --subpackage +# generated by cabal-rpm-2.3.1 --subpackage # https://docs.fedoraproject.org/en-US/packaging-guidelines/Haskell/ %global pkg_name Agda @@ -7,30 +7,45 @@ #%%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 vectorhashtables vector-hashtables-0.1.2.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 %{murmurhash} %{peano} %{pqueue} %{vectorhashtables} +%global subpkgs %{apnormalize} %{fmlist} %{ListLike} %{murmurhash} %{nonemptyvector} %{nonemptycontainers} %{peano} %{pqueue} %{processextras} %{showcombinators} %{genericdata} %{vectorhashtables} Name: %{pkg_name} -Version: 2.7.0.1 +Version: 2.8.0 # can only be reset when all subpkgs bumped -Release: 54%{?dist} +Release: 55%{?dist} Summary: A dependently typed functional programming language and proof assistant 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/%{murmurhash}/%{murmurhash}.tar.gz -Source2: https://hackage.haskell.org/package/%{peano}/%{peano}.tar.gz -Source3: https://hackage.haskell.org/package/%{pqueue}/%{pqueue}.tar.gz -Source4: https://hackage.haskell.org/package/%{vectorhashtables}/%{vectorhashtables}.tar.gz -Source5: 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 # i686: # [410 of 429] Compiling Agda.Compiler.MAlonzo.Compiler @@ -39,9 +54,8 @@ Source10: agda-mode-init.el 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 @@ -59,9 +73,13 @@ 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 @@ -69,15 +87,18 @@ 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 @@ -107,9 +128,13 @@ 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 @@ -117,15 +142,18 @@ 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 @@ -142,11 +170,46 @@ 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} @@ -164,10 +227,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 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 Rocq (formerly known as Coq), Idris, Lean and NuPRL. This package includes both a command-line program (agda) and an Emacs mode. @@ -227,9 +290,17 @@ 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 @@ -238,12 +309,8 @@ This package provides the Haskell %{name} profiling library. %prep # Begin cabal-rpm setup: -%setup -q -a1 -a2 -a3 -a4 -dos2unix -k -n %{SOURCE5} %{name}.cabal +%setup -q -a1 -a2 -a3 -a4 -a5 -a6 -a7 -a8 -a9 -a10 -a11 -a12 # End cabal-rpm setup -%if %{defined fedora} -#cabal-tweak-flag optimise-heavily True -%endif %if %{with clustercounting} #cabal-tweak-flag enable-cluster-counting True %endif @@ -252,6 +319,10 @@ dos2unix -k -n %{SOURCE5} %{name}.cabal 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 @@ -304,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 @@ -346,6 +417,10 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 diff --git a/sources b/sources index e6a6625..f12734a 100644 --- a/sources +++ b/sources @@ -1,5 +1,13 @@ -SHA512 (Agda-2.7.0.1.tar.gz) = ebe4aca950c045726aca1c96364a1b83c8447442b0fccd3fddcd7a8829161e6e6e4827e292efffb57c69f02664e59322e65d8c22a7cab64a4feffb187fedc28f +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 (vector-hashtables-0.1.2.0.tar.gz) = 46aa3c83936304b2a3df73f9e705ca2872a0c72e79e47156d9cc397797adfff56eec467dd60b5082e7a8c181ee8f69c51aa796fed5532720ac619e344cdb2294 +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 From 4a50bc87bbe2c69235006950ef1845029fa70a2a Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Wed, 23 Jul 2025 15:41:04 +0000 Subject: [PATCH 8/9] Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild --- Agda.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Agda.spec b/Agda.spec index c4fe758..0fd6c04 100644 --- a/Agda.spec +++ b/Agda.spec @@ -25,7 +25,7 @@ Name: %{pkg_name} Version: 2.8.0 # can only be reset when all subpkgs bumped -Release: 55%{?dist} +Release: 56%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause @@ -417,6 +417,9 @@ rm -r %{buildroot}%{_datadir}/%{pkgver}/emacs-mode %changelog +* 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 From 87281fb4a8b0c51ae536997779b3c50079606124 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 16 Jan 2026 02:27:23 +0000 Subject: [PATCH 9/9] Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild --- Agda.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Agda.spec b/Agda.spec index 0fd6c04..82bdb69 100644 --- a/Agda.spec +++ b/Agda.spec @@ -25,7 +25,7 @@ Name: %{pkg_name} Version: 2.8.0 # can only be reset when all subpkgs bumped -Release: 56%{?dist} +Release: 57%{?dist} Summary: A dependently typed functional programming language and proof assistant License: MIT AND BSD-3-Clause @@ -417,6 +417,9 @@ 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