~cypheon/Idris2

37ec2e921a4745d744589ffd89d8057231775895 — Johann Rudloff 20 days ago 0101db9 + 3095c09
Merge remote-tracking branch 'cypheon/fix-refc-clocks-per-nsec'
M .github/workflows/ci-macos-combined.yml => .github/workflows/ci-macos-combined.yml +1 -1
@@ 56,7 56,7 @@ jobs:
          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
          chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
      - name: Build self-hosted
        run: make all && make install
        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
        shell: bash
      - name: Test self-hosted
        run: make test INTERACTIVE=''

M .github/workflows/ci-ubuntu-combined.yml => .github/workflows/ci-ubuntu-combined.yml +3 -3
@@ 122,7 122,7 @@ jobs:
          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
          chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
      - name: Build self-hosted
        run: make all && make install
        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
      - name: Test self-hosted
        run: make test INTERACTIVE=''



@@ 146,7 146,7 @@ jobs:
          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
          chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
      - name: Build self-hosted
        run: make all && make install
        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
      - name: Test self-hosted
        run: make test INTERACTIVE=''



@@ 172,7 172,7 @@ jobs:
      - name: Build from previous version
        run: make all && make install && make clean
      - name: Build self-hosted from previous version
        run: make all && make install
        run: make all IDRIS2_BOOT="idris2 -Werror" && make install
      - name: Test self-hosted from previous version
        run: make test INTERACTIVE=''
      - name: Artifact Idris2

M Makefile => Makefile +1 -0
@@ 89,6 89,7 @@ libdocs:
	${MAKE} -C libs/base docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/contrib docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/network docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/test docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

${TEST_PREFIX}/${NAME_VERSION} :
	${MAKE} install-support PREFIX=${TEST_PREFIX}

M idris2api.ipkg => idris2api.ipkg +0 -1
@@ 155,7 155,6 @@ modules =
    Libraries.Text.Token,

    Libraries.Utils.Binary,
    Libraries.Utils.Either,
    Libraries.Utils.Hex,
    Libraries.Utils.Octal,
    Libraries.Utils.Path,

M libs/base/base.ipkg => libs/base/base.ipkg +1 -1
@@ 1,7 1,7 @@
package base
version = 0.3.0

opts = "--ignore-missing-ipkg --no-shadowing-warning"
opts = "--ignore-missing-ipkg -Wno-shadowing"

modules = Control.App,
          Control.App.Console,

M libs/contrib/contrib.ipkg => libs/contrib/contrib.ipkg +1 -1
@@ 1,7 1,7 @@
package contrib
version = 0.3.0

opts = "--ignore-missing-ipkg --no-shadowing-warning"
opts = "--ignore-missing-ipkg -Wno-shadowing"

modules = Control.ANSI,
          Control.ANSI.SGR,

M libs/test/Makefile => libs/test/Makefile +3 -0
@@ 4,5 4,8 @@ all:
install:
	${IDRIS2} --install test.ipkg

docs:
	${IDRIS2} --mkdoc test.ipkg

clean:
	$(RM) -r build

M src/Compiler/ES/ES.idr => src/Compiler/ES/ES.idr +4 -0
@@ 481,6 481,10 @@ jsPrim (NS _ (UN "prim__os")) [] =
    pure sysos
