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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
{-# LANGUAGE NondecreasingIndentation #-}
import Data.List
import Data.Maybe
import Distribution.Simple
import Distribution.Simple.LocalBuildInfo
import Distribution.Simple.Setup
import Distribution.Simple.BuildPaths (exeExtension)
import Distribution.PackageDescription
import Distribution.System ( buildPlatform )
import System.FilePath
import System.Directory (makeAbsolute, removeFile)
import System.Environment (getEnvironment)
import System.Process
import System.Exit
import System.IO
import System.IO.Error (isDoesNotExistError)
import Control.Monad (forM_, unless)
import Control.Exception (bracket, 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 pd) $ 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 pd) $ 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 :: PackageDescription -> FilePath -> [FilePath]
expandAgdaExt pd fp | takeExtension fp == ".agda" = [ fp, toIFile pd fp ]
| otherwise = [ fp ]
version :: PackageDescription -> String
version = intercalate "." . map show . versionNumbers . pkgVersion . package
projectRoot :: PackageDescription -> FilePath
projectRoot pd = takeDirectory agdaLibFile where
[agdaLibFile] = filter ((".agda-lib" ==) . takeExtension) $ dataFiles pd
toIFile :: PackageDescription -> FilePath -> FilePath
toIFile pd file = buildDir </> fileName where
root = projectRoot pd
buildDir = root </> "_build" </> version pd </> "agda"
fileName = makeRelative root $ 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..."
-- The Agda.Primitive* and Agda.Builtin* modules.
let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
-- Remove all existing .agdai files.
forM_ builtins $ \fp -> do
let fullpathi = toIFile pd (ddir </> fp)
handleExists e | isDoesNotExistError e = return ()
| otherwise = throwIO e
removeFile fullpathi `catch` handleExists
-- Type-check all builtin modules (in a single Agda session to take
-- advantage of caching).
let loadBuiltinCmds = concat
[ [ cmd ("Cmd_load " ++ f ++ " []")
, cmd "Cmd_no_metas"
-- Fail if any meta-variable is unsolved.
]
| b <- builtins
, let f = show (ddir </> b)
cmd c = "IOTCM " ++ f ++ " None Indirect (" ++ c ++ ")"
]
env <- getEnvironment
_output <- readCreateProcess
(proc agda
[ "--interaction"
, "--interaction-exit-on-error"
, "-Werror"
, "-v0"
])
{ delegate_ctlc = True
-- Make Agda look for data files in a
-- certain place.
, env = Just (("Agda_datadir", ddir) : env)
}
(unlines loadBuiltinCmds)
return ()
agdaExeExtension :: String
agdaExeExtension = exeExtension buildPlatform
|
