Setup.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE TemplateHaskell #-}

-- | Agda's self-setup.

module Agda.Setup
  ( getAgdaAppDir
  , getDataDir
  , getDataFileName
  , setup
  )
where

import           Control.Exception          ( IOException, try )
import           Control.Monad              ( forM, forM_, unless, void, when )

import           Data.ByteString            ( ByteString )
import qualified Data.ByteString            as BS
import           Data.Functor               ( (<&>) )
import           Data.List                  ( intercalate )

import           Language.Haskell.TH.Syntax ( qAddDependentFile, runIO )

-- Import instance Lift ByteString if not supplied by bytestring.
#if !MIN_VERSION_bytestring(0,11,2)
import           Instances.TH.Lift          ()
#endif

import           System.Directory
  ( XdgDirectory (..)
  , canonicalizePath, createDirectoryIfMissing, doesDirectoryExist
  , getAppUserDataDirectory, getXdgDirectory, removeFile
  )
import           System.Environment         ( lookupEnv )
import           System.FileLock            ( pattern Exclusive, withFileLock )
import           System.FilePath            ( (</>), joinPath, splitFileName, takeFileName )
import           System.IO                  ( hPutStrLn, stderr )

import           Agda.Setup.DataFiles       ( dataFiles, dataPath )
import           Agda.VersionCommit         ( versionWithCommitInfo )

import qualified Paths_Agda                 as Paths

-- | Given the `Agda_datadir`, what should the Agda data dir be?

mkDataDir :: FilePath -> FilePath
mkDataDir =
#ifdef USE_XDG_DATA_HOME
  (</> versionWithCommitInfo)
#else
  id
#endif

-- Tell TH that all the dataFiles are needed for compilation.
[] <$ mapM_ (qAddDependentFile . dataPath) dataFiles

-- | The embedded contents of the Agda data directory,
--   generated by Template Haskell at compile time.

embeddedDataDir :: [(FilePath, ByteString)]
embeddedDataDir = $(do

    -- Load all the dataFiles.
    contents <- runIO $ mapM (BS.readFile . dataPath) dataFiles

    -- Return the association list as Exp.
    [| zip dataFiles contents |]
  )

-- | Get the path to @~/.agda@ (system-specific).
--   Can be overwritten by the @AGDA_DIR@ environment variable.
--
--   (This is not to be confused with the directory 'getDataDir' for the data files
--   that Agda needs (e.g. the primitive modules).)
--
getAgdaAppDir :: IO FilePath
getAgdaAppDir = do
  -- The default can be overwritten by setting the AGDA_DIR environment variable
  lookupEnv "AGDA_DIR" >>= \case
    Nothing -> agdaDir
    Just dir -> doesDirectoryExist dir >>= \case
      True  -> canonicalizePath dir
      False -> do
        d <- agdaDir
        inform $ "Warning: Environment variable AGDA_DIR points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
        return d
  where
    -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
    agdaDir = do
      legacyAgdaDir <- getAppUserDataDirectory "agda"
      doesDirectoryExist legacyAgdaDir >>= \case
        True  -> return legacyAgdaDir
        False -> getXdgDirectory XdgConfig "agda"

-- | This overrides the 'getDataDir' from ''Paths_Agda''.
--   See the documentation for the @--print-agda-data-dir@ flag.

getDataDir :: IO FilePath
getDataDir = mkDataDir <$> getBaseDataDir

getBaseDataDir :: IO FilePath
getBaseDataDir = do
  lookupEnv "Agda_datadir" >>= \case
    Just dir -> doesDirectoryExist dir >>= \case
      True  -> canonicalizePath dir
      False -> do
        d <- defaultBaseDataDir
        inform $ "Warning: Environment variable Agda_datadir points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
        return d
    Nothing -> defaultBaseDataDir

defaultBaseDataDir :: IO FilePath
defaultBaseDataDir = do
#ifdef USE_XDG_DATA_HOME
  getXdgDirectory XdgData "agda"
#else
  Paths.getDataDir
#endif

-- | This overrides the 'getDataFileName' from ''Paths_Agda''.

getDataFileName :: FilePath -> IO FilePath
getDataFileName f = getDataDir <&> (</> f)

-- | @False@: Check whether we need to setup Agda.
--   This function can be called when starting up Agda.
--
-- @True@: force a setup e.g. when passing Agda option @--setup@.
--
-- Copies the embedded data files to the designated data directory.

setup :: Bool -> IO ()
setup force = do
  dir <- getBaseDataDir
  let doSetup = dumpDataDir force dir

  if force then doSetup else do
    ex <- doesDirectoryExist $ mkDataDir dir
    unless ex doSetup


-- | Spit out the embedded files into Agda data directory relative to the given directory.
--   Lock the directory while doing so.

dumpDataDir :: Bool -> FilePath -> IO ()
dumpDataDir verbose baseDataDir = do
  let dataDir = mkDataDir baseDataDir
  createDirectoryIfMissing True dataDir

  -- Create a file lock to prevent races caused by the dataDir already created
  -- but not filled with its contents.
  let lock = baseDataDir </> intercalate "-" [".lock", versionWithCommitInfo]
  withFileLock lock Exclusive \ _lock -> do

    forM_ embeddedDataDir \ (relativePath, content) -> do

      -- Make sure we also create the directories along the way.
      let (relativeDir, file) = splitFileName relativePath
      let dir  = dataDir </> relativeDir
      createDirectoryIfMissing True dir

      -- Write out the file contents.
      let path = dir </> file
      when verbose $ inform $ "Writing " ++ path
      BS.writeFile path content

  -- Remove the lock (this is surprisingly not done by withFileLock).
  -- Ignore any IOException (e.g. if the file does not exist).
  void $ try @IOException $ removeFile lock

-- | Dump line of warning or information to stderr.
inform :: String -> IO ()
inform = hPutStrLn stderr