17f0899 · Idris-dev · git.iko.soy

CHANGELOG.md+6−5

@@ -12,11 +12,12 @@

1212

1313## Tool Updates

1414

15−+ Idris' logging output has been updated to more accurately reflect

16− its progress through the compiler. Idris, when verbose, will report

17− explicitly: Type Checking; Totality Checking; IBC Generation;

18− Compiling; and Code Generation.

19−

15++ Idris' output has been updated to more accurately reflect its

16+ progress through the compiler i.e. Type Checking; Totality Checking;

17+ IBC Generation; Compiling; and Code Generation. To control the

18+ loudness of the reporting three verbosity levels are introduced:

19+ `--V0`, `--V1`, and `--V2`. The old aliases of `-V` and `--verbose`

20+ persist.

2021

2122## Library Updates

2223

docs/reference/compilation.rst+23−7

@@ -1,6 +1,6 @@

1−***********************

2−Compilation and Logging

3−***********************

1+************************************

2+Compilation, Logging, and Reporting

3+************************************

44

55This section provides information about the Idris compilation process, and

66provides details over how you can follow the process through logging.

@@ -41,11 +41,27 @@ With Idris you can ask it to terminate the compilation process after type checki

4141

4242Use of this option will still result in the generation of the Idris binary ``.ibc`` files, and is suitable if you do not wish to generate code from one of the supported backends.

4343

44−Logging Output

45−==============

44+Reporting Compilation Process

45+=============================

4646

47−The internal operation of Idris is captured using a category based logger.

48−Currently, the logging infrastructure has support for the following categories:

47+During compilation the reporting of Idris' progress can be controlled

48+by setting a verbosity level.

49+

50++ ``-V``, or alternatively ``--verbose`` and ``--V0``, will report which file Idris is currently type checking.

51++ ``--V1`` will additionally report: Parsing, IBC Generation, and Code

52+ Generation.

53++ ``--V2`` will additionally report: Totality Checking, Universe

54+ Checking, and the individual steps prior to code generation.

55+

56+

57+By default Idris' progress reporting is set to quiet-``-q``, or ``--quiet``.

58+

59+Logging Internal Operation

60+===========================

61+

62+For those that develop on the Idris compiler, the internal operation

63+of Idris is captured using a category based logger. Currently, the

64+logging infrastructure has support for the following categories:

4965

5066+ Parser

5167+ Elaborator

main/Main.hs+1−1

@@ -39,7 +39,7 @@ processClientOptions :: [Opt] -> Idris ()

3939processClientOptions opts = check opts getClient $ \fs -> case fs of

4040 [] -> ifail "No --client argument. This indicates a bug. Please report."

4141 (c : _) -> do

42− setVerbose False

42+ setVerbose 0

4343 setQuiet True

4444 case getPort opts of

4545 Just DontListen -> ifail "\"--client\" and \"--port none\" are incompatible"

man/idris.1+3−1

@@ -68,7 +68,9 @@ should not necessarily be seen as production ready nor for industrial use.

6868 --listlibs Display installed libraries

6969 --libdir Display library directory

7070 --include Display the includes flags

71− -V,--verbose Loud verbosity

71+ --V2 Loudest verbosity

72+ --V1 Louder verbosity

73+ -V, --V0, --verbose Loud verbosity

7274 --ibcsubdir FILE Write IBC files into sub directory

7375 -i,--idrispath ARG Add directory to the list of import paths

7476 --sourcepath ARG Add directory to the list of source search paths

src/IRTS/Compiler.hs+4

@@ -54,6 +54,7 @@ import System.Process

5454compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

5555compile codegen f mtm = do

5656 logCodeGen 1 "Compiling Output."

57+ iReport 2 "Compiling Output."

5758 checkMVs -- check for undefined metavariables

5859 checkTotality -- refuse to compile if there are totality problems

5960 exports <- findExports

@@ -90,9 +91,11 @@ compile codegen f mtm = do

9091 let ctxtIn = addAlist tagged emptyContext

9192

9293 logCodeGen 1 "Defunctionalising"

94+ iReport 3 "Defunctionalising"

9395 let defuns_in = defunctionalise nexttag ctxtIn

9496 logCodeGen 5 $ show defuns_in

9597 logCodeGen 1 "Inlining"

98+ iReport 3 "Inlining"

9699 let defuns = inline defuns_in

97100 logCodeGen 5 $ show defuns

98101 logCodeGen 1 "Resolving variables for CG"

@@ -110,6 +113,7 @@ compile codegen f mtm = do

