diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,11 +25,17 @@ * The File Effect has been updated to take into account changes in `Prelude.File` and to provide a 'better' API. +* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges. ## Tool updates * Idris' documentation system now displays the documentation for auto implicits in the output of `:doc`. This is tested for in `docs005`. + +## Miscellaneous updates + +* The test suite now uses [tasty-golden](https://hackage.haskell.org/package/tasty-golden). New tests must be registered in `test/TestData.hs`, as explained in the relevant `README.md`. +* Added OSX and Windows continous integration with Travis and Appveyor. # New in 0.12: diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -1,11 +1,18 @@ -.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs +.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_js test_c test test_clean lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs +ARGS= +TEST-JOBS= +TEST-ARGS= + include config.mk -include custom.mk ifdef CI CABALFLAGS += -f CI +ifndef APPVEYOR +TEST-ARGS += --color always endif +endif install: $(CABAL) install $(CABALFLAGS) @@ -20,13 +27,20 @@ test: doc test_c test_c: - $(MAKE) -C test IDRIS=../dist/build/idris/idris test + $(CABAL) test $(ARGS) --test-options \ + "$(TEST-ARGS) --rerun-update +RTS -N$(TEST-JOBS) -RTS" test_js: - $(MAKE) -C test IDRIS=../dist/build/idris/idris test_js + $(CABAL) test $(ARGS) --test-options \ + "$(TEST-ARGS) --node --rerun-update +RTS -N$(TEST-JOBS) -RTS" -test_timed: - $(MAKE) -C test IDRIS=../dist/build/idris/idris time +test_update: + $(CABAL) test $(ARGS) --test-options \ + "$(TEST-ARGS) --accept +RTS -N$(TEST-JOBS) -RTS" + +test_clean: + rm -f test/*~ + rm -f test/*/output lib_clean: $(MAKE) -C libs IDRIS=../../dist/build/idris/idris RTS=../../dist/build/rts/libidris_rts clean diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,8 +1,10 @@ # Idris [![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev) +[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev) [![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest) [![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris) + Idris (http://idris-lang.org/) is a general-purpose functional programming language with dependent types. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -264,6 +264,30 @@ make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local] -- ----------------------------------------------------------------------------- +-- Test + +-- FIXME: We use the __GLASGOW_HASKELL__ macro because MIN_VERSION_cabal seems +-- to be broken ! + +-- There are two "dataDir" in cabal, and they don't relate to each other. +-- When fetching modules, idris uses the second path (in the pkg record), +-- which by default is the root folder of the project. +-- We want it to be the install directory where we put the idris libraries. +fixPkg pkg target = pkg { dataDir = target } + +-- The "Args" argument of the testHooks has been added in cabal 1.22.0, +-- and should therefore be ignored for prior versions. +#if __GLASGOW_HASKELL__ < 710 +originalTestHook _ = testHook simpleUserHooks +#else +originalTestHook = testHook simpleUserHooks +#endif + +idrisTestHook args pkg local hooks flags = do + let target = datadir $ L.absoluteInstallDirs pkg local NoCopyDest + originalTestHook args (fixPkg pkg target) local hooks flags + +-- ----------------------------------------------------------------------------- -- Main -- Install libraries during both copy and install @@ -281,4 +305,9 @@ NoCopyDest pkg local , preSDist = idrisPreSDist , postSDist = idrisPostSDist +#if __GLASGOW_HASKELL__ < 710 + , testHook = idrisTestHook () +#else + , testHook = idrisTestHook +#endif } diff --git a/config.mk b/config.mk --- a/config.mk +++ b/config.mk @@ -14,9 +14,11 @@ # Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs CFLAGS :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS) -#CABALFLAGS := +# CABALFLAGS := +CABALFLAGS += --enable-tests ## Disable building of Effects -#CABALFLAGS :=-f NoEffects +#CABALFLAGS :=-f NoEffects $(CABALFLAGS) + ifneq (, $(findstring bsd, $(MACHINE))) GMP_INCLUDE_DIR := diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.12.1 +Version: 0.12.2 License: BSD3 License-file: LICENSE Author: Edwin Brady @@ -146,7 +146,7 @@ libs/effects/Makefile libs/effects/effects.ipkg libs/effects/Effect/*.idr - libs/effects/Effect/Logging/*.idr + libs/effects/Effect/Logging/*.idr libs/effects/*.idr libs/pruviloj/Makefile @@ -156,8 +156,8 @@ libs/pruviloj/Pruviloj/Derive/*.idr libs/pruviloj/Pruviloj/Internals/*.idr - test/Makefile - test/runtest.hs + test/TestRun.hs + test/TestData.hs test/regression001/run test/regression001/expected @@ -293,6 +293,15 @@ test/reg075/*.idr test/reg075/expected + test/base001/Makefile + test/base001/base001.idr + test/base001/base001.ipkg + test/base001/exit1.c + test/base001/expected + test/base001/run + test/base001/sys.c + test/base001/sys.h + test/basic001/run test/basic001/*.idr test/basic001/expected @@ -356,6 +365,10 @@ test/bignum002/*.idr test/bignum002/expected + test/bounded001/run + test/bounded001/*.idr + test/bounded001/expected + test/corecords001/*.idr test/corecords001/run test/corecords001/expected @@ -594,6 +607,10 @@ test/io003/*.idr test/io003/expected + test/layout001/expected + test/layout001/*.idr + test/layout001/run + test/literate001/run test/literate001/*.lidr test/literate001/expected @@ -604,10 +621,17 @@ test/meta002/run test/meta002/*.idr test/meta002/expected + test/meta003/run + test/meta003/*.idr + test/meta003/expected test/meta004/run test/meta004/*.idr test/meta004/expected + test/prelude001/expected + test/prelude001/prelude001.idr + test/prelude001/run + test/primitives001/run test/primitives001/*.idr test/primitives001/expected @@ -630,9 +654,27 @@ test/primitives006/expected test/pkg001/run - test/pkg001/test-pkg.ipkg test/pkg001/*.idr test/pkg001/expected + test/pkg001/*.ipkg + test/pkg002/run + test/pkg002/*.idr + test/pkg002/expected + test/pkg002/*.ipkg + test/pkg003/run + test/pkg003/*.idr + test/pkg003/expected + test/pkg003/*.ipkg + test/pkg004/run + test/pkg004/*.idr + test/pkg004/expected + test/pkg004/*.ipkg + test/pkg005/run + test/pkg005/expected + test/pkg005/*.ipkg + test/pkg006/run + test/pkg006/expected + test/pkg006/*.ipkg test/proof001/run test/proof001/*.idr @@ -1023,7 +1065,9 @@ , IRTS.Simplified , IRTS.System - , Pkg.Package + , Idris.Package + , Idris.Package.Common + , Util.DynamicLinker , Util.ScreenSize , Util.System @@ -1032,7 +1076,7 @@ Util.Pretty , Util.Net - , Pkg.PParser + , Idris.Package.Parser -- Auto Generated , Paths_idris @@ -1137,9 +1181,10 @@ ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields -Test-suite regression-and-sanity-tests +Test-suite regression-and-feature-tests Type: exitcode-stdio-1.0 - Main-is: runtest.hs + Main-is: TestRun.hs + Other-modules: TestData hs-source-dirs: test Build-depends: idris @@ -1150,7 +1195,16 @@ , filepath , directory , haskeline >= 0.7 + , optparse-applicative >= 0.11 && < 0.13 + , tagged + , tasty >= 0.8 + , tasty-golden >= 2.0 + , tasty-rerun >= 1.0.0 + , bytestring , transformers + if impl(ghc < 7.10) + Extensions: DeriveDataTypeable + ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -146,12 +146,18 @@ -- predefine Nat versions of Enum, so we can use them in the default impls total natEnumFromThen : Nat -> Nat -> Stream Nat -natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc +natEnumFromThen n next = n :: natEnumFromThen next (minus next n) total natEnumFromTo : Nat -> Nat -> List Nat -natEnumFromTo n m = map (plus n) (natRange (minus (S m) n)) +natEnumFromTo n m = if n <= m + then go n m + else List.reverse $ go m n + where go : Nat -> Nat -> List Nat + go n m = map (plus n) (natRange (minus (S m) n)) +total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat +natEnumFromThenTo' _ Z _ = [] +natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ))) total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat -natEnumFromThenTo _ Z _ = [] -natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ))) +natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m interface Enum a where total pred : a -> a @@ -184,36 +190,38 @@ fromNat n = cast n enumFromThen n inc = n :: enumFromThen (inc + n) inc enumFromTo n m = if n <= m - then go (natRange (S (cast {to = Nat} (m - n)))) - else [] - where go : List Nat -> List Integer - go [] = [] - go (x :: xs) = n + cast x :: go xs + then go n m + else List.reverse $ go m n + where go' : Integer -> List Nat -> List Integer + go' _ [] = [] + go' n (x :: xs) = n + cast x :: go' n xs + go : Integer -> Integer -> List Integer + go n m = go' n (natRange (S (cast {to = Nat} (m - n)))) enumFromThenTo _ 0 _ = [] - enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ))) + enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ))) where go : List Nat -> List Integer go [] = [] - go (x :: xs) = n + (cast x * inc) :: go xs + go (x :: xs) = n + (cast x * (next - n)) :: go xs Enum Int where pred n = n - 1 succ n = n + 1 toNat n = cast n fromNat n = cast n - enumFromTo n m = - if n <= m - then go [] (cast {to = Nat} (m - n)) m - else [] - where - go : List Int -> Nat -> Int -> List Int - go acc Z m = m :: acc - go acc (S k) m = go (m :: acc) k (m - 1) + enumFromTo n m = if n <= m + then go n m + else List.reverse $ go m n + where go' : List Int -> Nat -> Int -> List Int + go' acc Z m = m :: acc + go' acc (S k) m = go' (m :: acc) k (m - 1) + go : Int -> Int -> List Int + go n m = go' [] (cast {to = Nat} (m - n)) m enumFromThen n inc = n :: enumFromThen (inc + n) inc enumFromThenTo _ 0 _ = [] - enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ))) + enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ))) where go : List Nat -> List Int go [] = [] - go (x :: xs) = n + (cast x * inc) :: go xs + go (x :: xs) = n + (cast x * (next - n)) :: go xs Enum Char where toNat c = toNat (ord c) @@ -224,12 +232,12 @@ syntax "[" [start] ".." [end] "]" = enumFromTo start end syntax "[" [start] "," [next] ".." [end] "]" - = enumFromThenTo start (next - start) end + = enumFromThenTo start next end syntax "[" [start] ".." "]" = enumFrom start syntax "[" [start] "," [next] ".." "]" - = enumFromThen start (next - start) + = enumFromThen start next ---- More utilities diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -19,7 +19,7 @@ ||| Constant function. Ignores its second argument. const : a -> b -> a -const x = \v => x +const x = \value => x ||| Return the first element of a pair. fst : (a, b) -> a diff --git a/main/Main.hs b/main/Main.hs --- a/main/Main.hs +++ b/main/Main.hs @@ -10,11 +10,13 @@ import Idris.Error import Idris.CmdOptions +import Idris.Package + import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags ) import Util.System ( setupBundledCC ) -import Pkg.Package + -- Main program reads command line options, parses the main program, and gets -- on with the REPL. diff --git a/man/idris.1 b/man/idris.1 --- a/man/idris.1 +++ b/man/idris.1 @@ -1,6 +1,6 @@ .\" Manpage for Idris. .\" Contact <> to correct errors or typos. -.TH man 1 "25 March 2016" "0.12" "Idris man page" +.TH man 1 "25 March 2016" "0.12.2" "Idris man page" .SH NAME idris -\ a general purpose pure functional programming language with dependent types. .SH SYNOPSIS diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -1994,8 +1994,9 @@ else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs)) prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a prettySe d p bnd (PCase _ scr cases) = - align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$> - depth d (indent 2 (vsep (map ppcase cases))) + bracket p funcAppPrec $ + align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$> + depth d (indent 2 (vsep (map ppcase cases))) where ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec ([(n, False) | n <- vars l] ++ bnd) @@ -2255,6 +2256,7 @@ -> Doc OutputAnnotation prettyName infixParen showNS bnd n | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_" + | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_" | (UN n') <- n, T.unpack n' == "_" = text "_" | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs --- a/src/Idris/Core/Evaluate.hs +++ b/src/Idris/Core/Evaluate.hs @@ -636,6 +636,15 @@ ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t') ceqB ps b b' = ceq ps (binderTy b) (binderTy b') + -- Special case for 'case' blocks - size of scope causes complications, + -- we only want to check the blocks themselves are valid and identical + -- in the current scope. So, just check the bodies, and the additional + -- arguments the case blocks are applied to. + ceq ps x@(App _ _ _) y@(App _ _ _) + | (P _ cx _, xargs) <- unApply x, + (P _ cy _, yargs) <- unApply y, + caseName cx && caseName cy = sameCase ps cx cy xargs yargs + ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay) ceq ps (Constant x) (Constant y) = return (x == y) ceq ps (TType x) (TType y) | x == y = return True @@ -677,6 +686,24 @@ (_, ydef) = cases_compiletime yd in caseeq ((x,y):ps) xdef ydef _ -> return False + + sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] -> + StateT UCs TC Bool + sameCase ps x y xargs yargs + = case (lookupDef x ctxt, lookupDef y ctxt) of + ([Function _ xdef], [Function _ ydef]) + -> ceq ((x,y):ps) xdef ydef + ([CaseOp _ _ _ _ _ xd], + [CaseOp _ _ _ _ _ yd]) + -> let (xin, xdef) = cases_compiletime xd + (yin, ydef) = cases_compiletime yd in + do liftM2 (&&) + (do ok <- zipWithM (ceq ps) + (drop (length xin) xargs) + (drop (length yin) yargs) + return (and ok)) + (caseeq ((x,y):ps) xdef ydef) + _ -> return False -- SPECIALISATION ----------------------------------------------------------- -- We need too much control to be able to do this by tweaking the main diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs new file mode 100644 --- /dev/null +++ b/src/Idris/Package.hs @@ -0,0 +1,447 @@ +{-| +Module : Idris.Package +Description : Functionality for working with Idris packages. +Copyright : +License : BSD3 +Maintainer : The Idris Community. +-} +{-# LANGUAGE CPP #-} +module Idris.Package where + +import System.Process +import System.Directory +import System.Exit +import System.IO +import System.FilePath ((), addTrailingPathSeparator, takeFileName, + takeDirectory, normalise, addExtension, hasExtension) +import System.Directory (createDirectoryIfMissing, copyFile) + +import Util.System + +import Control.Monad +import Control.Monad.Trans.State.Strict (execStateT) +import Control.Monad.Trans.Except (runExceptT) + +import Data.List +import Data.List.Split(splitOn) +import Data.Maybe(fromMaybe) +import Data.Either(partitionEithers) + +import Idris.Core.TT +import Idris.REPL +import Idris.Parser (loadModule) +import Idris.Output (pshow) +import Idris.AbsSyntax +import Idris.IdrisDoc +import Idris.IBC +import Idris.Output +import Idris.Imports +import Idris.Error (ifail) + +import Idris.Package.Common +import Idris.Package.Parser + +import IRTS.System + +-- To build a package: +-- * read the package description +-- * check all the library dependencies exist +-- * invoke the makefile if there is one +-- * invoke idris on each module, with idris_opts +-- * install everything into datadir/pname, if install flag is set + +getPkgDesc :: FilePath -> IO PkgDesc +getPkgDesc = parseDesc + +-- --------------------------------------------------------- [ Build Packages ] + +-- | Run the package through the idris compiler. +buildPkg :: [Opt] -- ^ Command line options + -> Bool -- ^ Provide Warnings + -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file) + -> IO () +buildPkg copts warnonly (install, fp) = do + pkgdesc <- parseDesc fp + dir <- getCurrentDirectory + let idx = PkgIndex (pkgIndex (pkgname pkgdesc)) + oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc) + when (and oks) $ do + m_ist <- inPkgDir pkgdesc $ do + + make (makefile pkgdesc) + case (execout pkgdesc) of + Nothing -> do + case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of + Left emsg -> do + putStrLn emsg + exitWith (ExitFailure 1) + Right opts -> buildMods opts (modules pkgdesc) + Just o -> do + let exec = dir o + case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of + Left emsg -> do + putStrLn emsg + exitWith (ExitFailure 1) + Right opts -> buildMain opts (idris_main pkgdesc) + case m_ist of + Nothing -> exitWith (ExitFailure 1) + Just ist -> do + -- Quit with error code if there was a problem + case errSpan ist of + Just _ -> exitWith (ExitFailure 1) + _ -> return () + when install $ installPkg (opt getIBCSubDir copts) pkgdesc + where + buildMain opts (Just mod) = buildMods opts [mod] + buildMain _ Nothing = do + putStrLn "Can't build an executable: No main module given" + exitWith (ExitFailure 1) + +-- --------------------------------------------------------- [ Check Packages ] + +-- | Type check packages only +-- +-- This differs from build in that executables are not built, if the +-- package contains an executable. +checkPkg :: [Opt] -- ^ Command line Options + -> Bool -- ^ Show Warnings + -> Bool -- ^ quit on failure + -> FilePath -- ^ Path to ipkg file. + -> IO () +checkPkg copts warnonly quit fpath = do + pkgdesc <- parseDesc fpath + oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc) + when (and oks) $ do + res <- inPkgDir pkgdesc $ do + make (makefile pkgdesc) + + case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of + Left emsg -> do + putStrLn emsg + exitWith (ExitFailure 1) + Right opts -> do + buildMods opts (modules pkgdesc) + when quit $ case res of + Nothing -> exitWith (ExitFailure 1) + Just res' -> do + case errSpan res' of + Just _ -> exitWith (ExitFailure 1) + _ -> return () + +-- ------------------------------------------------------------------- [ REPL ] + +-- | Check a package and start a REPL. +-- +-- This function only works with packages that have a main module. +-- +replPkg :: [Opt] -- ^ Command line Options + -> FilePath -- ^ Path to ipkg file. + -> Idris () +replPkg copts fp = do + orig <- getIState + runIO $ checkPkg copts False False fp + pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition! + + case mergeOptions copts (idris_opts pkgdesc) of + Left emsg -> ifail emsg + Right opts -> do + putIState orig + dir <- runIO getCurrentDirectory + runIO $ setCurrentDirectory $ dir sourcedir pkgdesc + runMain opts (idris_main pkgdesc) + runIO $ setCurrentDirectory dir + + where + toPath n = foldl1' () $ splitOn "." n + + runMain opts (Just mod) = do + let f = toPath (showCG mod) + idrisMain ((Filename f) : opts) + runMain _ Nothing = + iputStrLn "Can't start REPL: no main module given" + +-- --------------------------------------------------------------- [ Cleaning ] + +-- | Clean Package build files +cleanPkg :: [Opt] -- ^ Command line options. + -> FilePath -- ^ Path to ipkg file. + -> IO () +cleanPkg copts fp = do + pkgdesc <- parseDesc fp + dir <- getCurrentDirectory + inPkgDir pkgdesc $ do + clean (makefile pkgdesc) + mapM_ rmIBC (modules pkgdesc) + rmIdx (pkgname pkgdesc) + case execout pkgdesc of + Nothing -> return () + Just s -> rmExe $ dir s + +-- ------------------------------------------------------ [ Generate IdrisDoc ] + + +-- | Generate IdrisDoc for package +-- TODO: Handle case where module does not contain a matching namespace +-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins +-- +-- Issue number #1572 on the issue tracker +-- https://github.com/idris-lang/Idris-dev/issues/1572 +documentPkg :: [Opt] -- ^ Command line options. + -> FilePath -- ^ Path to ipkg file. + -> IO () +documentPkg copts fp = do + pkgdesc <- parseDesc fp + cd <- getCurrentDirectory + let pkgDir = cd takeDirectory fp + outputDir = cd pkgname pkgdesc ++ "_doc" + popts = NoREPL : Verbose : idris_opts pkgdesc + mods = modules pkgdesc + fs = map (foldl1' () . splitOn "." . showCG) mods + setCurrentDirectory $ pkgDir sourcedir pkgdesc + make (makefile pkgdesc) + setCurrentDirectory pkgDir + case mergeOptions copts popts of + Left emsg -> do + putStrLn emsg + exitWith (ExitFailure 1) + Right opts -> do + let run l = runExceptT . execStateT l + load [] = return () + load (f:fs) = do loadModule f IBC_Building; load fs + loader = do + idrisMain opts + addImportDir (sourcedir pkgdesc) + load fs + idrisInstance <- run loader idrisInit + setCurrentDirectory cd + case idrisInstance of + Left err -> do + putStrLn $ pshow idrisInit err + exitWith (ExitFailure 1) + Right ist -> do + docRes <- generateDocs ist mods outputDir + case docRes of + Right _ -> return () + Left msg -> do + putStrLn msg + exitWith (ExitFailure 1) + +-- ------------------------------------------------------------------- [ Test ] + +-- | Build a package with a sythesized main function that runs the tests +testPkg :: [Opt] -- ^ Command line options. + -> FilePath -- ^ Path to ipkg file. + -> IO () +testPkg copts fp = do + pkgdesc <- parseDesc fp + ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc) + when (and ok) $ do + m_ist <- inPkgDir pkgdesc $ do + make (makefile pkgdesc) + -- Get a temporary file to save the tests' source in + (tmpn, tmph) <- tempfile ".idr" + hPutStrLn tmph $ + "module Test_______\n" ++ + concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc] + ++ "namespace Main\n" + ++ " main : IO ()\n" + ++ " main = do " + ++ concat [ show t ++ "\n " + | t <- idris_tests pkgdesc] + hClose tmph + (tmpn', tmph') <- tempfile "" + hClose tmph' + let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc) + case mergeOptions copts popts of + Left emsg -> do + putStrLn emsg + exitWith (ExitFailure 1) + Right opts -> do + m_ist <- idris opts + rawSystem tmpn' [] + return m_ist + case m_ist of + Nothing -> exitWith (ExitFailure 1) + Just ist -> do + -- Quit with error code if problem building + case errSpan ist of + Just _ -> exitWith (ExitFailure 1) + _ -> return () + +-- ----------------------------------------------------------- [ Installation ] + +-- | Install package +installPkg :: [String] -- ^ Alternate install location + -> PkgDesc -- ^ iPKG file. + -> IO () +installPkg altdests pkgdesc = inPkgDir pkgdesc $ do + d <- getTargetDir + let destdir = case altdests of + [] -> d + (d':_) -> d' + case (execout pkgdesc) of + Nothing -> do + mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc) + installIdx destdir (pkgname pkgdesc) + Just o -> return () -- do nothing, keep executable locally, for noe + + mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc) + +-- ---------------------------------------------------------- [ Helper Methods ] +-- Methods for building, testing, installing, and removal of idris +-- packages. + +buildMods :: [Opt] -> [Name] -> IO (Maybe IState) +buildMods opts ns = do let f = map (toPath . showCG) ns + idris (map Filename f ++ opts) + where toPath n = foldl1' () $ splitOn "." n + +testLib :: Bool -> String -> String -> IO Bool +testLib warn p f + = do d <- getDataDir + gcc <- getCC + (tmpf, tmph) <- tempfile "" + hClose tmph + let libtest = d "rts" "libtest.c" + e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf] + case e of + ExitSuccess -> return True + _ -> do if warn + then do putStrLn $ "Not building " ++ p ++ + " due to missing library " ++ f + return False + else fail $ "Missing library " ++ f + +rmIBC :: Name -> IO () +rmIBC m = rmFile $ toIBCFile m + +rmIdx :: String -> IO () +rmIdx p = do let f = pkgIndex p + ex <- doesFileExist f + when ex $ rmFile f + +rmExe :: String -> IO () +rmExe p = do + fn <- return $ if isWindows && not (hasExtension p) + then addExtension p ".exe" else p + rmFile fn + +toIBCFile (UN n) = str n ++ ".ibc" +toIBCFile (NS n ns) = foldl1' () (reverse (toIBCFile n : map str ns)) + +installIBC :: String -> String -> Name -> IO () +installIBC dest p m = do + let f = toIBCFile m + let destdir = dest p getDest m + putStrLn $ "Installing " ++ f ++ " to " ++ destdir + createDirectoryIfMissing True destdir + copyFile f (destdir takeFileName f) + return () + where + getDest (UN n) = "" + getDest (NS n ns) = foldl1' () (reverse (getDest n : map str ns)) + +installIdx :: String -> String -> IO () +installIdx dest p = do + let f = pkgIndex p + let destdir = dest p + putStrLn $ "Installing " ++ f ++ " to " ++ destdir + createDirectoryIfMissing True destdir + copyFile f (destdir takeFileName f) + return () + +installObj :: String -> String -> String -> IO () +installObj dest p o = do + let destdir = addTrailingPathSeparator (dest p) + putStrLn $ "Installing " ++ o ++ " to " ++ destdir + createDirectoryIfMissing True destdir + copyFile o (destdir takeFileName o) + return () + +#ifdef mingw32_HOST_OS +mkDirCmd = "mkdir " +#else +mkDirCmd = "mkdir -p " +#endif + +inPkgDir :: PkgDesc -> IO a -> IO a +inPkgDir pkgdesc action = + do dir <- getCurrentDirectory + when (sourcedir pkgdesc /= "") $ + do putStrLn $ "Entering directory `" ++ ("." sourcedir pkgdesc) ++ "'" + setCurrentDirectory $ dir sourcedir pkgdesc + res <- action + when (sourcedir pkgdesc /= "") $ + do putStrLn $ "Leaving directory `" ++ ("." sourcedir pkgdesc) ++ "'" + setCurrentDirectory dir + return res + +-- ------------------------------------------------------- [ Makefile Commands ] +-- | Invoke a Makefile's default target. +make :: Maybe String -> IO () +make Nothing = return () +make (Just s) = do rawSystem "make" ["-f", s] + return () + +-- | Invoke a Makefile's clean target. +clean :: Maybe String -> IO () +clean Nothing = return () +clean (Just s) = do rawSystem "make" ["-f", s, "clean"] + return () + +-- | Merge an option list representing the command line options into +-- those specified for a package description. +-- +-- This is not a complete union between the two options sets. First, +-- to prevent important package specified options from being +-- overwritten. Second, the semantics for this merge are not fully +-- defined. +-- +-- A discussion for this is on the issue tracker: +-- https://github.com/idris-lang/Idris-dev/issues/1448 +-- +mergeOptions :: [Opt] -- ^ The command line options + -> [Opt] -- ^ The package options + -> Either String [Opt] +mergeOptions copts popts = + case partitionEithers (map chkOpt (normaliseOpts copts)) of + ([], copts') -> Right $ copts' ++ popts + (es, _) -> Left $ genErrMsg es + where + normaliseOpts :: [Opt] -> [Opt] + normaliseOpts = filter filtOpt + + filtOpt :: Opt -> Bool + filtOpt (PkgBuild _) = False + filtOpt (PkgInstall _) = False + filtOpt (PkgClean _) = False + filtOpt (PkgCheck _) = False + filtOpt (PkgREPL _) = False + filtOpt (PkgMkDoc _) = False + filtOpt (PkgTest _) = False + filtOpt _ = True + + chkOpt :: Opt -> Either String Opt + chkOpt o@(OLogging _) = Right o + chkOpt o@(OLogCats _) = Right o + chkOpt o@(DefaultTotal) = Right o + chkOpt o@(DefaultPartial) = Right o + chkOpt o@(WarnPartial) = Right o + chkOpt o@(WarnReach) = Right o + chkOpt o@(IBCSubDir _) = Right o + chkOpt o@(ImportDir _ ) = Right o + chkOpt o@(UseCodegen _) = Right o + chkOpt o = Left (unwords ["\t", show o, "\n"]) + + genErrMsg :: [String] -> String + genErrMsg es = unlines + [ "Not all command line options can be used to override package options." + , "\nThe only changeable options are:" + , "\t--log , --total, --warnpartial, --warnreach" + , "\t--ibcsubdir , -i --idrispath " + , "\t--logging-categories " + , "\nThe options need removing are:" + , unlines es + ] + +-- --------------------------------------------------------------------- [ EOF ] diff --git a/src/Idris/Package/Common.hs b/src/Idris/Package/Common.hs new file mode 100644 --- /dev/null +++ b/src/Idris/Package/Common.hs @@ -0,0 +1,42 @@ +{-| +Module : Idris.Package.Common +Description : Data structures common to all `iPKG` file formats. +Copyright : +License : BSD3 +Maintainer : The Idris Community. +-} +module Idris.Package.Common where + +import Idris.Core.TT +import Idris.REPL +import Idris.AbsSyntaxTree + +-- | Description of an Idris package. +data PkgDesc = PkgDesc { + pkgname :: String -- ^ Name associated with a package. + , pkgdeps :: [String] -- ^ List of packages this package depends on. + , pkgbrief :: Maybe String -- ^ Brief description of the package. + , pkgversion :: Maybe String -- ^ Version string to associate with the package. + , pkgreadme :: Maybe String -- ^ Location of the README file. + , pkglicense :: Maybe String -- ^ Description of the licensing information. + , pkgauthor :: Maybe String -- ^ Author information. + , pkgmaintainer :: Maybe String -- ^ Maintainer information. + , pkghomepage :: Maybe String -- ^ Website associated with the package. + , pkgsourceloc :: Maybe String -- ^ Location of the source files. + , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker. + , libdeps :: [String] -- ^ External dependencies. + , objs :: [String] -- ^ Object files required by the package. + , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process. + , idris_opts :: [Opt] -- ^ List of options to give the compiler. + , sourcedir :: String -- ^ Source directory for Idris files. + , modules :: [Name] -- ^ Modules provided by the package. + , idris_main :: Maybe Name -- ^ If an executable in which module can the Main namespace and function be found. + , execout :: Maybe String -- ^ What to call the executable. + , idris_tests :: [Name] -- ^ Lists of tests to execute against the package. + } deriving (Show) + +-- | Default settings for package descriptions. +defaultPkg :: PkgDesc +defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing + Nothing Nothing Nothing Nothing + Nothing [] [] Nothing [] "" [] Nothing Nothing [] diff --git a/src/Idris/Package/Parser.hs b/src/Idris/Package/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Idris/Package/Parser.hs @@ -0,0 +1,242 @@ +{-| +Module : Idris.Package.Parser +Description : `iPKG` file parser and package description information. +Copyright : +License : BSD3 +Maintainer : The Idris Community. +-} +{-# LANGUAGE CPP, ConstraintKinds #-} +#if !(MIN_VERSION_base(4,8,0)) +{-# LANGUAGE OverlappingInstances #-} +#endif +module Idris.Package.Parser where + +import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace) +import qualified Text.PrettyPrint.ANSI.Leijen as PP +import Idris.Core.TT +import Idris.REPL +import Idris.AbsSyntaxTree +import Idris.Parser.Helpers hiding (stringLiteral) +import Idris.CmdOptions + +import Idris.Package.Common + +import Control.Monad.State.Strict +import Control.Applicative +import System.FilePath (takeFileName, isValid) +import Data.Maybe (isNothing, fromJust) +import Data.List (union) + +import Util.System + +type PParser = StateT PkgDesc IdrisInnerParser + +instance HasLastTokenSpan PParser where + getLastTokenSpan = return Nothing + +#if MIN_VERSION_base(4,9,0) +instance {-# OVERLAPPING #-} DeltaParsing PParser where + line = lift line + {-# INLINE line #-} + position = lift position + {-# INLINE position #-} + slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s + {-# INLINE slicedWith #-} + rend = lift rend + {-# INLINE rend #-} + restOfLine = lift restOfLine + {-# INLINE restOfLine #-} +#endif + +#if MIN_VERSION_base(4,8,0) +instance {-# OVERLAPPING #-} TokenParsing PParser where +#else +instance TokenParsing PParser where +#endif + someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure () + + +parseDesc :: FilePath -> IO PkgDesc +parseDesc fp = do + p <- readFile fp + case runparser pPkg defaultPkg fp p of + Failure (ErrInfo err _) -> fail (show $ PP.plain err) + Success x -> return x + +pPkg :: PParser PkgDesc +pPkg = do + reserved "package" + p <- filename + st <- get + put (st { pkgname = p }) + some pClause + st <- get + eof + return st + + +-- | Parses a filename. +-- | +-- | Treated for now as an identifier or a double-quoted string. +filename :: (MonadicParsing m, HasLastTokenSpan m) => m String +filename = (do + filename <- token $ + -- Treat a double-quoted string as a filename to support spaces. + -- This also moves away from tying filenames to identifiers, so + -- it will also accept hyphens + -- (https://github.com/idris-lang/Idris-dev/issues/2721) + stringLiteral + <|> + -- Through at least version 0.9.19.1, IPKG executable values were + -- possibly namespaced identifiers, like foo.bar.baz. + show <$> fst <$> iName [] + case filenameErrorMessage filename of + Just errorMessage -> fail errorMessage + Nothing -> return filename) + "filename" + where + -- TODO: Report failing span better! We could lookAhead, + -- or do something with DeltaParsing? + filenameErrorMessage :: FilePath -> Maybe String + filenameErrorMessage path = either Just (const Nothing) $ do + checkEmpty path + checkValid path + checkNoDirectoryComponent path + where + checkThat ok message = + if ok then Right () else Left message + + checkEmpty path = + checkThat (path /= "") "filename must not be empty" + + checkValid path = + checkThat (System.FilePath.isValid path) + "filename must contain only valid characters" + + checkNoDirectoryComponent path = + checkThat (path == takeFileName path) + "filename must contain no directory component" + + +pClause :: PParser () +pClause = do reserved "executable"; lchar '='; + exec <- filename + st <- get + put (st { execout = Just exec }) + + <|> do reserved "main"; lchar '='; + main <- fst <$> iName [] + st <- get + put (st { idris_main = Just main }) + + <|> do reserved "sourcedir"; lchar '='; + src <- fst <$> identifier + st <- get + put (st { sourcedir = src }) + + <|> do reserved "opts"; lchar '='; + opts <- stringLiteral + st <- get + let args = pureArgParser (words opts) + put (st { idris_opts = args ++ idris_opts st }) + + <|> do reserved "pkgs"; lchar '='; + ps <- sepBy1 (fst <$> identifier) (lchar ',') + st <- get + let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps + + put (st { pkgdeps = ps `union` (pkgdeps st) + , idris_opts = pkgs ++ idris_opts st}) + + <|> do reserved "modules"; lchar '='; + ms <- sepBy1 (fst <$> iName []) (lchar ',') + st <- get + put (st { modules = modules st ++ ms }) + + <|> do reserved "libs"; lchar '='; + ls <- sepBy1 (fst <$> identifier) (lchar ',') + st <- get + put (st { libdeps = libdeps st ++ ls }) + + <|> do reserved "objs"; lchar '='; + ls <- sepBy1 (fst <$> identifier) (lchar ',') + st <- get + put (st { objs = objs st ++ ls }) + + <|> do reserved "makefile"; lchar '='; + mk <- fst <$> iName [] + st <- get + put (st { makefile = Just (show mk) }) + + <|> do reserved "tests"; lchar '='; + ts <- sepBy1 (fst <$> iName []) (lchar ',') + st <- get + put st { idris_tests = idris_tests st ++ ts } + + <|> do reserved "version" + lchar '=' + vStr <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkgversion = Just vStr} + + <|> do reserved "readme" + lchar '=' + rme <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put (st { pkgreadme = Just rme }) + + <|> do reserved "license" + lchar '=' + lStr <- many (satisfy (not . isEol)) + eol + st <- get + put st {pkglicense = Just lStr} + + <|> do reserved "homepage" + lchar '=' + www <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkghomepage = Just www} + + <|> do reserved "sourceloc" + lchar '=' + srcpage <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkgsourceloc = Just srcpage} + + <|> do reserved "bugtracker" + lchar '=' + src <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkgbugtracker = Just src} + + <|> do reserved "brief" + lchar '=' + brief <- stringLiteral + st <- get + someSpace + put st {pkgbrief = Just brief} + + <|> do reserved "author"; lchar '='; + author <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkgauthor = Just author} + + <|> do reserved "maintainer"; lchar '='; + maintainer <- many (satisfy (not . isEol)) + eol + someSpace + st <- get + put st {pkgmaintainer = Just maintainer} diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -1116,7 +1116,9 @@ @ -} rhs :: SyntaxInfo -> Name -> IdrisParser PTerm -rhs syn n = do lchar '='; expr syn +rhs syn n = do lchar '=' + indentPropHolds gtProp + expr syn <|> do symbol "?="; fc <- getFC name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}"; diff --git a/src/Pkg/PParser.hs b/src/Pkg/PParser.hs deleted file mode 100644 --- a/src/Pkg/PParser.hs +++ /dev/null @@ -1,265 +0,0 @@ -{-| -Module : Pkg.PParser -Description : `iPKG` file parser and package description information. -Copyright : -License : BSD3 -Maintainer : The Idris Community. --} -{-# LANGUAGE CPP, ConstraintKinds #-} -#if !(MIN_VERSION_base(4,8,0)) -{-# LANGUAGE OverlappingInstances #-} -#endif -module Pkg.PParser where - -import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace) -import qualified Text.PrettyPrint.ANSI.Leijen as PP -import Idris.Core.TT -import Idris.REPL -import Idris.AbsSyntaxTree -import Idris.Parser.Helpers hiding (stringLiteral) -import Idris.CmdOptions - -import Control.Monad.State.Strict -import Control.Applicative -import System.FilePath (takeFileName, isValid) -import Data.Maybe (isNothing, fromJust) - -import Util.System - -type PParser = StateT PkgDesc IdrisInnerParser - -data PkgDesc = PkgDesc { - pkgname :: String -- ^ Name associated with a package. - , pkgbrief :: Maybe String -- ^ Brief description of the package. - , pkgversion :: Maybe String -- ^ Version string to associate with the package. - , pkgreadme :: Maybe String -- ^ Location of the README file. - , pkglicense :: Maybe String -- ^ Description of the licensing information. - , pkgauthor :: Maybe String -- ^ Author information. - , pkgmaintainer :: Maybe String -- ^ Maintainer information. - , pkghomepage :: Maybe String -- ^ Website associated with the package. - , pkgsourceloc :: Maybe String -- ^ Location of the source files. - , pkgbugtracker :: Maybe String -- ^ Location of the project's bug tracker. - , libdeps :: [String] -- ^ External dependencies. - , objs :: [String] -- ^ Object files required by the package. - , makefile :: Maybe String -- ^ Makefile used to build external code. Used as part of the FFI process. - , idris_opts :: [Opt] -- ^ List of options to give the compiler. - , sourcedir :: String -- ^ Source directory for Idris files. - , modules :: [Name] -- ^ Modules provided by the package. - , idris_main :: Name -- ^ If an executable in which module can the Main namespace and function be found. - , execout :: Maybe String -- ^ What to call the executable. - , idris_tests :: [Name] -- ^ Lists of tests to execute against the package. - } deriving (Show) - --- | Default settings for package descriptions. -defaultPkg :: PkgDesc -defaultPkg = PkgDesc "" Nothing Nothing Nothing Nothing - Nothing Nothing Nothing Nothing - Nothing [] [] Nothing [] "" [] (sUN "") Nothing [] - -instance HasLastTokenSpan PParser where - getLastTokenSpan = return Nothing - -#if MIN_VERSION_base(4,9,0) -instance {-# OVERLAPPING #-} DeltaParsing PParser where - line = lift line - {-# INLINE line #-} - position = lift position - {-# INLINE position #-} - slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s - {-# INLINE slicedWith #-} - rend = lift rend - {-# INLINE rend #-} - restOfLine = lift restOfLine - {-# INLINE restOfLine #-} -#endif - -#if MIN_VERSION_base(4,8,0) -instance {-# OVERLAPPING #-} TokenParsing PParser where -#else -instance TokenParsing PParser where -#endif - someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure () - - -parseDesc :: FilePath -> IO PkgDesc -parseDesc fp = do - p <- readFile fp - case runparser pPkg defaultPkg fp p of - Failure (ErrInfo err _) -> fail (show $ PP.plain err) - Success x -> return x - -pPkg :: PParser PkgDesc -pPkg = do - reserved "package" - p <- filename - st <- get - put (st { pkgname = p }) - some pClause - st <- get - eof - return st - - --- | Parses a filename. --- | --- | Treated for now as an identifier or a double-quoted string. -filename :: (MonadicParsing m, HasLastTokenSpan m) => m String -filename = (do - filename <- token $ - -- Treat a double-quoted string as a filename to support spaces. - -- This also moves away from tying filenames to identifiers, so - -- it will also accept hyphens - -- (https://github.com/idris-lang/Idris-dev/issues/2721) - stringLiteral - <|> - -- Through at least version 0.9.19.1, IPKG executable values were - -- possibly namespaced identifiers, like foo.bar.baz. - show <$> fst <$> iName [] - case filenameErrorMessage filename of - Just errorMessage -> fail errorMessage - Nothing -> return filename) - "filename" - where - -- TODO: Report failing span better! We could lookAhead, - -- or do something with DeltaParsing? - filenameErrorMessage :: FilePath -> Maybe String - filenameErrorMessage path = either Just (const Nothing) $ do - checkEmpty path - checkValid path - checkNoDirectoryComponent path - where - checkThat ok message = - if ok then Right () else Left message - - checkEmpty path = - checkThat (path /= "") "filename must not be empty" - - checkValid path = - checkThat (System.FilePath.isValid path) - "filename must contain only valid characters" - - checkNoDirectoryComponent path = - checkThat (path == takeFileName path) - "filename must contain no directory component" - - -pClause :: PParser () -pClause = do reserved "executable"; lchar '='; - exec <- filename - st <- get - put (st { execout = Just exec }) - - <|> do reserved "main"; lchar '='; - main <- fst <$> iName [] - st <- get - put (st { idris_main = main }) - - <|> do reserved "sourcedir"; lchar '='; - src <- fst <$> identifier - st <- get - put (st { sourcedir = src }) - - <|> do reserved "opts"; lchar '='; - opts <- stringLiteral - st <- get - let args = pureArgParser (words opts) - put (st { idris_opts = args ++ idris_opts st }) - - <|> do reserved "pkgs"; lchar '='; - ps <- sepBy1 (fst <$> identifier) (lchar ',') - st <- get - let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps - put (st {idris_opts = pkgs ++ idris_opts st}) - - <|> do reserved "modules"; lchar '='; - ms <- sepBy1 (fst <$> iName []) (lchar ',') - st <- get - put (st { modules = modules st ++ ms }) - - <|> do reserved "libs"; lchar '='; - ls <- sepBy1 (fst <$> identifier) (lchar ',') - st <- get - put (st { libdeps = libdeps st ++ ls }) - - <|> do reserved "objs"; lchar '='; - ls <- sepBy1 (fst <$> identifier) (lchar ',') - st <- get - put (st { objs = libdeps st ++ ls }) - - <|> do reserved "makefile"; lchar '='; - mk <- fst <$> iName [] - st <- get - put (st { makefile = Just (show mk) }) - - <|> do reserved "tests"; lchar '='; - ts <- sepBy1 (fst <$> iName []) (lchar ',') - st <- get - put st { idris_tests = idris_tests st ++ ts } - - <|> do reserved "version" - lchar '=' - vStr <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkgversion = Just vStr} - - <|> do reserved "readme" - lchar '=' - rme <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put (st { pkgreadme = Just rme }) - - <|> do reserved "license" - lchar '=' - lStr <- many (satisfy (not . isEol)) - eol - st <- get - put st {pkglicense = Just lStr} - - <|> do reserved "homepage" - lchar '=' - www <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkghomepage = Just www} - - <|> do reserved "sourceloc" - lchar '=' - srcpage <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkgsourceloc = Just srcpage} - - <|> do reserved "bugtracker" - lchar '=' - src <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkgbugtracker = Just src} - - <|> do reserved "brief" - lchar '=' - brief <- stringLiteral - st <- get - someSpace - put st {pkgbrief = Just brief} - - <|> do reserved "author"; lchar '='; - author <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkgauthor = Just author} - - <|> do reserved "maintainer"; lchar '='; - maintainer <- many (satisfy (not . isEol)) - eol - someSpace - st <- get - put st {pkgmaintainer = Just maintainer} diff --git a/src/Pkg/Package.hs b/src/Pkg/Package.hs deleted file mode 100644 --- a/src/Pkg/Package.hs +++ /dev/null @@ -1,437 +0,0 @@ -{-| -Module : Pkg.Package -Description : Functionality for working with Idris packages. -Copyright : -License : BSD3 -Maintainer : The Idris Community. --} -{-# LANGUAGE CPP #-} -module Pkg.Package where - -import System.Process -import System.Directory -import System.Exit -import System.IO -import System.FilePath ((), addTrailingPathSeparator, takeFileName, - takeDirectory, normalise, addExtension, hasExtension) -import System.Directory (createDirectoryIfMissing, copyFile) - -import Util.System - -import Control.Monad -import Control.Monad.Trans.State.Strict (execStateT) -import Control.Monad.Trans.Except (runExceptT) - -import Data.List -import Data.List.Split(splitOn) -import Data.Maybe(fromMaybe) -import Data.Either(partitionEithers) - -import Idris.Core.TT -import Idris.REPL -import Idris.Parser (loadModule) -import Idris.Output (pshow) -import Idris.AbsSyntax -import Idris.IdrisDoc -import Idris.IBC -import Idris.Output -import Idris.Imports -import Idris.Error (ifail) - -import Pkg.PParser - -import IRTS.System - --- To build a package: --- * read the package description --- * check all the library dependencies exist --- * invoke the makefile if there is one --- * invoke idris on each module, with idris_opts --- * install everything into datadir/pname, if install flag is set - --- --------------------------------------------------------- [ Build Packages ] - --- | Run the package through the idris compiler. -buildPkg :: [Opt] -- ^ Command line options - -> Bool -- ^ Provide Warnings - -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file) - -> IO () -buildPkg copts warnonly (install, fp) = do - pkgdesc <- parseDesc fp - dir <- getCurrentDirectory - let idx = PkgIndex (pkgIndex (pkgname pkgdesc)) - oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc) - when (and oks) $ do - m_ist <- inPkgDir pkgdesc $ do - - make (makefile pkgdesc) - case (execout pkgdesc) of - Nothing -> do - case mergeOptions copts (idx : NoREPL : Verbose : idris_opts pkgdesc) of - Left emsg -> do - putStrLn emsg - exitWith (ExitFailure 1) - Right opts -> buildMods opts (modules pkgdesc) - Just o -> do - let exec = dir o - case mergeOptions copts (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc) of - Left emsg -> do - putStrLn emsg - exitWith (ExitFailure 1) - Right opts -> buildMods opts [idris_main pkgdesc] - case m_ist of - Nothing -> exitWith (ExitFailure 1) - Just ist -> do - -- Quit with error code if there was a problem - case errSpan ist of - Just _ -> exitWith (ExitFailure 1) - _ -> return () - when install $ installPkg (opt getIBCSubDir copts) pkgdesc - --- --------------------------------------------------------- [ Check Packages ] - --- | Type check packages only --- --- This differs from build in that executables are not built, if the --- package contains an executable. -checkPkg :: [Opt] -- ^ Command line Options - -> Bool -- ^ Show Warnings - -> Bool -- ^ quit on failure - -> FilePath -- ^ Path to ipkg file. - -> IO () -checkPkg copts warnonly quit fpath = do - pkgdesc <- parseDesc fpath - oks <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc) - when (and oks) $ do - res <- inPkgDir pkgdesc $ do - make (makefile pkgdesc) - - case mergeOptions copts (NoREPL : Verbose : idris_opts pkgdesc) of - Left emsg -> do - putStrLn emsg - exitWith (ExitFailure 1) - Right opts -> do - buildMods opts (modules pkgdesc) - when quit $ case res of - Nothing -> exitWith (ExitFailure 1) - Just res' -> do - case errSpan res' of - Just _ -> exitWith (ExitFailure 1) - _ -> return () - --- ------------------------------------------------------------------- [ REPL ] - --- | Check a package and start a REPL. --- --- This function only works with packages that have a main module. --- -replPkg :: [Opt] -- ^ Command line Options - -> FilePath -- ^ Path to ipkg file. - -> Idris () -replPkg copts fp = do - orig <- getIState - runIO $ checkPkg copts False False fp - pkgdesc <- runIO $ parseDesc fp -- bzzt, repetition! - - case mergeOptions copts (idris_opts pkgdesc) of - Left emsg -> ifail emsg - Right opts -> do - let mod = idris_main pkgdesc - let f = toPath (showCG mod) - putIState orig - dir <- runIO getCurrentDirectory - runIO $ setCurrentDirectory $ dir sourcedir pkgdesc - - if (f /= "") - then idrisMain ((Filename f) : opts) - else iputStrLn "Can't start REPL: no main module given" - runIO $ setCurrentDirectory dir - - where - toPath n = foldl1' () $ splitOn "." n - --- --------------------------------------------------------------- [ Cleaning ] - --- | Clean Package build files -cleanPkg :: [Opt] -- ^ Command line options. - -> FilePath -- ^ Path to ipkg file. - -> IO () -cleanPkg copts fp = do - pkgdesc <- parseDesc fp - dir <- getCurrentDirectory - inPkgDir pkgdesc $ do - clean (makefile pkgdesc) - mapM_ rmIBC (modules pkgdesc) - rmIdx (pkgname pkgdesc) - case execout pkgdesc of - Nothing -> return () - Just s -> rmExe $ dir s - --- ------------------------------------------------------ [ Generate IdrisDoc ] - - --- | Generate IdrisDoc for package --- TODO: Handle case where module does not contain a matching namespace --- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins --- --- Issue number #1572 on the issue tracker --- https://github.com/idris-lang/Idris-dev/issues/1572 -documentPkg :: [Opt] -- ^ Command line options. - -> FilePath -- ^ Path to ipkg file. - -> IO () -documentPkg copts fp = do - pkgdesc <- parseDesc fp - cd <- getCurrentDirectory - let pkgDir = cd takeDirectory fp - outputDir = cd pkgname pkgdesc ++ "_doc" - popts = NoREPL : Verbose : idris_opts pkgdesc - mods = modules pkgdesc - fs = map (foldl1' () . splitOn "." . showCG) mods - setCurrentDirectory $ pkgDir sourcedir pkgdesc - make (makefile pkgdesc) - setCurrentDirectory pkgDir - case mergeOptions copts popts of - Left emsg -> do - putStrLn emsg - exitWith (ExitFailure 1) - Right opts -> do - let run l = runExceptT . execStateT l - load [] = return () - load (f:fs) = do loadModule f IBC_Building; load fs - loader = do - idrisMain opts - addImportDir (sourcedir pkgdesc) - load fs - idrisInstance <- run loader idrisInit - setCurrentDirectory cd - case idrisInstance of - Left err -> do - putStrLn $ pshow idrisInit err - exitWith (ExitFailure 1) - Right ist -> do - docRes <- generateDocs ist mods outputDir - case docRes of - Right _ -> return () - Left msg -> do - putStrLn msg - exitWith (ExitFailure 1) - --- ------------------------------------------------------------------- [ Test ] - --- | Build a package with a sythesized main function that runs the tests -testPkg :: [Opt] -- ^ Command line options. - -> FilePath -- ^ Path to ipkg file. - -> IO () -testPkg copts fp = do - pkgdesc <- parseDesc fp - ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc) - when (and ok) $ do - m_ist <- inPkgDir pkgdesc $ do - make (makefile pkgdesc) - -- Get a temporary file to save the tests' source in - (tmpn, tmph) <- tempfile ".idr" - hPutStrLn tmph $ - "module Test_______\n" ++ - concat ["import " ++ show m ++ "\n" | m <- modules pkgdesc] - ++ "namespace Main\n" - ++ " main : IO ()\n" - ++ " main = do " - ++ concat [ show t ++ "\n " - | t <- idris_tests pkgdesc] - hClose tmph - (tmpn', tmph') <- tempfile "" - hClose tmph' - let popts = (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc) - case mergeOptions copts popts of - Left emsg -> do - putStrLn emsg - exitWith (ExitFailure 1) - Right opts -> do - m_ist <- idris opts - rawSystem tmpn' [] - return m_ist - case m_ist of - Nothing -> exitWith (ExitFailure 1) - Just ist -> do - -- Quit with error code if problem building - case errSpan ist of - Just _ -> exitWith (ExitFailure 1) - _ -> return () - --- ----------------------------------------------------------- [ Installation ] - --- | Install package -installPkg :: [String] -- ^ Alternate install location - -> PkgDesc -- ^ iPKG file. - -> IO () -installPkg altdests pkgdesc = inPkgDir pkgdesc $ do - d <- getTargetDir - let destdir = case altdests of - [] -> d - (d':_) -> d' - case (execout pkgdesc) of - Nothing -> do - mapM_ (installIBC destdir (pkgname pkgdesc)) (modules pkgdesc) - installIdx destdir (pkgname pkgdesc) - Just o -> return () -- do nothing, keep executable locally, for noe - - mapM_ (installObj destdir (pkgname pkgdesc)) (objs pkgdesc) - --- ---------------------------------------------------------- [ Helper Methods ] --- Methods for building, testing, installing, and removal of idris --- packages. - -buildMods :: [Opt] -> [Name] -> IO (Maybe IState) -buildMods opts ns = do let f = map (toPath . showCG) ns - idris (map Filename f ++ opts) - where toPath n = foldl1' () $ splitOn "." n - -testLib :: Bool -> String -> String -> IO Bool -testLib warn p f - = do d <- getDataDir - gcc <- getCC - (tmpf, tmph) <- tempfile "" - hClose tmph - let libtest = d "rts" "libtest.c" - e <- rawSystem gcc [libtest, "-l" ++ f, "-o", tmpf] - case e of - ExitSuccess -> return True - _ -> do if warn - then do putStrLn $ "Not building " ++ p ++ - " due to missing library " ++ f - return False - else fail $ "Missing library " ++ f - -rmIBC :: Name -> IO () -rmIBC m = rmFile $ toIBCFile m - -rmIdx :: String -> IO () -rmIdx p = do let f = pkgIndex p - ex <- doesFileExist f - when ex $ rmFile f - -rmExe :: String -> IO () -rmExe p = do - fn <- return $ if isWindows && not (hasExtension p) - then addExtension p ".exe" else p - rmFile fn - -toIBCFile (UN n) = str n ++ ".ibc" -toIBCFile (NS n ns) = foldl1' () (reverse (toIBCFile n : map str ns)) - -installIBC :: String -> String -> Name -> IO () -installIBC dest p m = do - let f = toIBCFile m - let destdir = dest p getDest m - putStrLn $ "Installing " ++ f ++ " to " ++ destdir - createDirectoryIfMissing True destdir - copyFile f (destdir takeFileName f) - return () - where - getDest (UN n) = "" - getDest (NS n ns) = foldl1' () (reverse (getDest n : map str ns)) - -installIdx :: String -> String -> IO () -installIdx dest p = do - let f = pkgIndex p - let destdir = dest p - putStrLn $ "Installing " ++ f ++ " to " ++ destdir - createDirectoryIfMissing True destdir - copyFile f (destdir takeFileName f) - return () - -installObj :: String -> String -> String -> IO () -installObj dest p o = do - let destdir = addTrailingPathSeparator (dest p) - putStrLn $ "Installing " ++ o ++ " to " ++ destdir - createDirectoryIfMissing True destdir - copyFile o (destdir takeFileName o) - return () - -#ifdef mingw32_HOST_OS -mkDirCmd = "mkdir " -#else -mkDirCmd = "mkdir -p " -#endif - -inPkgDir :: PkgDesc -> IO a -> IO a -inPkgDir pkgdesc action = - do dir <- getCurrentDirectory - when (sourcedir pkgdesc /= "") $ - do putStrLn $ "Entering directory `" ++ ("." sourcedir pkgdesc) ++ "'" - setCurrentDirectory $ dir sourcedir pkgdesc - res <- action - when (sourcedir pkgdesc /= "") $ - do putStrLn $ "Leaving directory `" ++ ("." sourcedir pkgdesc) ++ "'" - setCurrentDirectory dir - return res - --- ------------------------------------------------------- [ Makefile Commands ] --- | Invoke a Makefile's default target. -make :: Maybe String -> IO () -make Nothing = return () -make (Just s) = do rawSystem "make" ["-f", s] - return () - --- | Invoke a Makefile's clean target. -clean :: Maybe String -> IO () -clean Nothing = return () -clean (Just s) = do rawSystem "make" ["-f", s, "clean"] - return () - --- | Merge an option list representing the command line options into --- those specified for a package description. --- --- This is not a complete union between the two options sets. First, --- to prevent important package specified options from being --- overwritten. Second, the semantics for this merge are not fully --- defined. --- --- A discussion for this is on the issue tracker: --- https://github.com/idris-lang/Idris-dev/issues/1448 --- -mergeOptions :: [Opt] -- ^ The command line options - -> [Opt] -- ^ The package options - -> Either String [Opt] -mergeOptions copts popts = - case partitionEithers (map chkOpt (normaliseOpts copts)) of - ([], copts') -> Right $ copts' ++ popts - (es, _) -> Left $ genErrMsg es - where - normaliseOpts :: [Opt] -> [Opt] - normaliseOpts = filter filtOpt - - filtOpt :: Opt -> Bool - filtOpt (PkgBuild _) = False - filtOpt (PkgInstall _) = False - filtOpt (PkgClean _) = False - filtOpt (PkgCheck _) = False - filtOpt (PkgREPL _) = False - filtOpt (PkgMkDoc _) = False - filtOpt (PkgTest _) = False - filtOpt _ = True - - chkOpt :: Opt -> Either String Opt - chkOpt o@(OLogging _) = Right o - chkOpt o@(OLogCats _) = Right o - chkOpt o@(DefaultTotal) = Right o - chkOpt o@(DefaultPartial) = Right o - chkOpt o@(WarnPartial) = Right o - chkOpt o@(WarnReach) = Right o - chkOpt o@(IBCSubDir _) = Right o - chkOpt o@(ImportDir _ ) = Right o - chkOpt o@(UseCodegen _) = Right o - chkOpt o = Left (unwords ["\t", show o, "\n"]) - - genErrMsg :: [String] -> String - genErrMsg es = unlines - [ "Not all command line options can be used to override package options." - , "\nThe only changeable options are:" - , "\t--log , --total, --warnpartial, --warnreach" - , "\t--ibcsubdir , -i --idrispath " - , "\t--logging-categories " - , "\nThe options need removing are:" - , unlines es - ] - --- --------------------------------------------------------------------- [ EOF ] diff --git a/src/Util/Net.hs b/src/Util/Net.hs --- a/src/Util/Net.hs +++ b/src/Util/Net.hs @@ -19,10 +19,10 @@ localhost <- inet_addr "127.0.0.1" bracketOnError (socket AF_INET Stream proto) - (sClose) + (close) (\sock -> do setSocketOption sock ReuseAddr 1 - bindSocket sock (SockAddrInet port localhost) + bind sock (SockAddrInet port localhost) listen sock maxListenQueue return sock ) @@ -32,10 +32,10 @@ localhost <- inet_addr "127.0.0.1" bracketOnError (socket AF_INET Stream proto) - (sClose) + (close) (\sock -> do setSocketOption sock ReuseAddr 1 - bindSocket sock (SockAddrInet aNY_PORT localhost) + bind sock (SockAddrInet aNY_PORT localhost) listen sock maxListenQueue port <- socketPort sock return (sock, port) diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-6.5 +resolver: lts-6.9 packages: - location: . diff --git a/test/Makefile b/test/Makefile deleted file mode 100644 --- a/test/Makefile +++ /dev/null @@ -1,34 +0,0 @@ -.PHONY: test test_js time update diff distclean $(TESTS) - -TESTS = $(sort $(patsubst %/,%.test,$(wildcard */))) - -test: $(TESTS) - - -info: runtest - @./runtest all - -%.test: runtest - @./runtest $(patsubst %.test,%,$@) -q - -test_js: runtest - @./runtest without tutorial007 sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 ffi008 primitives005 primitives006 views003 opts --codegen node - -update: runtest - @./runtest all -u - -diff: runtest - @./runtest all -d - -time: runtest - @./runtest all -t - -distclean: - @rm runtest - @rm -f *~ - @rm -f */output - - -runtest: - @ghc --make runtest.hs - @rm runtest.o runtest.hi diff --git a/test/TestData.hs b/test/TestData.hs new file mode 100644 --- /dev/null +++ b/test/TestData.hs @@ -0,0 +1,307 @@ +module TestData where + +import Data.IntMap as IMap +import Data.Map.Strict as Map +import Data.Set as Set + +data Codegen = C | JS deriving (Show, Eq, Ord) +type Index = Int +data CompatCodegen = ANY | C_CG | NODE_CG | NONE + +-- A TestFamily groups tests that share the same theme +data TestFamily = TestFamily { + -- A shorter lowcase name to use in filenames + id :: String, + -- A proper name for the test family that will be displayed + name :: String, + -- A map of test metadata: + -- - The key is the index (>=1 && <1000) + -- - The value is the set of compatible code generators, + -- or Nothing if the test doesn't depend on a code generator + tests :: IntMap (Maybe (Set Codegen)) +} deriving (Show) + +toCodegenSet :: CompatCodegen -> Maybe (Set Codegen) +toCodegenSet compatCodegen = fmap Set.fromList mList where + mList = case compatCodegen of + ANY -> Just [ C, JS ] + C_CG -> Just [ C ] + NODE_CG -> Just [ JS ] + NONE -> Nothing + +testFamilies :: [TestFamily] +testFamilies = fmap instantiate testFamiliesData where + instantiate (id, name, testsData) = TestFamily id name tests where + tests = IMap.fromList (fmap makeSetCodegen testsData) + makeSetCodegen (index, codegens) = (index, toCodegenSet codegens) + +testFamiliesForCodegen :: Codegen -> [TestFamily] +testFamiliesForCodegen codegen = + fmap (\testFamily -> testFamily {tests = IMap.filter f (tests testFamily)}) + testFamilies + where + f mCodegens = case mCodegens of + Just codegens -> Set.member codegen codegens + Nothing -> True + +-- The data to instanciate testFamilies +-- The first column is the id +-- The second column is the proper name (the prefix of the subfolders) +-- The third column is the data for each test +testFamiliesData :: [(String, String, [(Index, CompatCodegen)])] +testFamiliesData = [ + ("base", "Base", + [ ( 1, C_CG )]), + ("basic", "Basic", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, C_CG ), + ( 8, ANY ), + ( 9, ANY ), + ( 10, ANY ), + ( 11, C_CG ), + ( 12, ANY ), + ( 13, ANY ), + ( 14, ANY ), + ( 15, ANY ), + ( 16, ANY ), + ( 17, ANY ), + ( 18, ANY )]), + ("bignum", "Bignum", + [ ( 1, ANY ), + ( 2, ANY )]), + ("bounded", "Bounded", + [ ( 1, ANY )]), + ("corecords", "Corecords", + [ ( 1, ANY ), + ( 2, ANY )]), + ("delab", "De-elaboration", + [ ( 1, ANY )]), + ("directives", "Directives", + [ ( 1, ANY ), + ( 2, ANY )]), + ("disambig", "Disambiguation", + [ ( 2, ANY )]), + ("docs", "Documentation", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY )]), + ("dsl", "DSL", + [ ( 1, ANY ), + ( 2, C_CG ), + ( 3, ANY ), + ( 4, ANY )]), + ("effects", "Effects", + [ ( 1, C_CG ), + ( 2, C_CG ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY )]), + ("error", "Errors", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 8, ANY )]), + ("ffi", "FFI", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, C_CG ), + ( 7, C_CG ), + ( 8, C_CG )]), + ("folding", "Folding", + [ ( 1, ANY )]), + ("idrisdoc", "Idris documentation", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 8, ANY ), + ( 9, ANY )]), + ("interactive", "Interactive editing", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 8, ANY ), + ( 9, ANY ), + ( 10, ANY ), + ( 11, ANY ), + ( 12, ANY ), + ( 13, ANY )]), + ("interfaces", "Interfaces", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY )]), + ("io", "IO monad", + [ ( 1, C_CG ), + ( 2, ANY ), + ( 3, C_CG )]), + ("layout", "Layout", + [ ( 1, ANY )]), + ("literate", "Literate programming", + [ ( 1, ANY )]), + ("meta", "Meta-programming", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY )]), + ("pkg", "Packages", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY )]), + ("prelude", "Prelude", + [ ( 1, ANY )]), + ("primitives", "Primitive types", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 5, C_CG ), + ( 6, C_CG )]), + ("proof", "Theorem proving", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 8, ANY ), + ( 9, ANY ), + ( 10, ANY ), + ( 11, ANY )]), + ("proofsearch", "Proof search", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY )]), + ("pruviloj", "Pruviloj", + [ ( 1, ANY )]), + ("quasiquote", "Quasiquotations", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY )]), + ("records", "Records", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY )]), + ("reg", "Regressions", + [ ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 10, ANY ), + ( 13, ANY ), + ( 16, ANY ), + ( 17, ANY ), + ( 18, ANY ), + ( 20, ANY ), + ( 23, ANY ), + ( 24, ANY ), + ( 25, ANY ), + ( 27, ANY ), + ( 28, ANY ), + ( 29, C_CG ), + ( 31, ANY ), + ( 32, ANY ), + ( 34, ANY ), + ( 35, ANY ), + ( 39, ANY ), + ( 40, ANY ), + ( 41, ANY ), + ( 42, ANY ), + ( 44, ANY ), + ( 45, ANY ), + ( 48, ANY ), + ( 49, ANY ), + ( 50, ANY ), + ( 52, C_CG ), + ( 54, ANY ), + ( 55, ANY ), + ( 56, ANY ), + ( 67, ANY ), + ( 68, ANY ), + ( 69, ANY ), + ( 70, ANY ), + ( 72, ANY ), + ( 75, ANY )]), + ("regression", "Regression (loner)", + [ ( 1 , ANY )]), + ("sourceLocation", "Source location", + [ ( 1 , ANY )]), + ("sugar", "Syntactic sugar", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, C_CG ), + ( 5, ANY )]), + ("syntax", "Syntax extensions", + [ ( 1, ANY ), + ( 2, ANY )]), + ("tactics", "Tactics", + [ ( 1, ANY )]), + ("totality", "Totality checking", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, ANY ), + ( 8, ANY ), + ( 9, ANY ), + ( 10, ANY ), + ( 11, ANY ), + ( 12, ANY ), + ( 13, ANY ), + ( 14, ANY ), + ( 15, ANY )]), + ("tutorial", "Tutorial examples", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY ), + ( 4, ANY ), + ( 5, ANY ), + ( 6, ANY ), + ( 7, C_CG )]), + ("unique", "Uniqueness types", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, ANY )]), + ("universes", "Universes", + [ ( 1, ANY ), + ( 2, ANY )]), + ("views", "Views", + [ ( 1, ANY ), + ( 2, ANY ), + ( 3, C_CG )])] diff --git a/test/TestRun.hs b/test/TestRun.hs new file mode 100644 --- /dev/null +++ b/test/TestRun.hs @@ -0,0 +1,139 @@ +module Main where + +import Control.Monad +import Data.Typeable +import Data.Proxy +import Data.List +import Data.Map.Strict as Map +import Data.IntSet as ISet +import Data.IntMap as IMap +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BSC + +import System.Directory +import System.Environment +import System.Process +import System.Info +import System.IO +import System.FilePath (()) +import Options.Applicative +import Test.Tasty +import Test.Tasty.Golden +import Test.Tasty.Golden.Advanced +import Test.Tasty.Runners +import Test.Tasty.Options +import Test.Tasty.Ingredients.Rerun + +import TestData + +--------------------------------------------------------------------- [ Config ] + +type Flags = [String] + +-- Add arguments to calls of idris executable +idrisFlags :: Flags +idrisFlags = [] + +testDirectory :: String +testDirectory = "test" + +-------------------------------------------------------------------- [ Options ] + +-- The `--node` option makes idris use the node code generator +-- As a consequence, incompatible tests are removed + +newtype NodeOpt = NodeOpt Bool deriving (Eq, Ord, Typeable) + +nodeArg = "node" +nodeHelp = "Performs the tests with the node code generator" +instance IsOption NodeOpt where + defaultValue = NodeOpt False + parseValue = fmap NodeOpt . safeRead + optionName = return nodeArg + optionHelp = return nodeHelp + optionCLParser = fmap NodeOpt $ switch (long nodeArg <> help nodeHelp) + +ingredients :: [Ingredient] +ingredients = defaultIngredients ++ + [rerunningTests [consoleTestReporter], + includingOptions [Option (Proxy :: Proxy NodeOpt)] ] + +----------------------------------------------------------------------- [ Core ] + +-- Compare a given file contents against the golden file contents +-- A ripoff of goldenVsFile from Tasty.Golden +test :: String -> String -> IO () -> TestTree +test name path act = + goldenTest name (readFile ref) (act >> readFile new) cmp upd + where + ref = path "expected" + new = path "output" + cmp x y = return $ if normalize x == normalize y then Nothing + else Just $ printDiff (ref, x) (new, y) + upd = writeFile ref + -- just pretend that backslashes are slashes for comparison + -- purposes to avoid path problems, so don't write any tests + -- that depend on that distinction in other contexts. + -- Also compare CRLF and LF as equal, fixes a weird corner case + -- on Mac where basic010 and reg039 produces CRLF + normalize [] = [] + normalize ('\r':'\n':xs) = '\n' : normalize xs + normalize ('\\':'\\':xs) = '/' : normalize xs + normalize ('\\':xs) = '/' : normalize xs + normalize (x : xs) = x : normalize xs + + +-- Takes the filepath and content of `expected` and `output` +-- and formats an error message stating their difference +printDiff :: (String, String) -> (String, String) -> String +printDiff (ref, x) (new, y) = + let printContent cnt = + if Data.List.null cnt + then " is empty...\n" + else " is: \n" ++ unlines (fmap ((++) " ") (lines cnt)) + in + "Test mismatch!\n" ++ + "Golden file " ++ ref ++ printContent x ++ + "However, " ++ new ++ printContent y + +-- Should always output a 3-charater string from a postive Int +indexToString :: Int -> String +indexToString index = let str = show index in + (replicate (3 - length str) '0') ++ str + +-- Turns the collection of TestFamily into actual tests usable by Tasty +mkGoldenTests :: [TestFamily] -> Flags -> TestTree +mkGoldenTests testFamilies flags = + testGroup "Regression and feature tests" + (fmap mkTestFamily testFamilies) + where + mkTestFamily (TestFamily id name tests) = + testGroup name (fmap (mkTest id) (IMap.keys tests)) + mkTest id index = + let testname = id ++ indexToString index + path = testDirectory testname + in + test testname path (runTest path flags) + +-- Runs a test script +-- "bash" needed because Haskell has cmd as the default shell on windows, and +-- we also want to run the process with another current directory, so we get +-- this thing. +runTest :: String -> Flags -> IO () +runTest path flags = do + let run = (proc "bash" ("run" : flags)) {cwd = Just path, + std_out = CreatePipe, + std_err = CreatePipe} + (_, output, error_out) <- readCreateProcessWithExitCode run "" + writeFile (path "output") output + hPutStrLn stderr error_out + +main :: IO () +main = do + defaultMainWithIngredients ingredients $ + askOption $ \(NodeOpt node) -> + let (codegen, flags) = if node then (JS, ["--codegen", "node"]) + else (C , []) + in + mkGoldenTests (testFamiliesForCodegen codegen) + (flags ++ idrisFlags) diff --git a/test/base001/Makefile b/test/base001/Makefile new file mode 100644 --- /dev/null +++ b/test/base001/Makefile @@ -0,0 +1,11 @@ +.PHONY: +all: exit1 sys.o + +exit1: + @gcc -Wall -o exit1 exit1.c + +sys.o: + @gcc -Wall -c sys.c + +clean: + -@rm exit1 sys.o diff --git a/test/base001/base001.idr b/test/base001/base001.idr new file mode 100644 --- /dev/null +++ b/test/base001/base001.idr @@ -0,0 +1,35 @@ +module Main + +import System + +%include C "sys.h" +%link C "sys.o" + +WIFEXITED : (status : Int) -> IO Bool +WIFEXITED status = do + r <- foreign FFI_C "WIFEXITED_" (Int -> IO Int) status + pure $ r /= 0 + +WEXITSTATUS : (status : Int) -> IO Int +WEXITSTATUS status = foreign FFI_C "WEXITSTATUS_" (Int -> IO Int) status + +execute : (cmd : String) -> (expectedStatus : Int) -> IO () +execute cmd expectedStatus = do + putStrLn "-------------------------------------------" + putStrLn $ "Executing '" ++ cmd ++ "'" + status1 <- system cmd + putStrLn $ "raw status = " ++ show status1 -- XXX: Probably not portable. + exited <- WIFEXITED status1 + if exited + then do + exitStatus <- WEXITSTATUS status1 + putStrLn $ "exit status = " ++ show exitStatus + printLn $ exitStatus == expectedStatus + else pure () + putStrLn "" + +main : IO () +main = do + execute "exit 1" 1 + execute "./exit1" 1 + execute "./does-not-exist" 127 diff --git a/test/base001/base001.ipkg b/test/base001/base001.ipkg new file mode 100644 --- /dev/null +++ b/test/base001/base001.ipkg @@ -0,0 +1,5 @@ +package base001 + +executable = base001 +main = base001 +makefile = Makefile diff --git a/test/base001/exit1.c b/test/base001/exit1.c new file mode 100644 --- /dev/null +++ b/test/base001/exit1.c @@ -0,0 +1,17 @@ +#include +#include + +void doSystem(const char cmd[]) { + printf("exit1: Executing cmd '%s'\n", cmd); + int exitStatus = system(cmd); + printf("exit1: raw exitStatus = %d\n", exitStatus); // XXX: Probably not portable (hide from expected file). + if (WIFEXITED(exitStatus)) { + printf("exit1: WEXITSTATUS(exitStatus) = %d\n", WEXITSTATUS(exitStatus)); + } +} + +int main() { + doSystem("exit 1"); + doSystem("./does-not-exist"); + return 1; +} diff --git a/test/base001/expected b/test/base001/expected new file mode 100644 --- /dev/null +++ b/test/base001/expected @@ -0,0 +1,25 @@ +Type checking ./base001.idr +exit1: Executing cmd 'exit 1' +exit1: raw exitStatus = 256 +exit1: WEXITSTATUS(exitStatus) = 1 +exit1: Executing cmd './does-not-exist' +exit1: raw exitStatus = 32512 +exit1: WEXITSTATUS(exitStatus) = 127 +------------------------------------------- +Executing 'exit 1' +raw status = 256 +exit status = 1 +True + +------------------------------------------- +Executing './exit1' +raw status = 256 +exit status = 1 +True + +------------------------------------------- +Executing './does-not-exist' +raw status = 32512 +exit status = 127 +True + diff --git a/test/base001/run b/test/base001/run new file mode 100644 --- /dev/null +++ b/test/base001/run @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +if [[ ${OSTYPE} = 'msys' ]]; then + cat expected # skip this test on Windows +else + ${IDRIS:-idris} $@ --build base001.ipkg | grep -v 'make.*:' + ./base001 + make clean | grep -v 'make.*:' + rm -f *.ibc base001 +fi diff --git a/test/base001/sys.c b/test/base001/sys.c new file mode 100644 --- /dev/null +++ b/test/base001/sys.c @@ -0,0 +1,11 @@ +#include "sys.h" + +#include + +int WIFEXITED_(int status) { + return WIFEXITED(status); +} + +int WEXITSTATUS_(int status) { + return WEXITSTATUS(status); +} diff --git a/test/base001/sys.h b/test/base001/sys.h new file mode 100644 --- /dev/null +++ b/test/base001/sys.h @@ -0,0 +1,7 @@ +#ifndef SYS_H +#define SYS_H + +int WIFEXITED_(int status); +int WEXITSTATUS_(int status); + +#endif diff --git a/test/basic010/run b/test/basic010/run --- a/test/basic010/run +++ b/test/basic010/run @@ -8,7 +8,7 @@ done if (which timeout&>/dev/null); then - timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010 + timeout 10 ${IDRIS:-idris} $@ Main.idr --nocolour --check --warnreach -o basic010 timeout 5 ./basic010 else # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting @@ -35,7 +35,7 @@ } - timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010" + timeout 10 "${IDRIS:-idris} ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010" timeout 5 "./basic010" fi rm -f *.ibc basic010 diff --git a/test/basic013/basic013.idr b/test/basic013/basic013.idr --- a/test/basic013/basic013.idr +++ b/test/basic013/basic013.idr @@ -31,4 +31,13 @@ putStrLn ("Tail Tail: " ++ strTail (strTail newstr)) putStrLn ("Cons: " ++ strCons 'λ' newstr) putStrLn ("Reverse: " ++ reverse newstr) + printLn [1..5] + printLn [5..1] + printLn [(-9), (-7)..(-1)] + printLn [17,15..1] + printLn [19,15..2] + printLn $ the (List Nat) [1..5] + printLn $ the (List Nat) [5..1] + printLn $ the (List Int) [(-1)..(-5)] + printLn $ the (List Nat) [1,3..5] diff --git a/test/basic013/expected b/test/basic013/expected --- a/test/basic013/expected +++ b/test/basic013/expected @@ -12,3 +12,12 @@ Tail Tail: →xλx→xλx→xλx→xλx→x Cons: λλx→xλx→xλx→xλx→xλx→x Reverse: x→xλx→xλx→xλx→xλx→xλ +[1, 2, 3, 4, 5] +[5, 4, 3, 2, 1] +[-9, -7, -5, -3, -1] +[17, 15, 13, 11, 9, 7, 5, 3, 1] +[19, 15, 11, 7, 3] +[1, 2, 3, 4, 5] +[5, 4, 3, 2, 1] +[-1, -2, -3, -4, -5] +[1, 3, 5] diff --git a/test/bounded001/bounded001.idr b/test/bounded001/bounded001.idr new file mode 100644 --- /dev/null +++ b/test/bounded001/bounded001.idr @@ -0,0 +1,10 @@ +module Main + +-- Test wraparound from upper bounds of Bits types +main : IO () +main = do putStrLn (show $ the Bits16 maxBound) + putStrLn (show $ the Bits16 maxBound + 1) + putStrLn (show $ the Bits32 maxBound) + putStrLn (show $ the Bits32 maxBound + 1) + putStrLn (show $ the Bits64 maxBound) + putStrLn (show $ the Bits64 maxBound + 1) diff --git a/test/bounded001/expected b/test/bounded001/expected new file mode 100644 --- /dev/null +++ b/test/bounded001/expected @@ -0,0 +1,6 @@ +FFFF +0000 +FFFFFFFF +00000000 +FFFFFFFFFFFFFFFF +0000000000000000 diff --git a/test/bounded001/run b/test/bounded001/run new file mode 100644 --- /dev/null +++ b/test/bounded001/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ bounded001.idr -o bounded001 +./bounded001 +rm -f bounded001 *.ibc diff --git a/test/disambig002/disambig002.idr b/test/disambig002/disambig002.idr --- a/test/disambig002/disambig002.idr +++ b/test/disambig002/disambig002.idr @@ -2,6 +2,8 @@ import Data.Fin import Control.Isomorphism +-- Tests if Idris can disambiguate between the three `toVect` operators + Dec0 : Type -> Type Dec0 = Dec diff --git a/test/docs001/run b/test/docs001/run --- a/test/docs001/run +++ b/test/docs001/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolor docs001.idr < input +${IDRIS:-idris} $@ --quiet --nocolor docs001.idr < input rm *.ibc diff --git a/test/docs002/run b/test/docs002/run --- a/test/docs002/run +++ b/test/docs002/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nobanner --nocolor --quiet docs002.idr < input +${IDRIS:-idris} $@ --nobanner --nocolor --quiet docs002.idr < input rm *.ibc diff --git a/test/docs003/run b/test/docs003/run --- a/test/docs003/run +++ b/test/docs003/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolor docs003.idr < input +${IDRIS:-idris} $@ --quiet --nocolor docs003.idr < input rm *.ibc diff --git a/test/docs004/run b/test/docs004/run --- a/test/docs004/run +++ b/test/docs004/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolor docs004.idr < input +${IDRIS:-idris} $@ --quiet --nocolor docs004.idr < input rm *.ibc diff --git a/test/docs005/run b/test/docs005/run --- a/test/docs005/run +++ b/test/docs005/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolor docs005.idr < input +${IDRIS:-idris} $@ --quiet --nocolor docs005.idr < input rm *.ibc diff --git a/test/effects001/run b/test/effects001/run --- a/test/effects001/run +++ b/test/effects001/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash -${IDRIS:-idris} -p effects $@ test021.idr -o test021 -${IDRIS:-idris} -p effects $@ test021a.idr -o test021a +${IDRIS:-idris} $@ -p effects test021.idr -o test021 +${IDRIS:-idris} $@ -p effects test021a.idr -o test021a ./test021 ./test021a rm -f test021 test021a *.ibc diff --git a/test/effects002/run b/test/effects002/run --- a/test/effects002/run +++ b/test/effects002/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash -${IDRIS:-idris} -p effects $@ test025.idr -o test025 +${IDRIS:-idris} $@ -p effects test025.idr -o test025 ./test025 rm -f test025 *.ibc diff --git a/test/ffi001/run b/test/ffi001/run --- a/test/ffi001/run +++ b/test/ffi001/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolour test022.idr --exec main +${IDRIS:-idris} $@ --quiet --nocolour test022.idr --exec main rm -f *.ibc diff --git a/test/ffi002/run b/test/ffi002/run --- a/test/ffi002/run +++ b/test/ffi002/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet test023.idr -o test023 +${IDRIS:-idris} $@ --quiet test023.idr -o test023 rm -f test023 *.ibc diff --git a/test/ffi003/run b/test/ffi003/run --- a/test/ffi003/run +++ b/test/ffi003/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolour test024.idr --exec main < input +${IDRIS:-idris} $@ --quiet --nocolour test024.idr --exec main < input rm -f *.ibc diff --git a/test/ffi004/run b/test/ffi004/run --- a/test/ffi004/run +++ b/test/ffi004/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nocolour --check test026.idr +${IDRIS:-idris} $@ --quiet --nocolour --check test026.idr rm -f *.ibc diff --git a/test/ffi006/run b/test/ffi006/run --- a/test/ffi006/run +++ b/test/ffi006/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash ${IDRIS:-idris} $@ ffi006.idr --interface -o ffi006.o -${CC:=cc} ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006 +${CC:=cc} ffi006.c ffi006.o `${IDRIS:-idris} $@ --include` `${IDRIS:-idris} $@ --link` -o ffi006 ./ffi006 rm -f ffi006 *.ibc *.o *.h diff --git a/test/idrisdoc001/run b/test/idrisdoc001/run --- a/test/idrisdoc001/run +++ b/test/idrisdoc001/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash # Tests that no documentation is built for empty and/or private-only namespaces -${IDRIS:-idris} --mkdoc test_empty.ipkg +${IDRIS:-idris} $@ --mkdoc test_empty.ipkg rm -rf *.ibc *_doc diff --git a/test/idrisdoc002/run b/test/idrisdoc002/run --- a/test/idrisdoc002/run +++ b/test/idrisdoc002/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for functions -${IDRIS:-idris} --mkdoc test_functions.ipkg +${IDRIS:-idris} $@ --mkdoc test_functions.ipkg [ -d test_functions_doc ] && echo "Functions are documented" rm -rf *.ibc *_doc diff --git a/test/idrisdoc003/run b/test/idrisdoc003/run --- a/test/idrisdoc003/run +++ b/test/idrisdoc003/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for data types -${IDRIS:-idris} --mkdoc test_datatypes.ipkg +${IDRIS:-idris} $@ --mkdoc test_datatypes.ipkg [ -d test_datatypes_doc ] && echo "Data types are documented" rm -rf *.ibc *_doc diff --git a/test/idrisdoc004/run b/test/idrisdoc004/run --- a/test/idrisdoc004/run +++ b/test/idrisdoc004/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash # Tests that documentation is generated for typeclasses -${IDRIS:-idris} --mkdoc test_typeclasses.ipkg +${IDRIS:-idris} $@ --mkdoc test_typeclasses.ipkg [ -d test_typeclasses_doc ] && echo "Typeclasses are documented" rm -rf *.ibc *_doc diff --git a/test/idrisdoc005/run b/test/idrisdoc005/run --- a/test/idrisdoc005/run +++ b/test/idrisdoc005/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that references to other namespaces are traced -${IDRIS:-idris} --mkdoc test_tracing.ipkg +${IDRIS:-idris} $@ --mkdoc test_tracing.ipkg [ -f test_tracing_doc/docs/TestTracing.html ] && echo "TestTracing: Check" [ -f test_tracing_doc/docs/Prelude.Bool.html ] && echo "Prelude.Bool: Check" rm -rf *.ibc *_doc diff --git a/test/idrisdoc006/run b/test/idrisdoc006/run --- a/test/idrisdoc006/run +++ b/test/idrisdoc006/run @@ -1,8 +1,8 @@ #!/usr/bin/env bash # Tests that documentation properly is merged with existent. -${IDRIS:-idris} --mkdoc package_a.ipkg +${IDRIS:-idris} $@ --mkdoc package_a.ipkg [ -f test_merge_doc/IdrisDoc ] && echo "IdrisDoc file written" -${IDRIS:-idris} --mkdoc package_b.ipkg +${IDRIS:-idris} $@ --mkdoc package_b.ipkg ls -1p test_merge_doc/docs if grep -q "href\\=\"docs/A.fully.Qualified.NAME\\.html\"" test_merge_doc/index.html; then echo A.fully.Qualified.NAME is in the index diff --git a/test/idrisdoc007/run b/test/idrisdoc007/run --- a/test/idrisdoc007/run +++ b/test/idrisdoc007/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that documentation only is written when safe mkdir do_not_delete_doc -${IDRIS:-idris} --mkdoc package.ipkg > nowhere +${IDRIS:-idris} $@ --mkdoc package.ipkg > nowhere echo Exit status \(expects 1\): $? rm -rf do_not_delete_doc *.ibc nowhere diff --git a/test/idrisdoc008/run b/test/idrisdoc008/run --- a/test/idrisdoc008/run +++ b/test/idrisdoc008/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash # Tests that documentation is generated for both public and abstract members. -${IDRIS:-idris} --mkdoc visibility.ipkg +${IDRIS:-idris} $@ --mkdoc visibility.ipkg [ -f visibility_doc/docs/Abstract.html ] && echo "Abstract members are documented" [ -f visibility_doc/docs/Visible.html ] && echo "Public members are documented" rm -rf *.ibc *_doc diff --git a/test/interactive001/run b/test/interactive001/run --- a/test/interactive001/run +++ b/test/interactive001/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet test032.idr < input +${IDRIS:-idris} $@ --quiet test032.idr < input rm -f *.ibc diff --git a/test/interactive002/run b/test/interactive002/run --- a/test/interactive002/run +++ b/test/interactive002/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive002.idr < input +${IDRIS:-idris} $@ --quiet interactive002.idr < input rm -f *.ibc diff --git a/test/interactive003/run b/test/interactive003/run --- a/test/interactive003/run +++ b/test/interactive003/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive003.idr < input +${IDRIS:-idris} $@ --quiet interactive003.idr < input rm -f *.ibc diff --git a/test/interactive004/run b/test/interactive004/run --- a/test/interactive004/run +++ b/test/interactive004/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive004.idr < input +${IDRIS:-idris} $@ --quiet interactive004.idr < input rm -f *.ibc diff --git a/test/interactive005/run b/test/interactive005/run --- a/test/interactive005/run +++ b/test/interactive005/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --quiet interactive005.idr --consolewidth 70 < input +${IDRIS:-idris} $@ --nocolour --quiet interactive005.idr --consolewidth 70 < input rm -f *.ibc rm -f hello.bytecode rm -f hello diff --git a/test/interactive006/run b/test/interactive006/run --- a/test/interactive006/run +++ b/test/interactive006/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --port 5000 interactive006.idr < input +${IDRIS:-idris} $@ --quiet --port 5000 interactive006.idr < input rm -f *.ibc diff --git a/test/interactive007/run b/test/interactive007/run --- a/test/interactive007/run +++ b/test/interactive007/run @@ -1,2 +1,2 @@ #!/usr/bin/env bash -${IDRIS:-idris} -p contrib --nobanner --nocolor < input +${IDRIS:-idris} $@ -p contrib --nobanner --nocolor < input diff --git a/test/interactive008/run b/test/interactive008/run --- a/test/interactive008/run +++ b/test/interactive008/run @@ -1,2 +1,2 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nobanner --nocolor < input +${IDRIS:-idris} $@ --nobanner --nocolor < input diff --git a/test/interactive009/run b/test/interactive009/run --- a/test/interactive009/run +++ b/test/interactive009/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive009.idr < input +${IDRIS:-idris} $@ --quiet interactive009.idr < input rm -f *.ibc diff --git a/test/interactive010/run b/test/interactive010/run --- a/test/interactive010/run +++ b/test/interactive010/run @@ -1,2 +1,2 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet --nobanner --nocolor < input +${IDRIS:-idris} $@ --quiet --nobanner --nocolor < input diff --git a/test/interactive011/run b/test/interactive011/run --- a/test/interactive011/run +++ b/test/interactive011/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive011.idr < input +${IDRIS:-idris} $@ --quiet interactive011.idr < input rm -f *.ibc diff --git a/test/interactive012/run b/test/interactive012/run --- a/test/interactive012/run +++ b/test/interactive012/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --consolewidth 70 --quiet interactive012.idr < input +${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet interactive012.idr < input rm -f *.ibc diff --git a/test/interactive013/run b/test/interactive013/run --- a/test/interactive013/run +++ b/test/interactive013/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet interactive013.idr < input +${IDRIS:-idris} $@ --quiet interactive013.idr < input rm -f *.ibc diff --git a/test/layout001/expected b/test/layout001/expected new file mode 100644 --- /dev/null +++ b/test/layout001/expected @@ -0,0 +1,93 @@ +Checking layout001a.idr +./layout001a.idr:5:1: error: Wrong + indention: should be greater + than context + indentation, expected: space +y +^ +Checking layout001b.idr +./layout001b.idr:5:3: error: Wrong + indention: should be greater + than context + indentation, expected: space += y + ^ +Checking layout001c.idr +./layout001c.idr:3:1: error: Wrong + indention: should be greater + than context + indentation, expected: space +2 +^ +Checking layout001d.idr +Checking layout001e.idr +./layout001e.idr:6:1: error: Wrong + indention: should be greater + than context + indentation, expected: space +3 +^ +Checking layout001f.idr +./layout001f.idr:6:2: error: Wrong + indention: should be greater + than context + indentation, expected: space + 3 + ^ +Checking layout001g.idr +./layout001g.idr:6:3: error: Wrong + indention: should be greater + than context + indentation, expected: space + 3 + ^ +Checking layout001h.idr +./layout001h.idr:6:3: error: Wrong + indention: should be greater + than context + indentation, expected: space + 3 + ^ +Checking layout001i.idr +./layout001i.idr:6:4: error: Wrong + indention: should be greater + than context + indentation, expected: space + 3 + ^ +Checking layout001j.idr +./layout001j.idr:6:5: error: Wrong + indention: should be greater + than context + indentation, expected: space + 3 + ^ +Checking layout001k.idr +Checking layout001l.idr +./layout001l.idr:6:1: error: Wrong + indention: should be greater + than context + indentation, expected: space +y +^ +Checking layout001n.idr +Checking mplus1.idr +mplus1.idr:13:31: +When checking right hand side of term with expected type + Maybe Int + +When checking an application of function Prelude.Applicative.pure: + No such variable f +Checking mplus2.idr +./mplus2.idr:17:37: error: not + end of block, expected: ")", + "->", ";", "in", + ambiguous use of a left-associative operator, + ambiguous use of a non-associative operator, + ambiguous use of a right-associative operator, + do block expression, + end of input + `mplus` pure f + ^ +Checking mplus3.idr +mplus3.idr:11:1:warning - Unreachable case: term diff --git a/test/layout001/layout001a.idr b/test/layout001/layout001a.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001a.idr @@ -0,0 +1,5 @@ +f : Int -> Int +f x = z 1 + 1 where + z : Int -> Int + z y = +y diff --git a/test/layout001/layout001b.idr b/test/layout001/layout001b.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001b.idr @@ -0,0 +1,5 @@ +f : Int -> Int +f x = z 1 + 1 where + z : Int -> Int + z y += y diff --git a/test/layout001/layout001c.idr b/test/layout001/layout001c.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001c.idr @@ -0,0 +1,3 @@ +f : Int +f = +2 diff --git a/test/layout001/layout001d.idr b/test/layout001/layout001d.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001d.idr @@ -0,0 +1,3 @@ +f : Int +f += 2 diff --git a/test/layout001/layout001e.idr b/test/layout001/layout001e.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001e.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + +3 diff --git a/test/layout001/layout001f.idr b/test/layout001/layout001f.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001f.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001g.idr b/test/layout001/layout001g.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001g.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001h.idr b/test/layout001/layout001h.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001h.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001i.idr b/test/layout001/layout001i.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001i.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001j.idr b/test/layout001/layout001j.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001j.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001k.idr b/test/layout001/layout001k.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001k.idr @@ -0,0 +1,6 @@ +foo : Int -> Int +foo a = a + b + where + b : Int + b = 2 + + 3 diff --git a/test/layout001/layout001l.idr b/test/layout001/layout001l.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001l.idr @@ -0,0 +1,6 @@ +f : Int -> Int +f x = z 1 + 1 + where + z : Int -> Int + z y = +y diff --git a/test/layout001/layout001n.idr b/test/layout001/layout001n.idr new file mode 100644 --- /dev/null +++ b/test/layout001/layout001n.idr @@ -0,0 +1,33 @@ +module NonLayout + +{- +Haskell and Idris use indentation for grouping in the concrete syntax. +How this works is defined as an automatic translation to the equivalent +syntax using { ; and }, which you are free to use yourself. + +In Idris specifically, if let or where is followed by { then indentation no +longer matters for the following definitions until a balanced } appears. To +put multiple declarations on one line within the { } you put semicolons between +them: one ; for let declarations and ;; for where declarations. Whether this +discrepancy is a bug I don't know. +-} + +average : String -> Double +average str = answer where + wordCount : String -> Nat + wordCount str = length (words str) + wordLengths : List String -> List Nat + wordLengths strs = map length strs + answer = + let numWords = wordCount str in + let totalLength = sum (wordLengths (words str)) in + cast totalLength / cast numWords + +average' : String -> Double +average' str = answer where { + wordCount : String -> Nat ;; wordCount str = length (words str) + wordLengths : List String -> List Nat ;; wordLengths strs = map length strs + answer = let { + numWords = wordCount str; totalLength = sum (wordLengths (words str)) + } in cast totalLength / cast numWords +} diff --git a/test/layout001/mplus1.idr b/test/layout001/mplus1.idr new file mode 100644 --- /dev/null +++ b/test/layout001/mplus1.idr @@ -0,0 +1,17 @@ +mplus : Maybe a -> Maybe a -> Maybe a +mplus a b = ?mplus_rhs + +factor : Maybe Int +factor = ?term_rhs + +symbol : String -> Maybe Int +symbol = ?symbol_rhs + +term : Maybe Int +term = ?term_rhs + +term = do f <- factor + do symbol "*" + t <- term + pure (f * t) + `mplus` pure f diff --git a/test/layout001/mplus2.idr b/test/layout001/mplus2.idr new file mode 100644 --- /dev/null +++ b/test/layout001/mplus2.idr @@ -0,0 +1,17 @@ +mplus : Maybe a -> Maybe a -> Maybe a +mplus a b = ?mplus_rhs + +factor : Maybe Int +factor = ?term_rhs + +symbol : String -> Maybe Int +symbol = ?symbol_rhs + +term : Maybe Int +term = ?term_rhs + +term = do f <- factor + do symbol "*" + t <- term + pure (f * t) + `mplus` pure f diff --git a/test/layout001/mplus3.idr b/test/layout001/mplus3.idr new file mode 100644 --- /dev/null +++ b/test/layout001/mplus3.idr @@ -0,0 +1,17 @@ +mplus : Maybe a -> Maybe a -> Maybe a +mplus a b = ?mplus_rhs + +factor : Maybe Int +factor = ?term_rhs + +symbol : String -> Maybe Int +symbol = ?symbol_rhs + +term : Maybe Int +term = ?term_rhs + +term = do f <- factor + do symbol "*" + t <- term + pure (f * t) + `mplus` pure f diff --git a/test/layout001/run b/test/layout001/run new file mode 100644 --- /dev/null +++ b/test/layout001/run @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +for file in *.idr; do + echo Checking ${file} + ${IDRIS:-idris} --check $@ ${file} +done + +rm -f *.ibc diff --git a/test/meta002/run b/test/meta002/run --- a/test/meta002/run +++ b/test/meta002/run @@ -3,5 +3,5 @@ ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr # Disabled due to excess memory consumption -# idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr +# ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr rm -f *.ibc diff --git a/test/meta003/BadDef.idr b/test/meta003/BadDef.idr new file mode 100644 --- /dev/null +++ b/test/meta003/BadDef.idr @@ -0,0 +1,12 @@ +module BadDef + +import Language.Reflection.Elab + +mkN : String -> TTName +mkN n = NS (UN n) ["BadDef"] + +mkBadDef1 : Elab () +mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ()) + defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")] + +%runElab mkBadDef1 diff --git a/test/meta003/expected b/test/meta003/expected new file mode 100644 --- /dev/null +++ b/test/meta003/expected @@ -0,0 +1,6 @@ +BadDef.idr:12:1-9: +While running an elaboration script, the following error occurred: +Type mismatch between + () +and + String diff --git a/test/meta003/run b/test/meta003/run new file mode 100644 --- /dev/null +++ b/test/meta003/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr +rm -f *.ibc diff --git a/test/pkg002/Main.idr b/test/pkg002/Main.idr new file mode 100644 --- /dev/null +++ b/test/pkg002/Main.idr @@ -0,0 +1,4 @@ +module Main + +main : IO () +main = putStrLn "CouCou!" diff --git a/test/pkg002/expected b/test/pkg002/expected new file mode 100644 --- /dev/null +++ b/test/pkg002/expected diff --git a/test/pkg002/run b/test/pkg002/run new file mode 100644 --- /dev/null +++ b/test/pkg002/run @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +### Test: IPKG executable names can be any namespaced identifier. +${IDRIS:-idris} $@ --build test.ipkg +rm -f *.ibc +rm -f some.namespaced.identifier diff --git a/test/pkg002/test.ipkg b/test/pkg002/test.ipkg new file mode 100644 --- /dev/null +++ b/test/pkg002/test.ipkg @@ -0,0 +1,8 @@ +package test + +modules = Main + + +opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80" +main = Main +executable = some.namespaced.identifier diff --git a/test/pkg003/Main.idr b/test/pkg003/Main.idr new file mode 100644 --- /dev/null +++ b/test/pkg003/Main.idr @@ -0,0 +1,4 @@ +module Main + +main : IO () +main = putStrLn "CouCou!" diff --git a/test/pkg003/expected b/test/pkg003/expected new file mode 100644 --- /dev/null +++ b/test/pkg003/expected diff --git a/test/pkg003/run b/test/pkg003/run new file mode 100644 --- /dev/null +++ b/test/pkg003/run @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +### Test: IPKG executable names can be a quoted string +### containing a valid filename. +${IDRIS:-idris} $@ --build test.ipkg +rm -f *.ibc +rm -f 'quoting-allows-hyphens and spaces and fun stuff!' diff --git a/test/pkg003/test.ipkg b/test/pkg003/test.ipkg new file mode 100644 --- /dev/null +++ b/test/pkg003/test.ipkg @@ -0,0 +1,7 @@ +package test + +modules = Main + +opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80" +main = Main +executable = "quoting-allows-hyphens and spaces and fun stuff!" diff --git a/test/pkg004/Main.idr b/test/pkg004/Main.idr new file mode 100644 --- /dev/null +++ b/test/pkg004/Main.idr @@ -0,0 +1,4 @@ +module Main + +main : IO () +main = putStrLn "CouCou!" diff --git a/test/pkg004/expected b/test/pkg004/expected new file mode 100644 --- /dev/null +++ b/test/pkg004/expected @@ -0,0 +1,5 @@ +Uncaught error: user error (test.ipkg:9:1: error: filename + must contain no directory + component, expected: space + +^ ) diff --git a/test/pkg004/run b/test/pkg004/run new file mode 100644 --- /dev/null +++ b/test/pkg004/run @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +### Test: IPKG executable names CANNOT include a directory separator. +# TODO: Verify that a name like "a/b\c" is rejected by both *NIX and Windows +# (assuming these tests get run on Windows). +${IDRIS:-idris} $@ --build test.ipkg +rm -f *.ibc diff --git a/test/pkg004/test.ipkg b/test/pkg004/test.ipkg new file mode 100644 --- /dev/null +++ b/test/pkg004/test.ipkg @@ -0,0 +1,8 @@ +package test + +modules = Main + +opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80" + +main = Main +executable = "filenames/cannot include\a directory separator" diff --git a/test/pkg005/expected b/test/pkg005/expected new file mode 100644 --- /dev/null +++ b/test/pkg005/expected @@ -0,0 +1,1 @@ +Can't build an executable: No main module given diff --git a/test/pkg005/run b/test/pkg005/run new file mode 100644 --- /dev/null +++ b/test/pkg005/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +### Test: Build IPKG, executable without main. +${IDRIS:-idris} $@ --build test.ipkg diff --git a/test/pkg005/test.ipkg b/test/pkg005/test.ipkg new file mode 100644 --- /dev/null +++ b/test/pkg005/test.ipkg @@ -0,0 +1,3 @@ +package test + +executable = test diff --git a/test/pkg006/expected b/test/pkg006/expected new file mode 100644 --- /dev/null +++ b/test/pkg006/expected @@ -0,0 +1,1 @@ +Can't start REPL: no main module given diff --git a/test/pkg006/run b/test/pkg006/run new file mode 100644 --- /dev/null +++ b/test/pkg006/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +### Test: Launch REPL, IPKG executable without main. +${IDRIS:-idris} $@ --repl test.ipkg diff --git a/test/pkg006/test.ipkg b/test/pkg006/test.ipkg new file mode 100644 --- /dev/null +++ b/test/pkg006/test.ipkg @@ -0,0 +1,3 @@ +package test + +executable = test diff --git a/test/prelude001/expected b/test/prelude001/expected new file mode 100644 --- /dev/null +++ b/test/prelude001/expected @@ -0,0 +1,10 @@ +True +True +True +True +True +True +True +True +True +True diff --git a/test/prelude001/prelude001.idr b/test/prelude001/prelude001.idr new file mode 100644 --- /dev/null +++ b/test/prelude001/prelude001.idr @@ -0,0 +1,17 @@ +module Main + +main : IO () +main = do + printLn $ lines "" == [] + -- `lines` seems to ignore too many trailing newlines. + printLn $ lines "\n" == [] -- FIXME: Should be [""]. + printLn $ lines "\n\n" == [] -- FIXME: Should be ["", ""]. + printLn $ lines "\n\n\n" == [] -- FIXME: Should be ["", "", ""]. + printLn $ lines "1\n2\n3" == ["1", "2", "3"] + printLn $ lines "1\n2\n3\n" == ["1", "2", "3"] + printLn $ unlines [] == "" + -- `unlines` works as advertised doesn't follow Haskell here. + -- When files are written using unlines, vim complains of "noeoln". + printLn $ unlines ["1"] == "1" -- FIXME: Should be "1\n" + printLn $ unlines ["1", "2"] == "1\n2" -- FIXME: Should be "1\n2\n" + printLn $ unlines ["1", "2", "3"] == "1\n2\n3" -- FIXME: Should be "1\n2\n3\n" diff --git a/test/prelude001/run b/test/prelude001/run new file mode 100644 --- /dev/null +++ b/test/prelude001/run @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +${IDRIS:-idris} $@ prelude001.idr -o prelude001 +./prelude001 +rm -f prelude001 *.ibc diff --git a/test/primitives002/run b/test/primitives002/run --- a/test/primitives002/run +++ b/test/primitives002/run @@ -48,7 +48,7 @@ do echo ${T%% *} ${T##*#} generate_testfile "tmptest.idr" "${T%%#*}" - idris "$@" --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}" + ${IDRIS:-idris} $@ --quiet tmptest.idr -o tmptest || echo "missing primitive in ${CG}" ./tmptest <<<"${T##*#}" rm tmptest.idr tmptest.ibc tmptest done diff --git a/test/proof004/run b/test/proof004/run --- a/test/proof004/run +++ b/test/proof004/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check $@ test035.idr +${IDRIS:-idris} $@ --check test035.idr rm -f *.ibc diff --git a/test/proof005/run b/test/proof005/run --- a/test/proof005/run +++ b/test/proof005/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check $@ DefaultArgSubstitutionSuccess.idr +${IDRIS:-idris} $@ --check DefaultArgSubstitutionSuccess.idr rm -f *.ibc diff --git a/test/proof006/run b/test/proof006/run --- a/test/proof006/run +++ b/test/proof006/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check $@ DefaultArgSubstitutionSyntax.idr +${IDRIS:-idris} $@ --check DefaultArgSubstitutionSyntax.idr rm -f *.ibc diff --git a/test/proof007/run b/test/proof007/run --- a/test/proof007/run +++ b/test/proof007/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check $@ DefaultArgUnknownName.idr +${IDRIS:-idris} $@ --nocolour --check DefaultArgUnknownName.idr rm -f *.ibc diff --git a/test/proof008/run b/test/proof008/run --- a/test/proof008/run +++ b/test/proof008/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check $@ ClaimAndUnfocus.idr +${IDRIS:-idris} $@ --nocolour --check ClaimAndUnfocus.idr rm -f *.ibc diff --git a/test/proofsearch003/run b/test/proofsearch003/run --- a/test/proofsearch003/run +++ b/test/proofsearch003/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check proofsearch003.idr +${IDRIS:-idris} $@ --check proofsearch003.idr rm -f *.ibc diff --git a/test/reg002/run b/test/reg002/run --- a/test/reg002/run +++ b/test/reg002/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash -${IDRIS:-idris} reg012.idr -o reg012 +${IDRIS:-idris} $@ reg012.idr -o reg012 ./reg012 rm -f reg012 *.ibc diff --git a/test/reg003/run b/test/reg003/run --- a/test/reg003/run +++ b/test/reg003/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check reg003.idr -${IDRIS:-idris} --check reg003a.idr +${IDRIS:-idris} $@ --check reg003.idr +${IDRIS:-idris} $@ --check reg003a.idr rm -f *.ibc diff --git a/test/reg007/run b/test/reg007/run --- a/test/reg007/run +++ b/test/reg007/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check $@ reg007.lidr +${IDRIS:-idris} $@ --nocolour --check reg007.lidr rm -f *.ibc diff --git a/test/reg023/run b/test/reg023/run --- a/test/reg023/run +++ b/test/reg023/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ reg023.idr --check +${IDRIS:-idris} $@ --nocolour reg023.idr --check rm -f *.ibc diff --git a/test/reg034/run b/test/reg034/run --- a/test/reg034/run +++ b/test/reg034/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check reg034.idr +${IDRIS:-idris} $@ --nocolour --check reg034.idr rm -f reg034 *.ibc diff --git a/test/reg035/run b/test/reg035/run --- a/test/reg035/run +++ b/test/reg035/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check reg035.idr -${IDRIS:-idris} --nocolour --check reg035a.lidr -${IDRIS:-idris} --nocolour --check reg035b.idr +${IDRIS:-idris} $@ --nocolour --check reg035.idr +${IDRIS:-idris} $@ --nocolour --check reg035a.lidr +${IDRIS:-idris} $@ --nocolour --check reg035b.idr rm -f *.ibc diff --git a/test/reg039/run b/test/reg039/run --- a/test/reg039/run +++ b/test/reg039/run @@ -7,7 +7,7 @@ extraargs=("${extraargs[@]}" "'$arg'") done if (which timeout&>/dev/null); then - timeout 60 idris $@ --nocolour reg039.idr --exec go + timeout 60 ${IDRIS:-idris} $@ --nocolour reg039.idr --exec go else # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting # Executes command with a timeout @@ -30,6 +30,6 @@ fi } - timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go" + timeout 60 "${IDRIS:-idris} ${extraargs[*]} --nocolour reg039.idr --exec go" fi rm -f reg039 *.ibc diff --git a/test/reg040/run b/test/reg040/run --- a/test/reg040/run +++ b/test/reg040/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash -${IDRIS:-idris} --warnreach reg040.idr -o reg040 +${IDRIS:-idris} $@ --warnreach reg040.idr -o reg040 ./reg040 rm -f reg040 *.ibc diff --git a/test/reg044/run b/test/reg044/run --- a/test/reg044/run +++ b/test/reg044/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour reg044.idr --check +${IDRIS:-idris} $@ --nocolour reg044.idr --check rm -f *.ibc diff --git a/test/reg049/run b/test/reg049/run --- a/test/reg049/run +++ b/test/reg049/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check $@ reg049.idr +${IDRIS:-idris} $@ --nocolour --check $@ reg049.idr rm -f *.ibc diff --git a/test/reg050/run b/test/reg050/run --- a/test/reg050/run +++ b/test/reg050/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour --check $@ working.idr -${IDRIS:-idris} --nocolour --check $@ badbangop.idr -${IDRIS:-idris} --nocolour --check $@ baddoublebang.idr +${IDRIS:-idris} $@ --nocolour --check working.idr +${IDRIS:-idris} $@ --nocolour --check badbangop.idr +${IDRIS:-idris} $@ --nocolour --check baddoublebang.idr rm -f *.ibc diff --git a/test/reg054/run b/test/reg054/run --- a/test/reg054/run +++ b/test/reg054/run @@ -1,2 +1,2 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ reg054.idr --check +${IDRIS:-idris} $@ --nocolour reg054.idr --check diff --git a/test/reg055/run b/test/reg055/run --- a/test/reg055/run +++ b/test/reg055/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ reg055.idr --check -${IDRIS:-idris} --nocolour $@ reg055a.idr --check +${IDRIS:-idris} $@ --nocolour reg055.idr --check +${IDRIS:-idris} $@ --nocolour reg055a.idr --check rm -f *.ibc diff --git a/test/reg075/run b/test/reg075/run --- a/test/reg075/run +++ b/test/reg075/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --quiet reg075.idr < input +${IDRIS:-idris} $@ --quiet reg075.idr < input rm -f *.ibc diff --git a/test/runtest.hs b/test/runtest.hs deleted file mode 100644 --- a/test/runtest.hs +++ /dev/null @@ -1,230 +0,0 @@ -{-# LANGUAGE CPP #-} -module Main where - -import Control.Monad -import Data.Char -import Data.List -import Data.Maybe -import qualified Data.Set as S -import Data.Time.Clock -import System.Directory -import System.Environment -import System.FilePath -import System.Exit -import System.Info -import System.IO -import System.Process - --- Because GHC earlier than 7.8 lacks setEnv --- Install the setenv package on Windows. -#if __GLASGOW_HASKELL__ < 708 -#ifndef mingw32_HOST_OS -import qualified System.Posix.Env as PE(setEnv) - -setEnv k v = PE.setEnv k v True -#else -import System.SetEnv(setEnv) -#endif -#endif - -data Flag = Update | Diff | ShowOutput | Quiet | Time deriving (Eq, Show, Ord) - -type Flags = S.Set Flag - -data Status = Success | Failure | Updated deriving (Eq, Show) - -data Config = Config { - flags :: Flags, - idrOpts :: [String], - tests :: [String] -} deriving (Show, Eq) - -isQuiet conf = Quiet `S.member` (flags conf) -showOutput conf = ShowOutput `S.member` (flags conf) -showTime conf = Time `S.member` (flags conf) -showDiff conf = Diff `S.member` (flags conf) -doUpdate conf = Update `S.member` (flags conf) - -checkTestName :: String -> Bool -checkTestName d = (all isDigit $ take 3 $ reverse d) - && (not $ isInfixOf "disabled" d) - -enumTests :: IO [String] -enumTests = do - cwd <- getCurrentDirectory - dirs <- getDirectoryContents cwd - return $ sort $ filter checkTestName dirs - -parseFlag :: String -> Maybe Flag -parseFlag s = case s of - "-u" -> Just Update - "-d" -> Just Diff - "-s" -> Just ShowOutput - "-t" -> Just Time - "-q" -> Just Quiet - _ -> Nothing - -parseFlags :: [String] -> (S.Set Flag, [String]) -parseFlags xs = (S.fromList f, i) - where - f = catMaybes $ map parseFlag fl - (fl, i) = partition (\s -> parseFlag s /= Nothing) xs - -parseArgs :: [String] -> IO Config -parseArgs args = do - (tests, rest) <- case args of - ("all":xs) -> do - et <- enumTests - return (et, xs) - ("without":xs) -> do - t <- enumTests - (blacklist, ys) <- return $ break (== "opts") xs - return (t \\ blacklist, ys \\ ["opts"]) - (x:xs) -> do - exists <- doesDirectoryExist x - return (if checkTestName x && exists then [x] else [], xs) - [] -> do - et <- enumTests - return (et, []) - let (testOpts, idOpts) = parseFlags rest - return $ Config testOpts idOpts tests - --- "bash" needed because Haskell has cmd as the default shell on windows, and --- we also want to run the process with another current directory, so we get --- this thing. -runInShell :: String -> [String] -> IO (ExitCode, String) -runInShell test opts = do - (ec, output, _) <- readCreateProcessWithExitCode - ((proc "bash" ("run":opts)) { cwd = Just test, - std_out = CreatePipe }) - "" - return (ec, output) - -runTest :: Config -> String -> IO Status -runTest conf test = do - -- don't touch the current directory as we want to run these things - -- in parallel in the future - let inTest s = test ++ "/" ++ s - t1 <- getCurrentTime - (exitCode, output) <- runInShell test (idrOpts conf) - t2 <- getCurrentTime - expected <- readFile $ inTest "expected" - writeFile (inTest "output") output - res <- if (norm output == norm expected) - then do putStrLn $ test ++ " finished...success" - return Success - else if doUpdate conf - then do putStrLn $ test ++ " finished...UPDATE" - writeFile (inTest "expected") output - return Updated - else do putStrLn $ test ++ " finished...FAILURE" - _ <- rawSystem "diff" [inTest "output", inTest "expected"] - return Failure - when (showTime conf) $ do - let dt = diffUTCTime t2 t1 - putStrLn $ "Duration of " ++ test ++ " was " ++ show dt - return res - where - -- just pretend that backslashes are slashes for comparison - -- purposes to avoid path problems, so don't write any tests - -- that depend on that distinction in other contexts. - -- Also rewrite newlines for consistency. - norm ('\r':'\n':xs) = '\n' : norm xs - norm ('\\':'\\':xs) = '/' : norm xs - norm ('\\':xs) = '/' : norm xs - norm (x : xs) = x : norm xs - norm [] = [] - -printStats :: Config -> [Status] -> IO () -printStats conf stats = do - let total = length stats - let successful = length $ filter (== Success) stats - let failures = length $ filter (== Failure) stats - let updates = length $ filter (== Updated) stats - putStrLn "\n----" - putStrLn $ show total ++ " tests run: " ++ show successful ++ " succesful, " - ++ show failures ++ " failed, " ++ show updates ++ " updated." - let failed = map fst $ filter ((== Failure) . snd) $ zip (tests conf) stats - when (failed /= []) $ do - putStrLn "\nFailed tests:" - mapM_ putStrLn failed - putStrLn "" - -runTests :: Config -> IO Bool -runTests conf = do - stats <- mapM (runTest conf) (tests conf) - unless (isQuiet conf) $ printStats conf stats - return $ all (== Success) stats - -runShow :: Config -> IO Bool -runShow conf = do - mapM_ (\t -> callProcess "cat" [t++"/output"]) (tests conf) - return True - -runDiff :: Config -> IO Bool -runDiff conf = do - mapM_ (\t -> do putStrLn $ "Differences in " ++ t ++ ":" - ec <- rawSystem "diff" [t++"/output", t++"/expected"] - when (ec == ExitSuccess) $ putStrLn "No differences found.") - (tests conf) - return True - -whisper :: Config -> String -> IO () -whisper conf s = do unless (isQuiet conf) $ putStrLn s - -isWindows :: Bool -isWindows = os `elem` ["win32", "mingw32", "cygwin32"] - -setPath :: Config -> IO () -setPath conf = do - maybeEnv <- lookupEnv "IDRIS" - idrisExists <- case maybeEnv of - Just idrisExe -> do - let exeExtension = if isWindows then ".exe" else "" - doesFileExist (idrisExe ++ exeExtension) - Nothing -> return False - if (idrisExists) - then do - idrisAbs <- makeAbsolute $ fromMaybe "" maybeEnv - setEnv "IDRIS" idrisAbs - whisper conf $ "Using " ++ idrisAbs - else do - path <- getEnv "PATH" - setEnv "IDRIS" "" - let sandbox = "../.cabal-sandbox/bin" - hasBox <- doesDirectoryExist sandbox - bindir <- if hasBox - then do - whisper conf $ "Using Cabal sandbox at " ++ sandbox - makeAbsolute sandbox - else do - stackExe <- findExecutable "stack" - case stackExe of - Just stack -> do - out <- readProcess stack ["path", "--dist-dir"] [] - stackDistDir <- return $ takeWhile (/= '\n') out - let stackDir = "../" ++ stackDistDir ++ "/build/idris" - whisper conf $ "Using stack work dir at " ++ stackDir - makeAbsolute stackDir - Nothing -> return "" - when (bindir /= "") $ setEnv "PATH" (bindir ++ [searchPathSeparator] ++ path) - -main = do - hSetBuffering stdout LineBuffering - withCabal <- doesDirectoryExist "test" - when withCabal $ do - setCurrentDirectory "test" - args <- getArgs - conf <- parseArgs args - setPath conf - t1 <- getCurrentTime - res <- case tests conf of - [] -> return True - xs | showOutput conf -> runShow conf - xs | showDiff conf -> runDiff conf - xs -> runTests conf - t2 <- getCurrentTime - when (showTime conf) $ do - let dt = diffUTCTime t2 t1 - putStrLn $ "Duration of Entire Test Suite was " ++ show dt - unless res exitFailure diff --git a/test/totality003/run b/test/totality003/run --- a/test/totality003/run +++ b/test/totality003/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ totality003.idr --check -${IDRIS:-idris} --nocolour $@ totality003a.idr --check +${IDRIS:-idris} $@ --nocolour totality003.idr --check +${IDRIS:-idris} $@ --nocolour totality003a.idr --check rm -f *.ibc diff --git a/test/totality009/run b/test/totality009/run --- a/test/totality009/run +++ b/test/totality009/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash OPTS="--consolewidth infinite --nocolour" -${IDRIS:-idris} "$@" $OPTS --check TestLambdaImpossible -${IDRIS:-idris} "$@" $OPTS --check --warnpartial TestLambdaPossible -${IDRIS:-idris} "$@" $OPTS --check TestLambdaPossible2 +${IDRIS:-idris} $@ $OPTS --check TestLambdaImpossible +${IDRIS:-idris} $@ $OPTS --check --warnpartial TestLambdaPossible +${IDRIS:-idris} $@ $OPTS --check TestLambdaPossible2 rm -f *.ibc diff --git a/test/tutorial001/run b/test/tutorial001/run --- a/test/tutorial001/run +++ b/test/tutorial001/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --check tutorial001.idr +${IDRIS:-idris} $@ --check tutorial001.idr rm -f *.ibc diff --git a/test/tutorial006/run b/test/tutorial006/run --- a/test/tutorial006/run +++ b/test/tutorial006/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ tutorial006a.idr --check -${IDRIS:-idris} --nocolour $@ tutorial006b.idr --check -${IDRIS:-idris} --nocolour $@ tutorial006c.idr -p effects --check +${IDRIS:-idris} $@ --nocolour tutorial006a.idr --check +${IDRIS:-idris} $@ --nocolour tutorial006b.idr --check +${IDRIS:-idris} $@ --nocolour tutorial006c.idr -p effects --check rm -f *.ibc diff --git a/test/tutorial007/run b/test/tutorial007/run --- a/test/tutorial007/run +++ b/test/tutorial007/run @@ -1,5 +1,5 @@ #!/usr/bin/env bash -gcc -shared -fPIC nativetypes.c -o nativetypes.so -idris $@ tutorial007.idr -o tutorial007 +${CC:-cc} -shared -fPIC nativetypes.c -o nativetypes.so +${IDRIS:-idris} $@ tutorial007.idr -o tutorial007 ./tutorial007 rm -f tutorial007 *.ibc *.so sizefromc.txt diff --git a/test/unique001/run b/test/unique001/run --- a/test/unique001/run +++ b/test/unique001/run @@ -1,9 +1,9 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ unique001.idr -o unique001 +${IDRIS:-idris} $@ --nocolour unique001.idr -o unique001 ./unique001 -${IDRIS:-idris} --nocolour $@ unique001a.idr --check -${IDRIS:-idris} --nocolour $@ unique001b.idr --check -${IDRIS:-idris} --nocolour $@ unique001c.idr --check -${IDRIS:-idris} --nocolour $@ unique001d.idr --check -${IDRIS:-idris} --nocolour $@ unique001e.idr --check +${IDRIS:-idris} $@ --nocolour unique001a.idr --check +${IDRIS:-idris} $@ --nocolour unique001b.idr --check +${IDRIS:-idris} $@ --nocolour unique001c.idr --check +${IDRIS:-idris} $@ --nocolour unique001d.idr --check +${IDRIS:-idris} $@ --nocolour unique001e.idr --check rm -f unique001 *.ibc diff --git a/test/unique002/run b/test/unique002/run --- a/test/unique002/run +++ b/test/unique002/run @@ -1,4 +1,4 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ unique002.idr --check -${IDRIS:-idris} --nocolour $@ unique002a.idr --check +${IDRIS:-idris} $@ --nocolour unique002.idr --check +${IDRIS:-idris} $@ --nocolour unique002a.idr --check rm -f *.ibc diff --git a/test/unique003/run b/test/unique003/run --- a/test/unique003/run +++ b/test/unique003/run @@ -1,3 +1,3 @@ #!/usr/bin/env bash -${IDRIS:-idris} --nocolour $@ unique003.idr --check +${IDRIS:-idris} $@ --nocolour unique003.idr --check rm -f *.ibc