1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
import Data.Maybe
import Distribution.Simple
import Distribution.Simple.LocalBuildInfo
import Distribution.Simple.Setup
import Distribution.Simple.BuildPaths (exeExtension)
import Distribution.PackageDescription
#if MIN_VERSION_Cabal(2,3,0)
import Distribution.System ( buildPlatform )
#endif
import System.FilePath
import System.Directory (makeAbsolute, removeFile)
import System.Environment (getEnvironment)
import System.Process
import System.Exit
import System.IO.Error (isDoesNotExistError)
import Control.Monad (when, forM_, unless)
import Control.Exception (catch, throwIO)
main :: IO ()
main = defaultMainWithHooks userhooks
userhooks :: UserHooks
userhooks = simpleUserHooks
{ copyHook = copyHook'
, instHook = instHook'
}
-- Install and copy hooks are default, but amended with .agdai files in data-files.
instHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> InstallFlags -> IO ()
instHook' pd lbi hooks flags = instHook simpleUserHooks pd' lbi hooks flags where
pd' = pd { dataFiles = concatMap expandAgdaExt $ dataFiles pd }
-- Andreas, 2020-04-25, issue #4569: defer 'generateInterface' until after
-- the library has been copied to a destination where it can be found.
-- @cabal build@ will likely no longer produce the .agdai files, but @cabal install@ does.
copyHook' :: PackageDescription -> LocalBuildInfo -> UserHooks -> CopyFlags -> IO ()
copyHook' pd lbi hooks flags = do
-- Copy library and executable etc.
copyHook simpleUserHooks pd lbi hooks flags
unless (skipInterfaces lbi) $ do
-- Generate .agdai files.
generateInterfaces pd lbi
-- Copy again, now including the .agdai files.
copyHook simpleUserHooks pd' lbi hooks flags
where
pd' = pd
{ dataFiles = concatMap expandAgdaExt $ dataFiles pd
-- Andreas, 2020-04-25, issue #4569:
-- I tried clearing some fields to avoid copying again.
-- However, cabal does not like me messing with the PackageDescription.
-- Clearing @library@ or @executables@ leads to internal errors.
-- Thus, we just copy things again. Not a terrible problem.
-- , library = Nothing
-- , executables = []
-- , subLibraries = []
-- , foreignLibs = []
-- , testSuites = []
-- , benchmarks = []
-- , extraSrcFiles = []
-- , extraTmpFiles = []
-- , extraDocFiles = []
}
-- Used to add .agdai files to data-files
expandAgdaExt :: FilePath -> [FilePath]
expandAgdaExt fp | takeExtension fp == ".agda" = [ fp, toIFile fp ]
| otherwise = [ fp ]
toIFile :: FilePath -> FilePath
toIFile file = replaceExtension file ".agdai"
-- Andreas, 2019-10-21, issue #4151:
-- skip the generation of interface files with program suffix "-quicker"
skipInterfaces :: LocalBuildInfo -> Bool
skipInterfaces lbi = fromPathTemplate (progSuffix lbi) == "-quicker"
generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO ()
generateInterfaces pd lbi = do
-- for debugging, these are examples how you can inspect the flags...
-- print $ flagAssignment lbi
-- print $ fromPathTemplate $ progSuffix lbi
-- then...
let bdir = buildDir lbi
agda = bdir </> "agda" </> "agda" <.> agdaExeExtension
ddir <- makeAbsolute $ "src" </> "data"
-- assuming we want to type check all .agda files in data-files
-- current directory root of the package.
putStrLn "Generating Agda library interface files..."
forM_ (dataFiles pd) $ \fp -> when (takeExtension fp == ".agda") $ do
let fullpath = ddir </> fp
let fullpathi = toIFile fullpath
-- remove existing interface file
let handleExists e | isDoesNotExistError e = return ()
| otherwise = throwIO e
removeFile fullpathi `catch` handleExists
putStrLn $ "... " ++ fullpath
ok <- rawSystem' ddir agda [ "--no-libraries", "--local-interfaces"
, "--ignore-all-interfaces"
, "-Werror"
, fullpath, "-v0"
]
case ok of
ExitSuccess -> return ()
ExitFailure _ -> die $ "Error: Failed to typecheck " ++ fullpath ++ "!"
agdaExeExtension :: String
#if MIN_VERSION_Cabal(2,3,0)
agdaExeExtension = exeExtension buildPlatform
#else
agdaExeExtension = exeExtension
#endif
rawSystem' :: FilePath -> String -> [String] -> IO ExitCode
rawSystem' agda_datadir cmd args = do
-- modify environment with Agda_datadir, so agda-executable will look
-- for data-files in the right place
e <- getEnvironment
let e' = ("Agda_datadir", agda_datadir) : e
(_,_,_,p) <- createProcess_ "rawSystem" (proc cmd args) { delegate_ctlc = True, env = Just e' }
waitForProcess p
|