110113 triple <- Idris.AbsSyntax.targetTriple

111114 cpu <- Idris.AbsSyntax.targetCPU

112115 logCodeGen 1 "Generating Code."

116+ iReport 2 "Generating Code."

113117 case checked of

114118 OK c -> do return $ CodegenInfo f outty triple cpu

115119 hdrs impdirs objs libs flags

src/Idris/AbsSyntax.hs+25−11

@@ -385,7 +385,7 @@ allNames ns n = do i <- getIState

385385 case getCGAllNames i n of

386386 Just ns -> return ns

387387 Nothing -> case lookupCtxtExact n (idris_callgraph i) of

388− Just ci ->

388+ Just ci ->

389389 do more <- mapM (allNames (n:ns)) (calls ci)

390390 let ns' = nub (n : concat more)

391391 addCGAllNames i n ns'

@@ -1024,17 +1024,31 @@ targetCPU :: Idris String

10241024targetCPU = do i <- getIState

10251025 return (opt_cpu (idris_options i))

10261026

1027−verbose :: Idris Bool

1028−verbose = do i <- getIState

1029− -- Quietness overrides verbosity

1030− return (not (opt_quiet (idris_options i)) &&

1031− opt_verbose (idris_options i))

1027+verbose :: Idris Int

1028+verbose = do

1029+ i <- getIState

1030+ -- Quietness overrides verbosity

1031+ let quiet = opt_quiet $ idris_options i

1032+ if quiet

1033+ then return $ 0

1034+ else return $ (opt_verbose $ idris_options i)

1035+

1036+setVerbose :: Int -> Idris ()

1037+setVerbose t = do

1038+ i <- getIState

1039+ let opts = idris_options i

1040+ let opt' = opts { opt_verbose = t }

