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

CHANGELOG.md+6−5

compare with master

unifiedsplit

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

12

13## Tool Updates

14

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

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

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

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

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

18− Compiling; and Code Generation.

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

19−

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

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

20+ persist.

20

21

21## Library Updates

22## Library Updates

22

23

docs/reference/compilation.rst+23−7

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

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

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

2−Compilation and Logging

2+Compilation, Logging, and Reporting

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

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

4

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

6provides 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

41

42Use 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.

43

44−Logging Output

44+Reporting Compilation Process

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

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

46

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

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

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

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

64+logging infrastructure has support for the following categories:

49

65

50+ Parser

66+ Parser

51+ Elaborator

67+ Elaborator

main/Main.hs+1−1

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

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

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

41 (c : _) -> do

42− setVerbose False

42+ setVerbose 0

43 setQuiet True

44 case getPort opts of

45 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.

68 --listlibs Display installed libraries

69 --libdir Display library directory

70 --include Display the includes flags

71+ --V2 Loudest verbosity

72+ --V1 Louder verbosity

71− -V,--verbose Loud verbosity

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

72 --ibcsubdir FILE Write IBC files into sub directory

74 --ibcsubdir FILE Write IBC files into sub directory

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

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

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

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

src/IRTS/Compiler.hs+4

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

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

55compile codegen f mtm = do

56 logCodeGen 1 "Compiling Output."

57+ iReport 2 "Compiling Output."

57 checkMVs -- check for undefined metavariables

58 checkMVs -- check for undefined metavariables

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

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

59 exports <- findExports

60 exports <- findExports

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

90 let ctxtIn = addAlist tagged emptyContext

91 let ctxtIn = addAlist tagged emptyContext

91

92

92 logCodeGen 1 "Defunctionalising"

93 logCodeGen 1 "Defunctionalising"

94+ iReport 3 "Defunctionalising"

93 let defuns_in = defunctionalise nexttag ctxtIn

95 let defuns_in = defunctionalise nexttag ctxtIn

94 logCodeGen 5 $ show defuns_in

96 logCodeGen 5 $ show defuns_in

95 logCodeGen 1 "Inlining"

97 logCodeGen 1 "Inlining"

98+ iReport 3 "Inlining"

96 let defuns = inline defuns_in

99 let defuns = inline defuns_in

97 logCodeGen 5 $ show defuns

100 logCodeGen 5 $ show defuns

98 logCodeGen 1 "Resolving variables for CG"

101 logCodeGen 1 "Resolving variables for CG"

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

110 triple <- Idris.AbsSyntax.targetTriple

113 triple <- Idris.AbsSyntax.targetTriple

111 cpu <- Idris.AbsSyntax.targetCPU

114 cpu <- Idris.AbsSyntax.targetCPU

112 logCodeGen 1 "Generating Code."

115 logCodeGen 1 "Generating Code."

116+ iReport 2 "Generating Code."

113 case checked of

117 case checked of

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

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

115 hdrs impdirs objs libs flags

119 hdrs impdirs objs libs flags

src/Idris/AbsSyntax.hs+25−11

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

385 case getCGAllNames i n of

386 Just ns -> return ns

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

388− Just ci ->

388+ Just ci ->

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

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

391 addCGAllNames i n ns'

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

1024targetCPU = do i <- getIState

1025 return (opt_cpu (idris_options i))

1026

1027−verbose :: Idris Bool

1027+verbose :: Idris Int

1028+verbose = do

1028−verbose = do i <- getIState

1029+ i <- getIState

1029− -- Quietness overrides verbosity

1030+ -- Quietness overrides verbosity

1031+ let quiet = opt_quiet $ idris_options i

1032+ if quiet

1033+ then return $ 0

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

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

1031− opt_verbose (idris_options i))

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

