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