1041+ putIState $ i { idris_options = opt' }

10321042

1033−setVerbose :: Bool -> Idris ()

1034−setVerbose t = do i <- getIState

1035− let opts = idris_options i

1036− let opt' = opts { opt_verbose = t }

1037− putIState $ i { idris_options = opt' }

1043+iReport :: Int -> String -> Idris ()

1044+iReport level msg = do

1045+ verbosity <- verbose

1046+ i <- getIState

1047+ when (level <= verbosity) $

1048+ case idris_outputmode i of

1049+ RawOutput h -> runIO $ hPutStrLn h msg

1050+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" msg n

1051+ return ()

10381052

10391053typeInType :: Idris Bool

10401054typeInType = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4−4

@@ -91,7 +91,7 @@ data IOption = IOption {

9191 , opt_showimp :: Bool -- ^ show implicits

9292 , opt_errContext :: Bool

9393 , opt_repl :: Bool

94− , opt_verbose :: Bool

94+ , opt_verbose :: Int

9595 , opt_nobanner :: Bool

9696 , opt_quiet :: Bool

9797 , opt_codegen :: Codegen

@@ -120,7 +120,7 @@ defaultOpts = IOption { opt_logLevel = 0

120120 , opt_showimp = False

121121 , opt_errContext = False

122122 , opt_repl = True

123− , opt_verbose = False

123+ , opt_verbose = 0

124124 , opt_nobanner = False

125125 , opt_quiet = False

126126 , opt_codegen = Via IBCFormat "c"

@@ -512,7 +512,7 @@ data Opt = Filename String

512512 | NoCoverage

513513 | ErrContext

514514 | ShowImpl

515− | Verbose

515+ | Verbose Int

516516 | Port REPLPort -- ^ REPL TCP port

517517 | IBCSubDir String

518518 | ImportDir String

@@ -2472,7 +2472,7 @@ implicitNamesIn uvars ist tm

24722472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

24732473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

24742474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2475− ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;

2475+ ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;

24762476 ni 0 env val; ni 0 (n:env) sc

24772477 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

24782478 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

src/Idris/CmdOptions.hs+3−1

@@ -134,7 +134,9 @@ parseFlags = many $

134134 <|> flag' ShowDocDir (long "docdir" <> help "Display idrisdoc install directory")

135135 <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

136136

137− <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

137+ <|> flag' (Verbose 3) (long "V2" <> help "Loudest verbosity")

138+ <|> flag' (Verbose 2) (long "V1" <> help "Louder verbosity")

139+ <|> flag' (Verbose 1) (short 'V' <> long "V0" <>long "verbose" <> help "Loud verbosity")

138140

139141 <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

140142 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

src/Idris/IBC.hs+2−1

@@ -221,7 +221,8 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch

221221writeIBC :: FilePath -> FilePath -> Idris ()

222222writeIBC src f

223223 = do

224− logIBC 1 $ "Writing IBC for: " ++ show f

224+ logIBC 1 $ "Writing IBC for: " ++ show f

225+ iReport 2 $ "Writing IBC for: " ++ show f

225226 i <- getIState

226227-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

227228-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

src/Idris/Main.hs+5−2

@@ -68,7 +68,6 @@ idrisMain opts =

6868 let nobanner = NoBanner `elem` opts

6969 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

7070 let runrepl = not (NoREPL `elem` opts)

71− let verbose = runrepl || Verbose `elem` opts

7271 let output = opt getOutput opts

7372 let ibcsubdir = opt getIBCSubDir opts

7473 let importdirs = opt getImportDir opts

@@ -116,13 +115,16 @@ idrisMain opts =

116115 mapM_ addLangExt (opt getLanguageExt opts)

117116 setREPL runrepl

118117 setQuiet (quiet || isJust script || not (null immediate))

119− setVerbose verbose

118+

120119 setCmdLine opts

121120 setOutputTy outty

122121 setNoBanner nobanner

123122 setCodegen cgn

124123 mapM_ (addFlag cgn) cgFlags

125124 mapM_ makeOption opts

125+ vlevel <- verbose

126+ when (runrepl && vlevel == 0) $ setVerbose 1

127+

126128 -- if we have the --bytecode flag, drop into the bytecode assembler

127129 case bcs of

128130 [] -> return ()

@@ -215,6 +217,7 @@ idrisMain opts =

215217 where

216218 makeOption (OLogging i) = setLogLevel i

217219 makeOption (OLogCats cs) = setLogCats cs

220+ makeOption (Verbose v) = setVerbose v

218221 makeOption TypeCase = setTypeCase True

219222 makeOption TypeInType = setTypeInType True

220223 makeOption NoCoverage = setCoverage False

src/Idris/Package.hs+6−5

@@ -71,14 +71,14 @@ buildPkg copts warnonly (install, fp) = do

7171 make (makefile pkgdesc)

7272 case (execout pkgdesc) of

7373 Nothing -> do

74− case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of

74+ case mergeOptions copts (idx : NoREPL : Verbose 1 : idris_opts pkgdesc) of

7575 Left emsg -> do

7676 putStrLn emsg

7777 exitWith (ExitFailure 1)

7878 Right opts -> buildMods opts (modules pkgdesc)

7979 Just o -> do

8080 let exec = dir </> o

81− case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of

81+ case mergeOptions copts (idx : NoREPL : Verbose 1 : Output exec : idris_opts pkgdesc) of

8282 Left emsg -> do

8383 putStrLn emsg

8484 exitWith (ExitFailure 1)

@@ -115,7 +115,7 @@ checkPkg copts warnonly quit fpath = do

115115 res <- inPkgDir pkgdesc $ do

116116 make (makefile pkgdesc)

117117

118− case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of

118+ case mergeOptions copts (NoREPL : Verbose 1 : idris_opts pkgdesc) of

119119 Left emsg -> do

120120 putStrLn emsg

121121 exitWith (ExitFailure 1)

@@ -195,7 +195,7 @@ documentPkg copts (install,fp) = do

195195 cd <- getCurrentDirectory

196196 let pkgDir = cd </> takeDirectory fp

197197 outputDir = cd </> pkgname pkgdesc ++ "_doc"

198− popts = NoREPL : Verbose : idris_opts pkgdesc

198+ popts = NoREPL : Verbose 1 : idris_opts pkgdesc

199199 mods = modules pkgdesc

200200 fs = map (foldl1' (</>) . splitOn "." . showCG) mods

201201 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

@@ -259,7 +259,7 @@ testPkg copts fp = do

259259 hClose tmph

260260 (tmpn', tmph') <- tempfile ""

261261 hClose tmph'

262− let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)

262+ let popts = (Filename tmpn : NoREPL : Verbose 1 : Output tmpn' : idris_opts pkgdesc)

263263 case mergeOptions copts popts of

264264 Left emsg -> do

265265 putStrLn emsg

@@ -442,6 +442,7 @@ mergeOptions copts popts =

442442 chkOpt o@(IBCSubDir _) = Right o

443443 chkOpt o@(ImportDir _ ) = Right o

444444 chkOpt o@(UseCodegen _) = Right o

445+ chkOpt o@(Verbose _) = Right o

445446 chkOpt o = Left (unwords ["\t", show o, "\n"])

446447

447448 genErrMsg :: [String] -> String

src/Idris/Parser.hs+5−3

@@ -1700,6 +1700,7 @@ loadSource' lidr r maxline

17001700loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

17011701loadSource lidr f toline

17021702 = do logParser 1 ("Reading " ++ f)

1703+ iReport 2 ("Reading " ++ f)

17031704 i <- getIState

17041705 let def_total = default_total i

17051706 file_in <- runIO $ readSource f

@@ -1787,8 +1788,7 @@ loadSource lidr f toline

17871788 logLvl 10 (show (toAlist (idris_implicits i)))

17881789 logLvl 3 (show (idris_infixes i))

17891790 -- Now add all the declarations to the context

1790− v <- verbose

1791− when v $ iputStrLn $ "Type checking " ++ f

1791+ iReport 1 $ "Type checking " ++ f

17921792 -- we totality check after every Mutual block, so if

17931793 -- anything is a single definition, wrap it in a

17941794 -- mutual block on its own

@@ -1803,6 +1803,7 @@ loadSource lidr f toline

18031803 setContext ctxt')

18041804 (map snd (idris_totcheck i))

18051805 -- build size change graph from simplified definitions

1806+ iReport 3 $ "Totality checking " ++ f

18061807 logLvl 1 $ "Totality checking " ++ f

18071808 i <- getIState

18081809 mapM_ buildSCG (idris_totcheck i)

@@ -1826,7 +1827,8 @@ loadSource lidr f toline

18261827

18271828 logLvl 1 ("Finished " ++ f)

18281829 ibcsd <- valIBCSubDir i

1829− logLvl 1 $ "Universe checking " ++ f

1830+ logLvl 1 $ "Universe checking " ++ f

1831+ iReport 3 $ "Universe checking " ++ f

18301832 iucheck

18311833 let ibc = ibcPathNoFallback ibcsd f

18321834 i <- getIState

src/Idris/REPL.hs+2−3

@@ -194,7 +194,7 @@ processNetCmd orig i h fn cmd

194194 setErrContext True

195195 setOutH h

196196 setQuiet True

197− setVerbose False

197+ setVerbose 0

198198 mods <- loadInputs [f] toline

199199 ist <- getIState

200200 return (ist, f)

@@ -1273,7 +1273,7 @@ process fn (Missing n)

12731273 case lookupCtxt n (idris_patdefs i) of

12741274 [] -> iPrintError $ "Unknown name " ++ show n

12751275 [(_, tms)] ->

1276− iRenderResult (vsep (map (pprintPTerm ppOpts

1276+ iRenderResult (vsep (map (pprintPTerm ppOpts

12771277 []

12781278 []

12791279 (idris_infixes i))

@@ -1538,4 +1538,3 @@ replSettings :: Maybe FilePath -> Settings Idris

15381538replSettings hFile = setComplete replCompletion $ defaultSettings {

15391539 historyFile = hFile

15401540 }

1541−

src/Idris/REPL/Commands.hs+1

@@ -32,6 +32,7 @@ data Command = Quit

3232 | Universes

3333 | LogLvl Int

3434 | LogCategory [LogCat]

35+ | Verbosity Int

3536 | Spec PTerm

3637 | WHNF PTerm

3738 | TestInline PTerm

src/Idris/REPL/Parser.hs+8−1

@@ -118,6 +118,7 @@ parserCommandsForHelp =

118118 , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg))

119119 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

120120 , cmd_pprint)

121+ , (["verbosity"], NumberArg, "Set verbosity level", cmd_verb)

121122 ]

122123 where optionsList = intercalate ", " $ map fst setOptions

123124

@@ -146,7 +147,7 @@ parserCommands =

146147 , proofArgCmd ["mc", "makecase"] MakeCase

147148 ":mc <line> <name> adds a case block for the definition of the metavariable on the line"

148149 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

149− , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

150+ , (["log"], NumberArg, "Set logging level", cmd_log)

150151 , ( ["logcats"]

151152 , ManyArgs NameArg

152153 , "Set logging categories"

@@ -405,6 +406,12 @@ cmd_log name = do

405406 eof

406407 return (Right (LogLvl i))

407408

409+cmd_verb :: String -> P.IdrisParser (Either String Command)

410+cmd_verb name = do

411+ i <- fmap (fromIntegral . fst) P.natural

412+ eof

413+ return (Right (Verbosity i))

414+

408415cmd_cats :: String -> P.IdrisParser (Either String Command)

409416cmd_cats name = do

410417 cs <- sepBy pLogCats (P.whiteSpace)