1041+ putIState $ i { idris_options = opt' }

1032

1042

1033−setVerbose :: Bool -> Idris ()

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

1044+iReport level msg = do

1045+ verbosity <- verbose

1034−setVerbose t = do i <- getIState

1046+ i <- getIState

1035− let opts = idris_options i

1047+ when (level <= verbosity) $

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

1048+ case idris_outputmode i of

1037− putIState $ i { idris_options = opt' }

1049+ RawOutput h -> runIO $ hPutStrLn h msg

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

1051+ return ()

1038

1052

1039typeInType :: Idris Bool

1053typeInType :: Idris Bool

1040typeInType = do i <- getIState

1054typeInType = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4−4

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

91 , opt_showimp :: Bool -- ^ show implicits

92 , opt_errContext :: Bool

93 , opt_repl :: Bool

94− , opt_verbose :: Bool

94+ , opt_verbose :: Int

95 , opt_nobanner :: Bool

96 , opt_quiet :: Bool

97 , opt_codegen :: Codegen

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

120 , opt_showimp = False

121 , opt_errContext = False

122 , opt_repl = True

123− , opt_verbose = False

123+ , opt_verbose = 0

124 , opt_nobanner = False

125 , opt_quiet = False

126 , opt_codegen = Via IBCFormat "c"

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

512 | NoCoverage

513 | ErrContext

514 | ShowImpl

515− | Verbose

515+ | Verbose Int

516 | Port REPLPort -- ^ REPL TCP port

517 | IBCSubDir String

518 | ImportDir String

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

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

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

2474 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;

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

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

2478 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 $

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

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

136

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

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

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

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

138

140

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

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

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

142 <|> (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

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

222writeIBC src f

223 = 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

225 i <- getIState

226 i <- getIState

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

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

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

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

src/Idris/Main.hs+5−2

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

68 let nobanner = NoBanner `elem` opts

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

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

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

72 let output = opt getOutput opts

71 let output = opt getOutput opts

73 let ibcsubdir = opt getIBCSubDir opts

72 let ibcsubdir = opt getIBCSubDir opts

74 let importdirs = opt getImportDir opts

73 let importdirs = opt getImportDir opts

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

116 mapM_ addLangExt (opt getLanguageExt opts)

115 mapM_ addLangExt (opt getLanguageExt opts)

117 setREPL runrepl

116 setREPL runrepl

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

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

119− setVerbose verbose

118+

120 setCmdLine opts

119 setCmdLine opts

121 setOutputTy outty

120 setOutputTy outty

122 setNoBanner nobanner

121 setNoBanner nobanner

123 setCodegen cgn

122 setCodegen cgn

124 mapM_ (addFlag cgn) cgFlags

123 mapM_ (addFlag cgn) cgFlags

125 mapM_ makeOption opts

124 mapM_ makeOption opts

125+ vlevel <- verbose

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

127+

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

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

127 case bcs of

129 case bcs of

128 [] -> return ()

130 [] -> return ()

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

215 where

217 where

216 makeOption (OLogging i) = setLogLevel i

218 makeOption (OLogging i) = setLogLevel i

217 makeOption (OLogCats cs) = setLogCats cs

219 makeOption (OLogCats cs) = setLogCats cs

220+ makeOption (Verbose v) = setVerbose v

218 makeOption TypeCase = setTypeCase True

221 makeOption TypeCase = setTypeCase True

219 makeOption TypeInType = setTypeInType True

222 makeOption TypeInType = setTypeInType True

220 makeOption NoCoverage = setCoverage False

223 makeOption NoCoverage = setCoverage False

src/Idris/Package.hs+6−5

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

71 make (makefile pkgdesc)

72 case (execout pkgdesc) of

73 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

75 Left emsg -> do

76 putStrLn emsg

77 exitWith (ExitFailure 1)

78 Right opts -> buildMods opts (modules pkgdesc)

79 Just o -> do

80 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

82 Left emsg -> do

83 putStrLn emsg

84 exitWith (ExitFailure 1)

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

115 res <- inPkgDir pkgdesc $ do

116 make (makefile pkgdesc)

117

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

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

119 Left emsg -> do

120 putStrLn emsg

121 exitWith (ExitFailure 1)

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

195 cd <- getCurrentDirectory

196 let pkgDir = cd </> takeDirectory fp

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

198− popts = NoREPL : Verbose : idris_opts pkgdesc

198+ popts = NoREPL : Verbose 1 : idris_opts pkgdesc

199 mods = modules pkgdesc

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

201 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

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

259 hClose tmph

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

261 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)

263 case mergeOptions copts popts of

264 Left emsg -> do

265 putStrLn emsg

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

442 chkOpt o@(IBCSubDir _) = Right o

443 chkOpt o@(ImportDir _ ) = Right o

444 chkOpt o@(UseCodegen _) = Right o

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

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

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

446

447

447 genErrMsg :: [String] -> String

448 genErrMsg :: [String] -> String

src/Idris/Parser.hs+5−3

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

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

1701loadSource lidr f toline

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

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

1703 i <- getIState

1704 i <- getIState

1704 let def_total = default_total i

1705 let def_total = default_total i

1705 file_in <- runIO $ readSource f

1706 file_in <- runIO $ readSource f

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

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

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

1788 logLvl 3 (show (idris_infixes i))

1789 logLvl 3 (show (idris_infixes i))

1789 -- Now add all the declarations to the context

1790 -- Now add all the declarations to the context

1790− v <- verbose

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

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

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

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

1794 -- mutual block on its own

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

1803 setContext ctxt')

1804 (map snd (idris_totcheck i))

1805 -- build size change graph from simplified definitions

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

1806 logLvl 1 $ "Totality checking " ++ f

1807 logLvl 1 $ "Totality checking " ++ f

1807 i <- getIState

1808 i <- getIState

1808 mapM_ buildSCG (idris_totcheck i)

1809 mapM_ buildSCG (idris_totcheck i)

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

1826

1827

1827 logLvl 1 ("Finished " ++ f)

1828 logLvl 1 ("Finished " ++ f)

1828 ibcsd <- valIBCSubDir i

1829 ibcsd <- valIBCSubDir i

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

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

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

1830 iucheck

1832 iucheck

1831 let ibc = ibcPathNoFallback ibcsd f

1833 let ibc = ibcPathNoFallback ibcsd f

1832 i <- getIState

1834 i <- getIState

src/Idris/REPL.hs+2−3

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

194 setErrContext True

195 setOutH h

196 setQuiet True

197− setVerbose False

197+ setVerbose 0

198 mods <- loadInputs [f] toline

199 ist <- getIState

200 return (ist, f)

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

1273 case lookupCtxt n (idris_patdefs i) of

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

1275 [(_, tms)] ->

1276− iRenderResult (vsep (map (pprintPTerm ppOpts

1276+ iRenderResult (vsep (map (pprintPTerm ppOpts

1277 []

1278 []

1279 (idris_infixes i))

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

1538replSettings hFile = setComplete replCompletion $ defaultSettings {

1539 historyFile = hFile

1540 }

1541−

src/Idris/REPL/Commands.hs+1

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

32 | Universes

33 | LogLvl Int

34 | LogCategory [LogCat]

35+ | Verbosity Int

35 | Spec PTerm

36 | Spec PTerm

36 | WHNF PTerm

37 | WHNF PTerm

37 | TestInline PTerm

38 | TestInline PTerm

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

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

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

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

120 , cmd_pprint)

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

121 ]

122 ]

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

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

123

124

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

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

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

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

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

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

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

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

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

150 , ( ["logcats"]

151 , ( ["logcats"]

151 , ManyArgs NameArg

152 , ManyArgs NameArg

152 , "Set logging categories"

153 , "Set logging categories"

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

405 eof

406 eof

406 return (Right (LogLvl i))

407 return (Right (LogLvl i))

407

408

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+

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

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

409cmd_cats name = do

416cmd_cats name = do

410 cs <- sepBy pLogCats (P.whiteSpace)

417 cs <- sepBy pLogCats (P.whiteSpace)