1
Description: Compile with libraries in Debian
2
Author: Nils Anders Danielsson <nils.anders.danielsson@gmail.com>
6
Thu Feb 24 10:33:21 GMT 2011 Nils Anders Danielsson <nils.anders.danielsson@gmail.com>
7
* Made Agda build using GHC 6.12.3, mtl 1.1.0.2 and QuickCheck 2.1.0.3.
9
===================================================================
10
--- agda.orig/Agda.cabal 2011-02-24 18:19:56.317593241 +0000
11
+++ agda/Agda.cabal 2011-02-24 18:22:33.703954610 +0000
13
Note also that this library does not follow the package versioning
14
policy, because the library is only intended to be used by the Emacs
15
mode and the Agda-executable package.
16
-tested-with: GHC == 6.12.1, GHC == 6.12.3, GHC == 7.0.1
17
+tested-with: GHC == 6.12.3
18
extra-source-files: src/full/Agda/undefined.h
20
doc/release-notes/*.txt
23
hs-source-dirs: src/full
25
- build-depends: base >= 4.2 && < 4.4
26
+ build-depends: base >= 4.2 && < 4.3
28
build-depends: base == 4.1.*,
31
build-depends: epic >= 0.1.7 && < 0.2
32
- build-depends: mtl == 2.0.*,
33
- QuickCheck >= 2.3 && < 2.5,
34
+ build-depends: mtl >= 1.1 && < 2,
35
+ QuickCheck >= 2.1.0.2 && < 2.5,
36
haskell-src-exts >= 1.9.6 && < 1.10,
37
containers >= 0.1.0 && < 1,
39
Index: agda/src/full/Agda/Interaction/Options.hs
40
===================================================================
41
--- agda.orig/src/full/Agda/Interaction/Options.hs 2011-02-24 18:19:56.337595320 +0000
42
+++ agda/src/full/Agda/Interaction/Options.hs 2011-02-24 18:22:33.703954610 +0000
46
import Control.Monad ( when )
47
-import Control.Monad.Error ( MonadError(..) )
48
+import Control.Monad.Error ( MonadError(catchError) )
49
import Data.List ( isSuffixOf )
50
import System.Console.GetOpt (getOpt, usageInfo, ArgOrder(ReturnInOrder)
51
, OptDescr(..), ArgDescr(..)
54
case optInputFile o of
55
Nothing -> return $ o { optInputFile = Just f }
56
- Just _ -> throwError "only one input file allowed"
57
+ Just _ -> fail "only one input file allowed"
59
versionFlag o = return $ o { optShowVersion = True }
60
helpFlag o = return $ o { optShowHelp = True }
63
n <- readM (last ss) `catchError` \_ -> usage
65
- usage = throwError "argument to verbose should be on the form x.y.z:N or N"
66
+ usage = fail "argument to verbose should be on the form x.y.z:N or N"
68
terminationDepthFlag s o =
69
do k <- readM s `catchError` \_ -> usage
70
when (k < 1) $ usage -- or: turn termination checking off for 0
71
return $ o { optTerminationDepth = k-1 }
72
- where usage = throwError "argument to termination-depth should be >= 1"
73
+ where usage = fail "argument to termination-depth should be >= 1"
75
integerArgument :: String -> String -> Either String Int
76
integerArgument flag s =
77
readM s `catchError` \_ ->
78
- throwError $ "option '" ++ flag ++ "' requires an integer argument"
79
+ fail $ "option '" ++ flag ++ "' requires an integer argument"
81
standardOptions :: [OptDescr (Flag CommandLineOptions)]
84
parseOptions' argv opts fileArg = \defaults ->
85
case getOpt (ReturnInOrder fileArg) opts argv of
86
(o,_,[]) -> foldl (>>=) (return defaults) o
87
- (_,_,errs) -> throwError $ concat errs
88
+ (_,_,errs) -> fail $ concat errs
90
-- | Parse the standard options.
91
parseStandardOptions :: [String] -> Either String CommandLineOptions
93
-> Either String PragmaOptions
94
parsePragmaOptions argv opts = do
95
ps <- parseOptions' argv pragmaOptions
96
- (\s _ -> throwError $ "Bad option in pragma: " ++ s)
97
+ (\s _ -> fail $ "Bad option in pragma: " ++ s)
98
(optPragmaOptions opts)
99
checkOpts (opts { optPragmaOptions = ps })
102
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
103
parsePluginOptions argv opts =
104
parseOptions' argv opts
105
- (\s _ -> throwError $
106
- "Internal error: Flag " ++ s ++ " passed to a plugin")
107
+ (\s _ -> fail $ "Internal error: Flag " ++ s ++ " passed to a plugin")
109
-- | The usage info message. The argument is the program name (probably
111
Index: agda/src/full/Agda/Syntax/Notation.hs
112
===================================================================
113
--- agda.orig/src/full/Agda/Syntax/Notation.hs 2011-02-24 18:19:56.337595320 +0000
114
+++ agda/src/full/Agda/Syntax/Notation.hs 2011-02-24 18:22:33.703954610 +0000
117
import Control.Applicative
118
import Control.Monad (when)
119
-import Control.Monad.Error (throwError)
122
import Data.Generics (Typeable, Data)
125
-- | From notation with names to notation with indices.
126
mkNotation :: [HoleName] -> [String] -> Either String Notation
127
-mkNotation _ [] = throwError "empty notation is disallowed"
128
+mkNotation _ [] = fail "empty notation is disallowed"
129
mkNotation holes ids = do
130
xs <- mapM mkPart ids
131
- when (not (isAlternating xs)) $ throwError "syntax must alternate holes and non-holes"
132
- when (not (isExprLinear xs)) $ throwError "syntax must use holes exactly once"
133
- when (not (isLambdaLinear xs)) $ throwError "syntax must use binding holes exactly once"
134
+ when (not (isAlternating xs)) $ fail "syntax must alternate holes and non-holes"
135
+ when (not (isExprLinear xs)) $ fail "syntax must use holes exactly once"
136
+ when (not (isLambdaLinear xs)) $ fail "syntax must use binding holes exactly once"
139
case (findIndices (\x -> ident == holeName x) holes,
141
([],[x]) -> return $ BindHole x
142
([x], []) -> return $ NormalHole x
143
([], []) -> return $ IdPart ident
144
- _ -> throwError "hole names must be unique"
145
+ _ -> fail "hole names must be unique"
147
isExprLinear xs = sort [ x | NormalHole x <- xs] == [ i | (i,h) <- zip [0..] holes ]
148
isLambdaLinear xs = sort [ x | BindHole x <- xs] == [ i | (i,h) <- zip [0..] holes, isLambdaHole h ]
149
Index: agda/src/full/Agda/Utils/Monad.hs
150
===================================================================
151
--- agda.orig/src/full/Agda/Utils/Monad.hs 2011-02-24 18:19:56.357597401 +0000
152
+++ agda/src/full/Agda/Utils/Monad.hs 2011-02-24 18:22:33.703954610 +0000
154
-{-# LANGUAGE FlexibleContexts, CPP #-}
155
+{-# LANGUAGE CPP #-}
157
module Agda.Utils.Monad
158
( module Agda.Utils.Monad
160
#include "../undefined.h"
161
import Agda.Utils.Impossible
163
+-- Instances --------------------------------------------------------------
165
+instance Applicative (Reader env) where
169
+instance (Error e, Monad m) => Applicative (ErrorT e m) where
173
+instance Monad m => Applicative (ReaderT env m) where
177
+instance Monad m => Applicative (StateT s m) where
181
+instance Monad m => Applicative (SS.StateT s m) where
185
+instance (Monoid o, Monad m) => Applicative (WriterT o m) where
189
+instance Applicative (State s) where
193
-- Monads -----------------------------------------------------------------
198
-- Read -------------------------------------------------------------------
200
-readM :: (Error e, MonadError e m, Read a) => String -> m a
201
+readM :: (Monad m, Read a) => String -> m a
202
readM s = case reads s of
205
- throwError $ strMsg $ "readM: parse error string " ++ s
206
+ _ -> fail $ "readM: parse error string " ++ s
added
removed
debian/patches/relax-build-dependencies
