mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
181 lines
6.5 KiB
Haskell
181 lines
6.5 KiB
Haskell
-- |
|
|
-- 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
|