jsPrim (NS _ (UN "void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"  -- DEPRECATED. TODO: remove when bootstrap has been updated
jsPrim (NS _ (UN "prim__void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"
jsPrim (NS _ (UN "prim__codegen")) [] = do
    (cg :: _) <- ccTypes <$> get ESs
        | _ => pure "\"javascript\""
    pure $ jsString cg
jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)

tag2es : Either Int String -> String

M src/Core/Context.idr => src/Core/Context.idr +3 -3
@@ 2574,8 2574,8 @@ setSession sopts
         put Ctxt (record { options->session = sopts } defs)

export
recordWarning : {auto c : Ref Ctxt Defs} ->
                Warning -> Core ()
recordWarning : {auto c : Ref Ctxt Defs} -> Warning -> Core ()
recordWarning w
    = do defs <- get Ctxt
         put Ctxt (record { warnings $= (w ::) } defs)
         session <- getSession
         put Ctxt $ record { warnings $= (w ::) } defs

M src/Core/Core.idr => src/Core/Core.idr +29 -13
@@ 59,6 59,13 @@ Pretty DotReason where
  pretty UnknownDot = reflow "Unknown reason"
  pretty UnderAppliedCon = reflow "Under-applied constructor"

public export
data Warning : Type where
     UnreachableClause : {vars : _} ->
                         FC -> Env Term vars -> Term vars -> Warning
     ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
     Deprecated : String -> Warning

-- All possible errors, carrying a location
public export
data Error : Type where


@@ 75,6 82,7 @@ data Error : Type where
                    FC -> Env Term vars -> Term vars -> Term vars -> Error -> Error
     ValidCase : {vars : _} ->
                 FC -> Env Term vars -> Either (Term vars) Error -> Error

     UndefinedName : FC -> Name -> Error
     InvisibleName : FC -> Name -> Maybe Namespace -> Error
     BadTypeConType : FC -> Name -> Error


@@ 155,13 163,7 @@ data Error : Type where
     InRHS : FC -> Name -> Error -> Error

     MaybeMisspelling : Error -> List1 String -> Error

public export
data Warning : Type where
     UnreachableClause : {vars : _} ->
                         FC -> Env Term vars -> Term vars -> Warning
     ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
     Deprecated : String -> Warning
     WarningAsError : Warning -> Error

export
Show TTCErrorMsg where


@@ 173,6 175,14 @@ Show TTCErrorMsg where

-- Simplest possible display - higher level languages should unelaborate names
-- and display annotations appropriately

export
Show Warning where
    show (UnreachableClause _ _ _) = ":Unreachable clause"
    show (ShadowingGlobalDefs _ _) = ":Shadowing names"
    show (Deprecated name) = ":Deprecated " ++ name


export
Show Error where
  show (Fatal err) = show err


@@ 339,6 349,14 @@ Show Error where
     = show err ++ "\nDid you mean" ++ case ns of
         (n ::: []) => ": " ++ n ++ "?"
         _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
  show (WarningAsError w) = show w

export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
getWarningLoc (Deprecated _) = Nothing

export
getErrorLoc : Error -> Maybe FC
getErrorLoc (Fatal err) = getErrorLoc err


@@ 409,12 427,7 @@ getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err
getErrorLoc (MaybeMisspelling err _) = getErrorLoc err

export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
getWarningLoc (Deprecated _) = Nothing
getErrorLoc (WarningAsError warn) = getWarningLoc warn

-- Core is a wrapper around IO that is specialised for efficiency.
export


@@ 563,6 576,8 @@ interface Catchable m t | m where
    throw : {0 a : Type} -> t -> m a
    catch : m a -> (t -> m a) -> m a

    breakpoint : m a -> m (Either t a)

export
Catchable Core Error where
  catch (MkCore prog) h


@@ 570,6 585,7 @@ Catchable Core Error where
                    case p' of
                         Left e => let MkCore he = h e in he
                         Right val => pure (Right val))
  breakpoint (MkCore prog) = MkCore (pure <$> prog)
  throw = coreFail

-- Prelude.Monad.foldlM hand specialised for Core

M src/Core/Options.idr => src/Core/Options.idr +3 -1
@@ 157,6 157,8 @@ record Session where
  dumpanf : Maybe String -- file to output ANF definitions
  dumpvmcode : Maybe String -- file to output VM code definitions
  profile : Bool -- generate profiling information, if supported
  -- Warnings
  warningsAsErrors : Bool
  showShadowingWarning : Bool

public export


@@ 206,7 208,7 @@ export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
                               False False False Nothing Nothing
                               Nothing Nothing False True
                               Nothing Nothing False False True

export
defaultElab : ElabDirectives

M src/Idris/CommandLine.idr => src/Idris/CommandLine.idr +5 -1
@@ 130,6 130,8 @@ data CLOpt
  Timing |
  DebugElabCheck |
  BlodwenPaths |
  ||| Treat warnings as errors
  WarningsAsErrors |
  ||| Do not print shadowing warnings
  IgnoreShadowingWarnings |
  ||| Generate bash completion info


@@ 216,7 218,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
              (Just "Generate profile data when compiling, if supported"),

           optSeparator,
           MkOpt ["--no-shadowing-warning"] [] [IgnoreShadowingWarnings]
           MkOpt ["-Werror"] [] [WarningsAsErrors]
              (Just "Treat warnings as errors"),
           MkOpt ["-Wno-shadowing"] [] [IgnoreShadowingWarnings]
              (Just "Do not print shadowing warnings"),

           optSeparator,

M src/Idris/Error.idr => src/Idris/Error.idr +22 -22
@@ 152,6 152,27 @@ ploc2 fc1 fc2 =
      snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs

export
pwarning : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           Warning -> Core (Doc IdrisAnn)
pwarning (UnreachableClause fc env tm)
    = pure $ errorDesc (reflow "Unreachable clause:"
        <++> code !(pshow env tm))
        <+> line <+> !(ploc fc)
pwarning (ShadowingGlobalDefs _ ns)
    = pure $ vcat
    $ reflow "We are about to implicitly bind the following lowercase names."
   :: reflow "You may be unintentionally shadowing the associated global definitions:"
   :: map (\ (n, ns) => indent 2 $ hsep $ pretty n
                            :: reflow "is shadowing"
                            :: punctuate comma (map pretty (forget ns)))
          (forget ns)

pwarning (Deprecated s)
    = pure $ pretty "Deprecation warning:" <++> pretty s

export
perror : {auto c : Ref Ctxt Defs} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto o : Ref ROpts REPLOpts} ->


@@ 467,28 488,7 @@ perror (MaybeMisspelling err ns) = pure $ !(perror err) <+> case ns of
       reflow "Did you mean any of:"
       <++> concatWith (surround (comma <+> space)) (map pretty xs)
       <+> comma <++> reflow "or" <++> pretty x <+> "?"


export
pwarning : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           Warning -> Core (Doc IdrisAnn)
pwarning (UnreachableClause fc env tm)
    = pure $ errorDesc (reflow "Unreachable clause:"
        <++> code !(pshow env tm))
        <+> line <+> !(ploc fc)
pwarning (ShadowingGlobalDefs _ ns)
    = pure $ vcat
    $ reflow "We are about to implicitly bind the following lowercase names."
   :: reflow "You may be unintentionally shadowing the associated global definitions:"
   :: map (\ (n, ns) => indent 2 $ hsep $ pretty n
                            :: reflow "is shadowing"
                            :: punctuate comma (map pretty (forget ns)))
          (forget ns)

pwarning (Deprecated s)
    = pure $ pretty "Deprecation warning:" <++> pretty s
perror (WarningAsError warn) = pwarning warn

prettyMaybeLoc : Maybe FC -> Doc IdrisAnn
prettyMaybeLoc Nothing = emptyDoc

M src/Idris/IDEMode/Parser.idr => src/Idris/IDEMode/Parser.idr +2 -3
@@ 18,7 18,6 @@ import Parser.Support
import Libraries.Text.Lexer
import Libraries.Text.Lexer.Tokenizer
import Libraries.Text.Parser
import Libraries.Utils.Either
import Libraries.Utils.String

%default total


@@ 81,8 80,8 @@ sexp
ideParser : {e : _} ->
            (fname : String) -> String -> Grammar SemanticDecorations Token e ty -> Either Error ty
ideParser fname str p
    = do toks   <- mapError (fromLexError fname) $ idelex str
         (decor, (parsed, _)) <- mapError (fromParsingError fname) $ parseWith p toks
    = do toks   <- mapFst (fromLexError fname) $ idelex str
         (decor, (parsed, _)) <- mapFst (fromParsingError fname) $ parseWith p toks
         Right parsed



M src/Idris/ModTree.idr => src/Idris/ModTree.idr +24 -20
@@ 20,12 20,13 @@ import Idris.Syntax
import Idris.Pretty

import Data.List
import Libraries.Data.StringMap
import Data.Either

import System.Directory
import System.File

import Libraries.Utils.Either
import Libraries.Data.StringMap
import Libraries.Data.String.Extra as String

%default covering



@@ 167,33 168,36 @@ buildMod loc num len mod
        -- since the imports have been built! But we still have to check.
        depFilesE <- traverse (nsToPath loc) (imports mod)
        let (ferrs, depFiles) = partitionEithers depFilesE
        ttcTime <- catch (do t <- fnameModified mttc
                             pure (Just t))
                         (\err => pure Nothing)

        ttcTime <- breakpoint (fnameModified mttc)
        srcTime <- fnameModified src
        depTimes <- traverse (\f => do t <- fnameModified f
                                       pure (f, t)) depFiles
        let needsBuilding =
               case ttcTime of
                    Nothing => True
                    Just t => any (\x => x > t) (srcTime :: map snd depTimes)
                    Left _ => True
                    Right t => any (\x => x > t) (srcTime :: map snd depTimes)
        u <- newRef UST initUState
        m <- newRef MD (initMetadata src)
        put Syn initSyntax

        if needsBuilding
           then do let msg : Doc IdrisAnn = pretty num <+> slash <+> pretty len <+> colon
                               <++> pretty "Building" <++> pretty mod.buildNS <++> parens (pretty src)
                   [] <- process {u} {m} msg src
                      | errs => do emitWarnings
                                   traverse_ emitError errs
                                   pure (ferrs ++ errs)
                   emitWarnings
                   traverse_ emitError ferrs
                   pure ferrs
           else do emitWarnings
                   traverse_ emitError ferrs
                   pure ferrs
        errs <- if (not needsBuilding) then pure [] else
           do let pad = minus (length $ show len) (length $ show num)
              let msg : Doc IdrisAnn
                  = pretty num <+> pretty (String.replicate pad ' ')
                    <+> slash <+> pretty len <+> colon
                    <++> pretty "Building" <++> pretty mod.buildNS
                    <++> parens (pretty src)
              process {u} {m} msg src

        defs <- get Ctxt
        ws <- emitWarningsAndErrors (if null errs then ferrs else errs)
        pure (ws ++ if null errs then ferrs else ferrs ++ errs)
  where
    isModuleNotFound : Error -> Bool
    isModuleNotFound e = case e of
      (ModuleNotFound _ _) => True
      _ => False

buildMods : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->

M src/Idris/Package.idr => src/Idris/Package.idr +1 -0
@@ 658,6 658,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
    optType (Directive d)    = POpt
    optType (BuildDir f)     = POpt
    optType (OutputDir f)    = POpt
    optType WarningsAsErrors = POpt
    optType (ConsoleWidth n) = PIgnore
    optType (Color b)        = PIgnore
    optType NoBanner         = PIgnore

M src/Idris/REPL/Common.idr => src/Idris/REPL/Common.idr +24 -10
@@ 93,13 93,6 @@ emitProblem a replDocCreator idemodeDocCreator getFC
    addOne : (Int, Int) -> (Int, Int)
    addOne (l, c) = (l + 1, c + 1)

export
emitWarning : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Warning -> Core ()
emitWarning w = emitProblem w displayWarning pwarning getWarningLoc

-- Display an error message from checking a source file
export
emitError : {auto c : Ref Ctxt Defs} ->


@@ 109,14 102,35 @@ emitError : {auto c : Ref Ctxt Defs} ->
emitError e = emitProblem e display perror getErrorLoc

export
emitWarning : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Warning -> Core ()
emitWarning w = emitProblem w displayWarning pwarning getWarningLoc

export
emitWarnings : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Core ()
               Core (List Error)
emitWarnings
    = do defs <- get Ctxt
         traverse_ emitWarning (reverse (warnings defs))
         put Ctxt (record { warnings = [] } defs)
         let ws = reverse (warnings defs)
         session <- getSession
         if (session.warningsAsErrors)
           then let errs = WarningAsError <$> ws in
                errs <$ traverse_ emitError errs
           else [] <$ traverse_ emitWarning ws

export
emitWarningsAndErrors : {auto c : Ref Ctxt Defs} ->
                        {auto o : Ref ROpts REPLOpts} ->
                        {auto s : Ref Syn SyntaxInfo} ->
                        List Error -> Core (List Error)
emitWarningsAndErrors errs = do
  ws <- emitWarnings
  traverse_ emitError errs
  pure ws

getFCLine : FC -> Maybe Int
getFCLine = map startLine . isNonEmptyFC

M src/Idris/SetOptions.idr => src/Idris/SetOptions.idr +3 -0
@@ 340,6 340,9 @@ preOptions (ConsoleWidth n :: opts)
preOptions (Color b :: opts)
    = do setColor b
         preOptions opts
preOptions (WarningsAsErrors :: opts)
    = do setSession (record { warningsAsErrors = True } !getSession)
         preOptions opts
preOptions (IgnoreShadowingWarnings :: opts)
    = do setSession (record { showShadowingWarning = False } !getSession)
         preOptions opts

D src/Libraries/Utils/Either.idr => src/Libraries/Utils/Either.idr +0 -17
@@ 1,17 0,0 @@
module Libraries.Utils.Either

%default total

export
mapError : (a -> c) -> Either a b -> Either c b
mapError f e = either (Left . f) (Right . id) e

export
partitionEithers : List (Either a b) -> (List a, List b)
partitionEithers [] = ([], [])
partitionEithers (Left x :: es)
        = let (ls, rs) = partitionEithers es in
              (x :: ls, rs)
partitionEithers (Right y :: es)
        = let (ls, rs) = partitionEithers es in
              (ls, y :: rs)

M src/Parser/Package.idr => src/Parser/Package.idr +3 -3
@@ 7,16 7,16 @@ import public Libraries.Text.Parser
import public Parser.Support

import Core.Core

import System.File
import Libraries.Utils.Either

%default total

export
runParser : (fname : String) -> String -> Rule ty -> Either Error ty
runParser fname str p
    = do toks   <- mapError (\err => fromLexError fname (NoRuleApply, err)) $ lex str
         parsed <- mapError (fromParsingError fname) $ parse p toks
    = do toks   <- mapFst (\err => fromLexError fname (NoRuleApply, err)) $ lex str
         parsed <- mapFst (fromParsingError fname) $ parse p toks
         Right (fst parsed)

export

M src/Parser/Source.idr => src/Parser/Source.idr +4 -4
@@ 8,8 8,8 @@ import Core.Core
import Core.Name
import Core.Metadata
import Core.FC

import System.File
import Libraries.Utils.Either

%default total



@@ 19,9 19,9 @@ runParserTo : {e : _} ->
              Maybe LiterateStyle -> Lexer ->
              String -> Grammar SemanticDecorations Token e ty -> Either Error (SemanticDecorations, ty)
runParserTo fname lit reject str p
    = do str    <- mapError (fromLitError fname) $ unlit lit str
         toks   <- mapError (fromLexError fname) $ lexTo reject str
         (decs, (parsed, _)) <- mapError (fromParsingError fname) $ parseWith p toks
    = do str    <- mapFst (fromLitError fname) $ unlit lit str
         toks   <- mapFst (fromLexError fname) $ lexTo reject str
         (decs, (parsed, _)) <- mapFst (fromParsingError fname) $ parseWith p toks
         Right (decs, parsed)

export

M src/TTImp/Utils.idr => src/TTImp/Utils.idr +8 -1
@@ 80,7 80,14 @@ findUniqueBindableNames fc arg env used t
            let ctxt = gamma defs
            ns <- map catMaybes $ for assoc $ \ (n, _) => do
                    ns <- lookupCtxtName (UN n) ctxt
                    pure $ MkPair n . map fst <$> Lib.fromList ns
                    let ns = flip mapMaybe ns $ \(n, _, d) =>
                               case definition d of
                                -- do not warn about holes: `?a` is not actually
                                -- getting shadowed as it will not become a
                                -- toplevel declaration
                                 Hole _ _ => Nothing
                                 _ => pure n
                    pure $ MkPair n <$> Lib.fromList ns
            whenJust (Lib.fromList ns) $ recordWarning . ShadowingGlobalDefs fc
       pure assoc


M support/refc/clock.c => support/refc/clock.c +1 -1
@@ 1,7 1,7 @@
#include "clock.h"

#define NSEC_PER_SEC 1000000000
#define CLOCKS_PER_NSEC ((float)(CLOCKS_PER_SEC / NSEC_PER_SEC))
#define CLOCKS_PER_NSEC ((float)CLOCKS_PER_SEC / NSEC_PER_SEC)

Value *clockTimeMonotonic()
{

M tests/Main.idr => tests/Main.idr +1 -12
@@ 1,16 1,5 @@
module Main

import Data.Maybe
import Data.List
import Data.List1
import Data.Strings

import System
import System.Directory
import System.File
import System.Info
import System.Path

import Test.Golden

%default covering


@@ 73,7 62,7 @@ idrisTestsError = MkTestPool "Error messages" []
      ["error001", "error002", "error003", "error004", "error005",
       "error006", "error007", "error008", "error009", "error010",
       "error011", "error012", "error013", "error014", "error015",
       "error016", "error017", "error018",
       "error016", "error017", "error018", "error019",
       -- Parse errors
       "perror001", "perror002", "perror003", "perror004", "perror005",
       "perror006", "perror007", "perror008"]

A tests/idris2/error019/Error.idr => tests/idris2/error019/Error.idr +5 -0
@@ 0,0 1,5 @@
some : Bool -> Bool
some True = True
some False = True
some False = True
some False = False

A tests/idris2/error019/expected => tests/idris2/error019/expected +20 -0
@@ 0,0 1,20 @@
1/1: Building Error (Error.idr)
Error: Unreachable clause: some False

Error.idr:4:1--4:11
 1 | some : Bool -> Bool
 2 | some True = True
 3 | some False = True
 4 | some False = True
     ^^^^^^^^^^

Error: Unreachable clause: some False

Error.idr:5:1--5:11
 1 | some : Bool -> Bool
 2 | some True = True
 3 | some False = True
 4 | some False = True
 5 | some False = False
     ^^^^^^^^^^


A tests/idris2/error019/run => tests/idris2/error019/run +3 -0
@@ 0,0 1,3 @@
$1 --no-color --console-width 0 --no-banner -Werror --check Error.idr

rm -rf build/

A tests/idris2/warning001/Holes.idr => tests/idris2/warning001/Holes.idr +10 -0
@@ 0,0 1,10 @@
test : List Nat -> List Nat
test [] = []
test (n :: ns) = ?n :: ns

replicate : (n : Nat) -> a -> List a
replicate Z a = []
replicate (S n) a = a :: replicate n a

testReplicate : test (replicate (1+n) k) === replicate (2+n) k
testReplicate = ?goal

M tests/idris2/warning001/expected => tests/idris2/warning001/expected +1 -0
@@ 19,3 19,4 @@ You may be unintentionally shadowing the associated global definitions:
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  g is shadowing Main.g
1/1: Building Holes (Holes.idr)

M tests/idris2/warning001/run => tests/idris2/warning001/run +1 -0
@@ 2,5 2,6 @@ $1 --no-color --console-width 0 --check Issue539.idr
$1 --no-color --console-width 0 --check Issue621.idr
$1 --no-color --console-width 0 --check Issue1401.idr
$1 --no-color --console-width 0 --check PR1407.idr
$1 --no-color --console-width 0 --check Holes.idr

rm -rf build

M tests/typedd-book/chapter04/expected => tests/typedd-book/chapter04/expected +9 -9
@@ 1,4 1,4 @@
1/12: Building BSTree (BSTree.idr)
1 /12: Building BSTree (BSTree.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Prelude.Types.elem


@@ 8,13 8,13 @@ You may be unintentionally shadowing the associated global definitions:
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Prelude.Types.elem
2/12: Building DataStore (DataStore.idr)
3/12: Building Direction (Direction.idr)
4/12: Building Generic (Generic.idr)
5/12: Building Picture (Picture.idr)
6/12: Building Shape (Shape.idr)
7/12: Building SumInputs (SumInputs.idr)
8/12: Building Tree (Tree.idr)
2 /12: Building DataStore (DataStore.idr)
3 /12: Building Direction (Direction.idr)
4 /12: Building Generic (Generic.idr)
5 /12: Building Picture (Picture.idr)
6 /12: Building Shape (Shape.idr)
7 /12: Building SumInputs (SumInputs.idr)
8 /12: Building Tree (Tree.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Prelude.Types.elem


@@ 24,7 24,7 @@ You may be unintentionally shadowing the associated global definitions:
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Prelude.Types.elem
9/12: Building TryIndex (TryIndex.idr)
9 /12: Building TryIndex (TryIndex.idr)
10/12: Building Vect (Vect.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:

M tests/typedd-book/chapter08/expected => tests/typedd-book/chapter08/expected +9 -9
@@ 1,4 1,4 @@
1/10: Building AppendVec (AppendVec.idr)
1 /10: Building AppendVec (AppendVec.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Data.Vect.elem, Prelude.Types.elem


@@ 8,12 8,12 @@ You may be unintentionally shadowing the associated global definitions:
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Data.Vect.elem, Prelude.Types.elem
2/10: Building CheckEqDec (CheckEqDec.idr)
3/10: Building CheckEqMaybe (CheckEqMaybe.idr)
4/10: Building EqNat (EqNat.idr)
5/10: Building ExactLength (ExactLength.idr)
6/10: Building ExactLengthDec (ExactLengthDec.idr)
7/10: Building ReverseVec (ReverseVec.idr)
8/10: Building TCVects (TCVects.idr)
9/10: Building Void (Void.idr)
2 /10: Building CheckEqDec (CheckEqDec.idr)
3 /10: Building CheckEqMaybe (CheckEqMaybe.idr)
4 /10: Building EqNat (EqNat.idr)
5 /10: Building ExactLength (ExactLength.idr)
6 /10: Building ExactLengthDec (ExactLengthDec.idr)
7 /10: Building ReverseVec (ReverseVec.idr)
8 /10: Building TCVects (TCVects.idr)
9 /10: Building Void (Void.idr)
10/10: Building All (All.idr)

M tests/typedd-book/chapter10/expected => tests/typedd-book/chapter10/expected +9 -9
@@ 7,15 7,15 @@ DLFail.idr:3:23--3:25
 3 | describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs
                           ^^

1/13: Building DataStore (DataStore.idr)
2/13: Building DescribeList (DescribeList.idr)
3/13: Building DescribeList2 (DescribeList2.idr)
4/13: Building IsSuffix (IsSuffix.idr)
5/13: Building MergeSort (MergeSort.idr)
6/13: Building MergeSortView (MergeSortView.idr)
7/13: Building Reverse (Reverse.idr)
8/13: Building ReverseSnoc (ReverseSnoc.idr)
9/13: Building Shape (Shape.idr)
1 /13: Building DataStore (DataStore.idr)
2 /13: Building DescribeList (DescribeList.idr)
3 /13: Building DescribeList2 (DescribeList2.idr)
4 /13: Building IsSuffix (IsSuffix.idr)
5 /13: Building MergeSort (MergeSort.idr)
6 /13: Building MergeSortView (MergeSortView.idr)
7 /13: Building Reverse (Reverse.idr)
8 /13: Building ReverseSnoc (ReverseSnoc.idr)
9 /13: Building Shape (Shape.idr)
10/13: Building Shape_abs (Shape_abs.idr)
11/13: Building SnocList (SnocList.idr)
12/13: Building TestStore (TestStore.idr)

M tests/typedd-book/chapter11/expected => tests/typedd-book/chapter11/expected +9 -9
@@ 1,15 1,15 @@
1/12: Building Arith (Arith.idr)
2/12: Building ArithCmd (ArithCmd.idr)
3/12: Building ArithCmdDo (ArithCmdDo.idr)
4/12: Building ArithTotal (ArithTotal.idr)
5/12: Building Greet (Greet.idr)
6/12: Building InfIO (InfIO.idr)
7/12: Building InfList (InfList.idr)
1 /12: Building Arith (Arith.idr)
2 /12: Building ArithCmd (ArithCmd.idr)
3 /12: Building ArithCmdDo (ArithCmdDo.idr)
4 /12: Building ArithTotal (ArithTotal.idr)
5 /12: Building Greet (Greet.idr)
6 /12: Building InfIO (InfIO.idr)
7 /12: Building InfList (InfList.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  elem is shadowing Prelude.Types.elem
8/12: Building Label (Label.idr)
9/12: Building RunIO (RunIO.idr)
8 /12: Building Label (Label.idr)
9 /12: Building RunIO (RunIO.idr)
10/12: Building Streams (Streams.idr)
11/12: Building StreamFail (StreamFail.idr)
12/12: Building All (All.idr)

M tests/typedd-book/chapter12/expected => tests/typedd-book/chapter12/expected +9 -9
@@ 1,5 1,5 @@
1/10: Building ArithState (ArithState.idr)
2/10: Building DataStore (DataStore.idr)
1 /10: Building ArithState (ArithState.idr)
2 /10: Building DataStore (DataStore.idr)
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  schema is shadowing Main.DataStore.schema


@@ 12,11 12,11 @@ You may be unintentionally shadowing the associated global definitions:
Warning: We are about to implicitly bind the following lowercase names.
You may be unintentionally shadowing the associated global definitions:
  schema is shadowing Main.DataStore.schema
3/10: Building Record (Record.idr)
4/10: Building State (State.idr)
5/10: Building StateMonad (StateMonad.idr)
6/10: Building Traverse (Traverse.idr)
7/10: Building TreeLabel (TreeLabel.idr)
8/10: Building TreeLabelState (TreeLabelState.idr)
9/10: Building TreeLabelType (TreeLabelType.idr)
3 /10: Building Record (Record.idr)
4 /10: Building State (State.idr)
5 /10: Building StateMonad (StateMonad.idr)
6 /10: Building Traverse (Traverse.idr)
7 /10: Building TreeLabel (TreeLabel.idr)
8 /10: Building TreeLabelState (TreeLabelState.idr)
9 /10: Building TreeLabelType (TreeLabelType.idr)
10/10: Building All (All.idr)