summaryrefslogtreecommitdiff
path: root/src/full/Agda/Main.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Main.hs')
-rw-r--r--src/full/Agda/Main.hs50
1 files changed, 23 insertions, 27 deletions
diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs
index 1400682..2a2a688 100644
--- a/src/full/Agda/Main.hs
+++ b/src/full/Agda/Main.hs
@@ -12,6 +12,7 @@ import Data.Maybe
import System.Environment
import System.Exit
+import Agda.Syntax.Position (Range)
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract.Name (toTopLevelModuleName)
@@ -19,7 +20,7 @@ import Agda.Interaction.CommandLine
import Agda.Interaction.Options
import Agda.Interaction.Monad
import Agda.Interaction.EmacsTop (mimicGHCi)
-import Agda.Interaction.Imports (MaybeWarnings(..))
+import Agda.Interaction.Imports (MaybeWarnings'(..))
import qualified Agda.Interaction.Imports as Imp
import qualified Agda.Interaction.Highlighting.Dot as Dot
import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX
@@ -40,9 +41,9 @@ import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.String
-import Agda.Tests
-import Agda.Version
+import Agda.VersionCommit
+import qualified Agda.Utils.Benchmark as UtilsBench
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Impossible
@@ -67,9 +68,6 @@ runAgdaWithOptions
runAgdaWithOptions generateHTML progName opts
| optShowHelp opts = liftIO printUsage
| optShowVersion opts = liftIO printVersion
- | optRunTests opts = liftIO $ do
- ok <- testSuite
- unless ok exitFailure
| isNothing (optInputFile opts)
&& not (optInteractive opts)
&& not (optGHCiInteraction opts)
@@ -77,15 +75,21 @@ runAgdaWithOptions generateHTML progName opts
| otherwise = do
-- Main function.
-- Bill everything to root of Benchmark trie.
- Bench.billTo [] (checkFile opts) `finally_` do
+ UtilsBench.setBenchmarking True
+ -- Andreas, Nisse, 2016-10-11 AIM XXIV
+ -- Turn benchmarking on provisionally, otherwise we lose track of time spent
+ -- on e.g. LaTeX-code generation.
+ -- Benchmarking might be turned off later by setCommandlineOptions
+
+ Bench.billTo [] checkFile `finally_` do
-- Print benchmarks.
Bench.print
-- Print accumulated statistics.
printStatistics 20 Nothing =<< use lensAccumStatistics
where
- checkFile :: CommandLineOptions -> TCM ()
- checkFile opts = do
+ checkFile :: TCM ()
+ checkFile = do
let i = optInteractive opts
ghci = optGHCiInteraction opts
ghc = optGhcCompile opts
@@ -126,22 +130,14 @@ runAgdaWithOptions generateHTML progName opts
file <- getInputFile
(i, mw) <- Imp.typeCheckMain file
- unsolvedOK <- optAllowUnsolved <$> pragmaOptions
-
- -- Reported unsolved problems as error unless unsolvedOK.
-- An interface is only generated if NoWarnings.
result <- case mw of
- -- Unsolved metas.
- SomeWarnings (Warnings w@(_:_) _)
- | not unsolvedOK -> typeError $ UnsolvedMetas w
- -- Unsolved constraints.
- SomeWarnings (Warnings _ w@(_:_))
- | not unsolvedOK -> typeError $ UnsolvedConstraints w
- -- Unsolved metas, unsolved constraints, or
- -- interaction points left whose metas have been solved
- -- automatically. (See Issue 1296).
- SomeWarnings (Warnings _ _) -> return Nothing
- NoWarnings -> return $ Just i
+ SomeWarnings ws -> do
+ ws' <- applyFlagsToTCWarnings RespectFlags ws
+ case ws' of
+ [] -> return Nothing
+ cuws -> tcWarningsToError cuws
+ NoWarnings -> return $ Just i
reportSDoc "main" 50 $ pretty i
@@ -152,7 +148,7 @@ runAgdaWithOptions generateHTML progName opts
Dot.generateDot $ i
whenM (optGenerateLaTeX <$> commandLineOptions) $
- LaTeX.generateLaTeX (toTopLevelModuleName $ iModuleName i) (iHighlighting i)
+ LaTeX.generateLaTeX i
return result
@@ -164,8 +160,8 @@ printUsage = do
-- | Print version information.
printVersion :: IO ()
-printVersion =
- putStrLn $ "Agda version " ++ version
+printVersion = do
+ putStrLn $ "Agda version " ++ versionWithCommitInfo
-- | What to do for bad options.
optionError :: String -> IO ()
@@ -178,7 +174,7 @@ runTCMPrettyErrors :: TCM () -> IO ()
runTCMPrettyErrors tcm = do
r <- runTCMTop $ tcm `catchError` \err -> do
s <- prettyError err
- liftIO $ putStrLn s
+ unless (null s) (liftIO $ putStrLn s)
throwError err
case r of
Right _ -> exitSuccess