[ #5154 ] Changed Agda.cabal and stack-XYZ.yaml files.

* Removed Cabal test-suite * Removed -Werror * Removed -fprof-auto * Added doc/user-manual.pdf * Cleaning stack-XYZ.yaml files + Removed QuickCheck dependency + Removed tasty-* dependencies + Removed local package (src/size-solver)
agda · Jun 19, 2021 · 246a229 · andreasabel · Nov 29, 2021 · fgaz
1 parent 880b457
commit 246a229
Show file tree

Hide file tree

Showing 8 changed files with 1 addition and 332 deletions.
diff --git a/Agda.cabal b/Agda.cabal
@@ -77,8 +77,7 @@ extra-source-files: CHANGELOG.md
                     doc/release-notes/2.2.2.md
                     doc/release-notes/2.2.4.md
                     doc/release-notes/2.2.0.md
--- Liang-Ting (2019-11-26): See Issues #4216
---                    doc/user-manual.pdf
+                    doc/user-manual.pdf
                     stack-8.0.2.yaml
                     stack-8.2.2.yaml
                     stack-8.4.4.yaml
@@ -660,7 +659,6 @@ library
     ghc-options: -fprint-potential-instances
                  -- Initially, we disable all the warnings.
                  -w
-                 -Werror
                  -- This option must be the first one after disabling the
                  -- warnings. See Issue #2094.
                  -Wunrecognised-warning-flags
@@ -756,8 +754,6 @@ library
   if impl(ghc >= 9.0)
     ghc-options: -Werror=invalid-haddock
 
-  ghc-prof-options: -fprof-auto
-
   default-language: Haskell2010
 
   -- NOTE: If adding or removing default extensions, also change:
@@ -831,264 +827,3 @@ executable agda-mode
                   , filepath >= 1.4.1.0 && < 1.5
                   , process >= 1.4.2.0 && < 1.7
   default-language: Haskell2010
-
--- Cabal testsuite integration has some serious bugs, but we
--- can still make it work. See also:
--- https://github.com/haskell/cabal/issues/1938
--- https://github.com/haskell/cabal/issues/2214
--- https://github.com/haskell/cabal/issues/1953
---
--- This test suite should only be run using the Makefile.
--- The Makefile sets up the required environment,
--- executing the tests using cabal directly is almost
--- guarantued to fail. See also Issue 1490.
-test-suite agda-tests
-  type:             exitcode-stdio-1.0
-  hs-source-dirs:   test/
-  main-is:          Main.hs
-  other-modules:      Bugs.Tests
-                    , Compiler.Tests
-                    , Fail.Tests
-                    , Interactive.Tests
-                    , Internal.Compiler.MAlonzo.Encode
-                    , Internal.Helpers
-                    , Internal.Interaction.Highlighting.Precise
-                    , Internal.Interaction.Highlighting.Range
-                    , Internal.Interaction.Library
-                    , Internal.Interaction.Options
-                    , Internal.Syntax.Abstract.Name
-                    , Internal.Syntax.Common
-                    , Internal.Syntax.Concrete.Name
-                    , Internal.Syntax.Internal
-                    , Internal.Syntax.Parser.Parser
-                    , Internal.Syntax.Position
-                    , Internal.Termination.CallGraph
-                    , Internal.Termination.CallMatrix
-                    , Internal.Termination.Order
-                    , Internal.Termination.Semiring
-                    , Internal.Termination.SparseMatrix
-                    , Internal.Termination.Termination
-                    , Internal.Tests
-                    , Internal.TypeChecking
-                    , Internal.TypeChecking.Free
-                    , Internal.TypeChecking.Free.Lazy
-                    , Internal.TypeChecking.Generators
-                    , Internal.TypeChecking.Irrelevance
-                    , Internal.TypeChecking.Monad.Base
-                    , Internal.TypeChecking.Positivity
-                    , Internal.TypeChecking.Positivity.Occurrence
-                    , Internal.TypeChecking.Rules.LHS.Problem
-                    , Internal.TypeChecking.SizedTypes
-                    , Internal.TypeChecking.SizedTypes.Syntax
-                    , Internal.TypeChecking.SizedTypes.WarshallSolver
-                    , Internal.TypeChecking.Substitute
-                    , Internal.Utils.AssocList
-                    , Internal.Utils.Bag
-                    , Internal.Utils.BiMap
-                    , Internal.Utils.Cluster
-                    , Internal.Utils.Either
-                    , Internal.Utils.Favorites
-                    , Internal.Utils.FileName
-                    , Internal.Utils.Graph.AdjacencyMap.Unidirectional
-                    , Internal.Utils.IntSet
-                    , Internal.Utils.List
-                    , Internal.Utils.ListT
-                    , Internal.Utils.Maybe.Strict
-                    , Internal.Utils.Monoid
-                    , Internal.Utils.NonEmptyList
-                    , Internal.Utils.PartialOrd
-                    , Internal.Utils.Permutation
-                    , Internal.Utils.RangeMap
-                    , Internal.Utils.SmallSet
-                    , Internal.Utils.Three
-                    , Internal.Utils.Trie
-                    , Internal.Utils.Warshall
-                    , LaTeXAndHTML.Tests
-                    , LibSucceed.Tests
-                    , Succeed.Tests
-                    , UserManual.Tests
-                    , Utils
-
-  build-depends:  Agda
-                , array >= 0.5.1.1 && < 0.6
-                , base >= 4.9.0.0 && < 4.16
-                , bytestring >= 0.10.8.1 && < 0.12
-                -- containers-0.5.11.0 is the first to contain IntSet.intersection
-                , containers >= 0.5.11.0 && < 0.7
-                , directory >= 1.2.6.1.2 && < 1.4
-                , filepath >= 1.4.1.0 && < 1.5
-                , filemanip >= 0.3.6.3 && < 0.4
-                , mtl >= 2.2.1 && < 2.3
-                , process >= 1.4.2.0 && < 1.7
-                , process-extras >= 0.3.0 && < 0.3.4 || >= 0.4.1.3 && < 0.5 || >= 0.7.1 && < 0.8
-                , QuickCheck >= 2.14.1 && < 2.15
-                , regex-tdfa >= 1.3.1.0 && < 1.4
-                , strict >= 0.3.2 && < 0.5
-                , tasty >= 1.1.0.4 && < 1.5
-                , tasty-hunit >= 0.9.2 && < 0.11
-                , tasty-quickcheck >= 0.9.2 && < 0.11
-                -- tasty-silver 3.1.13 has option --ansi-tricks=false
-                -- NB: tasty-silver 3.2 requires tasty >= 1.4
-                , tasty-silver >= 3.1.13 && < 3.3
-                , temporary >= 1.2.0.3 && < 1.4
-                , text >= 1.2.3.0 && < 1.3
-                , unix-compat >= 0.4.3.1 && < 0.6
-                , uri-encode >= 1.5.0.4 && < 1.6
-
-  -- ASR (2018-10-16).
-  -- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and
-  -- 8.4.3. See Issue #3277.
-  -- The other GHC versions can be restricted to >= 1.2.3.1.
-  if impl(ghc < 8.4.1) || impl(ghc > 8.4.3)
-    build-depends: text >= 1.2.3.1
-
-  -- 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
-
-  default-language:  Haskell2010
-
-  -- NOTE: If adding or removing default extensions, also change:
-  --         .ghci-8.0
-  --         .hlint.yaml
-  -- This should also use the same extensions as the `library` target above.
-  default-extensions:  BangPatterns
-                     , ConstraintKinds
-                     --L-T Chen (2019-07-15):
-                     -- Enabling DataKinds only locally makes the compile time
-                     -- slightly shorter, see PR #3920.
-                     --, DataKinds
-                     , DefaultSignatures
-                     , DeriveDataTypeable
-                     , DeriveFoldable
-                     , DeriveFunctor
-                     , DeriveGeneric
-                     , DeriveTraversable
-                     , ExistentialQuantification
-                     , FlexibleContexts
-                     , FlexibleInstances
-                     , FunctionalDependencies
-                     , GeneralizedNewtypeDeriving
-                     , InstanceSigs
-                     , LambdaCase
-                     , MultiParamTypeClasses
-                     , MultiWayIf
-                     , NamedFieldPuns
-                     , OverloadedStrings
-                     , PatternSynonyms
-                     , RankNTypes
-                     , RecordWildCards
-                     , ScopedTypeVariables
-                     , StandaloneDeriving
-                     , TupleSections
-                     , TypeFamilies
-                     , TypeSynonymInstances
-
-  if flag(optimise-heavily)
-    ghc-options: -fexpose-all-unfoldings
-                 -fspecialise-aggressively
-
-  -- NOTE: If adding or removing flags, also change `.ghci-8.0`
-  if impl(ghc <= 8.0.2)
-    ghc-options: -threaded
-                 -- Initially, we disable all the warnings.
-                 -w
-                 -Werror
-                 -- This option must be the first one after disabling the
-                 -- warnings. See Issue #2094.
-                 -Wunrecognised-warning-flags
-                 -Wdeprecated-flags
-                 -Wderiving-typeable
-                 -Wdodgy-exports
-                 -Wdodgy-foreign-imports
-                 -Wdodgy-imports
-                 -Wduplicate-exports
-                 -Wempty-enumerations
-                 -Widentities
-                 -Wincomplete-patterns
-                 -Winline-rule-shadowing
-                 -Wmissing-fields
-                 -Wmissing-methods
-                 -Wmissing-pattern-synonym-signatures
-                 -Wmissing-signatures
-                 -Wnoncanonical-monad-instances
-                 -Wnoncanonical-monoid-instances
-                 -Woverflowed-literals
-                 -Woverlapping-patterns
-                 -Wsemigroup
-                 -Wtabs
-                 -Wtyped-holes
-                 -Wunrecognised-pragmas
-                 -Wunticked-promoted-constructors
-                 -Wunused-do-bind
-                 -Wunused-foralls
-                 -Wwarnings-deprecations
-                 -Wwrong-do-bind
-  else
-    ghc-options: -threaded
-                 -Werror=unrecognised-warning-flags
-                 -Werror=deprecated-flags
-                 -Werror=deriving-typeable
-                 -Werror=dodgy-exports
-                 -Werror=dodgy-foreign-imports
-                 -Werror=dodgy-imports
-                 -Werror=duplicate-exports
-                 -Werror=empty-enumerations
-                 -Werror=identities
-                 -Werror=incomplete-patterns
-                 -Werror=inline-rule-shadowing
-                 -Werror=missing-fields
-                 -Werror=missing-methods
-                 -Werror=missing-pattern-synonym-signatures
-                 -Werror=missing-signatures
-                 -Werror=noncanonical-monad-instances
-                 -Werror=noncanonical-monoid-instances
-                 -Werror=overflowed-literals
-                 -Werror=overlapping-patterns
-                 -Werror=semigroup
-                 -Werror=tabs
-                 -Werror=typed-holes
-                 -Werror=unrecognised-pragmas
-                 -Werror=unticked-promoted-constructors
-                 -Werror=unused-do-bind
-                 -Werror=unused-foralls
-                 -Werror=warnings-deprecations
-                 -Werror=wrong-do-bind
-
-  -- ASR (2017-04-11). TODO: Using -Werror=missing-home-modules generates an
-  -- error.
-  -- NOTE: If adding or removing flags, also change `.ghci-8.2`
-  if impl(ghc >= 8.2)
-    ghc-options: -Werror=cpp-undef
-                 -Werror=simplifiable-class-constraints
-                 -Werror=unbanged-strict-patterns
-
-  -- NOTE: If adding or removing flags, also change `.ghci-8.6`
-  if impl(ghc >= 8.6)
-    ghc-options: -Werror=inaccessible-code
-                 -Werror=star-binder
-                 -Werror=star-is-type
-  -- The following warning is an error in GHC >= 8.10.
-  if impl(ghc >= 8.6) && impl(ghc < 8.10)
-    ghc-options: -Werror=implicit-kind-vars
-
-  -- NOTE: If adding or removing flags, also change `.ghci-8.8`
-  if impl(ghc >= 8.8)
-    ghc-options: -Werror=missed-extra-shared-lib
-
-  -- NOTE: If adding or removing flags, also change `.ghci-8.10`
-  if impl(ghc >= 8.10)
-    ghc-options: -Werror=deriving-defaults
-                 -Werror=redundant-record-wildcards
-                 -Werror=unused-packages
-                 -Werror=unused-record-wildcards
-
-  -- NOTE: If adding or removing flags, also change `.ghci-9.0`
-  if impl(ghc >= 9.0)
-    ghc-options: -Werror=invalid-haddock
diff --git a/stack-8.0.2.yaml b/stack-8.0.2.yaml
@@ -3,7 +3,6 @@ compiler: ghc-8.0.2
 compiler-check: match-exact
 
 extra-deps:
-- QuickCheck-2.14.2
 - ansi-terminal-0.10.3
 - ansi-wl-pprint-0.6.9
 - async-2.2.1
@@ -16,15 +15,7 @@ extra-deps:
 - regex-base-0.94.0.0
 - regex-tdfa-1.3.1.0
 - splitmix-0.1.0.3
-- tasty-1.1.0.4
-- tasty-silver-3.1.13
-- tasty-quickcheck-0.10.1.1
 - text-1.2.3.1
 - uuid-types-1.0.3
 - wcwidth-0.0.2
 - text-icu-0.7.1.0
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-8.10.5.yaml b/stack-8.10.5.yaml
@@ -1,8 +1,3 @@
 resolver: lts-18.0
 compiler: ghc-8.10.5
 compiler-check: match-exact
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-8.2.2.yaml b/stack-8.2.2.yaml
@@ -3,7 +3,6 @@ compiler: ghc-8.2.2
 compiler-check: match-exact
 
 extra-deps:
-- QuickCheck-2.14.2
 - async-2.2.1
 - binary-0.8.3.0
 - cpphs-1.20.9
@@ -12,14 +11,7 @@ extra-deps:
 - regex-base-0.94.0.0
 - regex-tdfa-1.3.1.0
 - splitmix-0.1.0.3
-- tasty-1.1.0.4
-- tasty-silver-3.1.13
 - text-1.2.3.1
 - uuid-types-1.0.3
 - wcwidth-0.0.2
 - text-icu-0.7.1.0
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-8.4.4.yaml b/stack-8.4.4.yaml
@@ -3,17 +3,10 @@ compiler: ghc-8.4.4
 compiler-check: match-exact
 
 extra-deps:
-- QuickCheck-2.14.2
 - cpphs-1.20.9
 - random-1.2.0
 - regex-base-0.94.0.0
 - regex-tdfa-1.3.1.0
 - splitmix-0.1.0.3
-- tasty-silver-3.1.13
 - uuid-types-1.0.3
 - text-icu-0.7.1.0
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
@@ -3,7 +3,6 @@ compiler: ghc-8.6.5
 compiler-check: match-exact
 
 extra-deps:
-- QuickCheck-2.14.2
 - STMonadTrans-0.4.3
 - cpphs-1.20.9
 - data-hash-0.2.0.1
@@ -15,8 +14,3 @@ extra-deps:
 - splitmix-0.1.0.3
 - uuid-types-1.0.3
 - text-icu-0.7.1.0
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
-- 'src/size-solver'
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
@@ -3,12 +3,6 @@ compiler: ghc-8.8.4
 compiler-check: match-exact
 
 extra-deps:
-- QuickCheck-2.14.2
 - random-1.2.0
 - splitmix-0.1.0.3
 - text-icu-0.7.1.0
-
-# Local packages, usually specified by relative directory name
-packages:
-  - '.'
-  - 'src/size-solver'