280810b · Idris-dev · git.iko.soy

CHANGELOG.md+8

compare with master

unifiedsplit

@@ -10,6 +10,14 @@

10 + `FirstClassReflection`, which must be enabled to define a `%reflection`

11 function

12

13+## Tool Updates

14+

15++ Output from verbose Idris 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+

20+

13## Library Updates

21## Library Updates

14

22

15+ Terminating programs has been improved with more appropriate

23+ Terminating programs has been improved with more appropriate

src/IRTS/Compiler.hs+4−2

@@ -53,7 +53,9 @@ import System.Process

53-- | Compile to simplified forms and return CodegenInfo

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

55compile codegen f mtm

56+ = do v <- verbose

57+ when v $ iputStrLn "Compiling Output."

56− = do checkMVs -- check for undefined metavariables

58+ checkMVs -- check for undefined metavariables

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

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

58 exports <- findExports

60 exports <- findExports

59 let rootNames = case mtm of

61 let rootNames = case mtm of

@@ -108,7 +110,7 @@ compile codegen f mtm

108 Just f -> runIO $ writeFile f (dumpDefuns defuns)

110 Just f -> runIO $ writeFile f (dumpDefuns defuns)

109 triple <- Idris.AbsSyntax.targetTriple

111 triple <- Idris.AbsSyntax.targetTriple

110 cpu <- Idris.AbsSyntax.targetCPU

112 cpu <- Idris.AbsSyntax.targetCPU

111− logCodeGen 1 "Building output"

113+ when v $ iputStrLn "Generating Code."

112 case checked of

114 case checked of

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

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

114 hdrs impdirs objs libs flags

116 hdrs impdirs objs libs flags

src/Idris/AbsSyntaxTree.hs+1−1

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

120 , opt_showimp = False

121 , opt_errContext = False

122 , opt_repl = True

123− , opt_verbose = True

123+ , opt_verbose = False

124 , opt_nobanner = False

125 , opt_quiet = False

126 , opt_codegen = Via IBCFormat "c"

src/Idris/IBC.hs+3−2

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

220

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

222writeIBC src f

223+ = do v <- verbose

223− = do logIBC 1 $ "Writing ibc " ++ show f

224+ when v $ iputStrLn $ "Writing IBC for: " ++ show f

224 i <- getIState

225 i <- getIState

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

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

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

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

@@ -313,7 +314,7 @@ ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of

313 _ -> ifail "IBC write failed"

314 _ -> ifail "IBC write failed"

314ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316−ibc i (IBCFlags n) f

317+ibc i (IBCFlags n) f

317 = case lookupCtxtExact n (idris_flags i) of

318 = case lookupCtxtExact n (idris_flags i) of

318 Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319 Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319 _ -> ifail "IBC write failed"

320 _ -> ifail "IBC write failed"

src/Idris/Parser.hs+2−2

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

1803 setContext ctxt')

1804 (map snd (idris_totcheck i))

1805 -- build size change graph from simplified definitions

1806− logLvl 1 "Totality checking"

1806+ when v $ iputStrLn $ "Totality checking " ++ f

1807 i <- getIState

1808 mapM_ buildSCG (idris_totcheck i)

1809 mapM_ checkDeclTotality (idris_totcheck i)

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

1826

1827 logLvl 1 ("Finished " ++ f)

1828 ibcsd <- valIBCSubDir i

1829− logLvl 1 "Universe checking"

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

1830 iucheck

1831 let ibc = ibcPathNoFallback ibcsd f

1832 i <- getIState

test/base001/expected+4

@@ -1,4 +1,8 @@

1Type checking ./base001.idr

2+Totality checking ./base001.idr

3+Writing IBC for: "./base001.ibc"

4+Compiling Output.

5+Generating Code.

2exit1: Executing cmd 'exit 1'

6exit1: Executing cmd 'exit 1'

3exit1: raw exitStatus = 256

7exit1: raw exitStatus = 256

4exit1: WEXITSTATUS(exitStatus) = 1

8exit1: WEXITSTATUS(exitStatus) = 1

test/pkg008/expected+7−1

@@ -1,10 +1,16 @@

1Entering directory `./src'

2Type checking ./NumOps.idr

3+Totality checking ./NumOps.idr

4+Writing IBC for: "./NumOps.ibc"

3Type checking ./Test.idr

5Type checking ./Test.idr

6+Totality checking ./Test.idr

7+Writing IBC for: "./Test.ibc"

4Leaving directory `./src'

8Leaving directory `./src'

9+Entering directory `./src'

10+Compiling Output.

11+Generating Code.

5Test Passed

12Test Passed

6Test Passed

13Test Passed

7−Entering directory `./src'

8Leaving directory `./src'

14Leaving directory `./src'

9Entering directory `./src'

15Entering directory `./src'

10Removed: NumOps.ibc

16Removed: NumOps.ibc