cryptol/docs/ProgrammingCryptol/tools/compileProgrammingCryptol.hs

-- |
-- Module      :  Main
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# OPTIONS -Wall #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE ImplicitParams #-}

module Main(main) where

import Control.Parallel.Strategies
import Data.Char
import Data.List
import Numeric
import System.Exit
import System.IO
import System.Timeout
import System.Directory
import System.FilePath
import System.Process
import System.Time


---------------------------------------------------------------
-- Configuration

targetName :: String
targetName = "Cryptol"

topDir       :: FilePath
topDir       = "/Volumes/Galois/Projects/CTK/Cryptol/teardrop/Documentation/ProgrammingCryptol"

fullTriggers :: [FilePath] -- these trigger full compile
fullTriggers = [ "bib"  </> "cryptol.bib"
               , "utils" </> "Indexes.tex"
               , "utils" </> "GlossaryItems.tex"
               ]

-- rest is derived or should be glacial, but better checkout
tmpDir :: FilePath
tmpDir = "/tmp"

logFile :: FilePath   -- latex log
logFile = tmpDir </> targetName <.> "log"

target :: FilePath    -- final pdf
target = targetName <.> "pdf"

title :: String  -- growl title
title = targetName
---------------------------------------------------------------
-- utils
ifM :: Monad m => m Bool -> m a -> m a -> m a
ifM t tb fb = t >>= \b -> if b then tb else fb

whenM :: Monad m => m Bool -> m () -> m ()
whenM t a = ifM t a (return ())

ignore :: Monad m => m a -> m ()
ignore m = m >> return ()

modTime :: FilePath -> IO (Maybe ClockTime)
modTime fn = fmap Just (getModificationTime fn) `catch` const (return Nothing)

safeSys :: IO () -> IO ()
safeSys a = a `catch` die
  where die e = do putStrLn $ "\nException: " ++ show e
                   exitWith (ExitFailure 1)

instance NFData ExitCode

timeIt :: NFData a => IO a -> IO (String, a)
timeIt m = do start <- getClockTime
              r <- m
              end <- rnf r `seq` getClockTime
              let elapsed  = diffClockTimes end start
                  elapsedS = "Elapsed:" ++ showTDiff elapsed
              rnf elapsedS `seq` return (elapsedS, r)
  where showTDiff :: TimeDiff -> String
        showTDiff itd = et
          where td = normalizeTimeDiff itd
                vals = dropWhile (\(v, _) -> v == 0) (zip [tdYear td, tdMonth td, tdDay td, tdHour td, tdMin td] "YMDhm")
                sec = ' ' : show (tdSec td) ++ dropWhile (/= '.') pico
                pico = showFFloat (Just 3) (((10**(-12))::Double) * fromIntegral (tdPicosec td)) "s"
                et = concatMap (\(v, c) -> ' ':show v ++ [c]) vals ++ sec

growl :: (?curId :: Id) => Bool -> String -> [String] -> IO ()
growl goaway t s = ignore $ readProcess "growlnotify" (stickyArg ++ [title, t] ++ ["-d", "Cryptol" ++ show ?curId] ++ ["-m", args]) ""
  where stickyArg | goaway = []
                  | True   = ["-s"]
        args = concat $ intersperse "\n" s
---------------------------------------------------------------

type Id = Integer

main :: IO ()
main = do hSetBuffering stdin NoBuffering
          hSetBuffering stdout NoBuffering
          hSetEcho stdout False
          safeSys $ setCurrentDirectory topDir
          let ?curId = 0 in prompt True

prompt :: (?curId :: Id) => Bool -> IO ()
prompt tout = do
      let curId'  = ?curId+1
          prompt' = let ?curId = curId' in prompt
      putStr $ "\r" ++ replicate 60 ' ' ++ "\r" ++ if tout then promptS else promptWS
      mbc <- (if tout then timeout 1000000 else (fmap Just)) getChar
      case fmap toUpper mbc of
        Nothing  -> whenM need (ifM needFull full quick) >> prompt' True
        Just 'L' -> quick >> prompt' True
        Just 'F' -> full  >> prompt' True
        Just 'C' -> prompt' True
        Just 'W' -> prompt' False
        Just 'Q' -> do putStrLn "\nTerminating.."
                       exitWith ExitSuccess
        _        -> prompt' True
  where promptS, promptWS :: String
        promptS  = "Action (l[atex] f[ull] w[ait] q[uit])? "
        promptWS = "Action (l[atex] f[ull] w[ait] q[uit] c[ontinue])? "

needFull :: IO Bool
needFull = do mtt  <- modTime target
              mtts <- mapM modTime fullTriggers
              return $ any (> mtt) mtts

quick :: (?curId :: Id) => IO ()
quick = do whenM (doesFileExist target) $ removeFile target
           make "quick" ["quick"]

full  :: (?curId :: Id) => IO ()
full = do _ <- readProcess "make" ["superClean"] ""
          make "full" []

need :: IO Bool
need = do r <- readProcess "make" ["-n"] ""
          return $ dropWhile (/= ':') r /= ": Nothing to be done for `all'.\n"

make :: (?curId :: Id) => String -> [String] -> IO ()
make how args = do
    growl False "" $ ["Starting " ++ how ++ " compilation"]
    (d, ec) <- timeIt $ system $ unwords $ "make" : args
    case ec of
      ExitFailure _ -> dieErrors
      ExitSuccess   -> checkWarnings d

dieErrors :: (?curId :: Id) => IO ()
dieErrors = do logCts <- readFile logFile >>= return . filter (not . all isSpace) . lines
               let process (x:y:z:rest) sofar
                     | take 2 y == "l." = process rest (z:y:x:sofar)
                     | True             = process (y:z:rest) sofar
                   process _ sofar  = sofar
                   badLines = process logCts []
               growl False "(FAILED)" badLines

checkWarnings :: (?curId :: Id) => String -> IO ()
checkWarnings d = do logLines <- readFile logFile >>= return . lines
                     let badLines = filter isEither logLines
                     case badLines of
                       [] -> checkSpelling d
                       _  -> growl False "(FAILED)" $ badLines
  where (lw, w) = (length w, "LaTeX Warning")
        (lu, u) = (length u, "undefined")
        isWarning   s = any (\l -> take lw l == w) $ tails s
        isUndefined s = any (\l -> take lu l == u) $ tails s
        isEither s = isWarning s || isUndefined s

checkSpelling :: (?curId :: Id) => String -> IO ()
checkSpelling d = do logCts <- readProcessWithExitCode "make" ["quickSpell"] "" >>= \(_, out, err) -> return (lines (out ++ err))
                     let new = map (drop 2) $ filter (\l -> take 1 l == "<") logCts
                         old = map (drop 2) $ filter (\l -> take 1 l == ">") logCts
                     case new of
                       [] -> case old of
                               [] -> growl True "(SUCCESS)" [d]
                               _  -> growl False "(SUCCESS, Fixed words)" $ old
                       _  -> growl False "(FAILED Spell check)" $ new