e4cf620 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

e4cf620Edwin Brady12 years ago

README.md+28−12

compare with master

unifiedsplit

@@ -7,14 +7,18 @@ Idris (http://idris-lang.org/) is a general-purpose functional programming

7language with dependent types.

9## Standard Installation Instructions

10−This repository represents the latest development version of the language, and may contain bugs that are being actively worked on.

10+This repository represents the latest development version of the language,

11+and may contain bugs that are being actively worked on.

11−For those who wish to use a more stable version of Idris please consider installing the latest version that has been released on Hackage.

12+For those who wish to use a more stable version of Idris please consider

13+installing the latest version that has been released on Hackage.

12Installation instructions for various platforms can be [found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).

14Installation instructions for various platforms can be [found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).

14## Installing Development Versions

16## Installing Development Versions

16−If you like to work against the latest development version, please consider using Cabal Sandboxes to minimise disruption to your local Haskell setup.

18+If you like to work against the latest development version, please consider

19+using Cabal Sandboxes to minimise disruption to your local Haskell setup.

20+Instructions for installing Idris HEAD within a cabal sandbox are

17−Instructions for install Idris HEAD within a cabal sandbox are [available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).

21+[available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).

19To configure, edit config.mk. The default values should work for most people.

23To configure, edit config.mk. The default values should work for most people.

@@ -31,17 +35,21 @@ for the same architecture as your Haskell compiler (e.g. 64 bit libraries

31for 64 bit ghc). By default, Idris builds without it. To build with it, pass

35for 64 bit ghc). By default, Idris builds without it. To build with it, pass

32the flag `-f FFI`.

36the flag `-f FFI`.

34−To build with `libffi` by default, create a `custom.mk` file and add the following line to it:

38+To build with `libffi` by default, create a `custom.mk` file and add the

39+following line to it:

36`CABALFLAGS += -f FFI`

41`CABALFLAGS += -f FFI`

38The file custom.mk-alldeps is a suitable example.

43The file custom.mk-alldeps is a suitable example.

45+The continuous integration builds on travis-ci.org are built using the

40−The continues integration builds on travis-ci.org are build using the ghc-flag -Werror. To enable this behaviour locally also, please compile using `make CI=true` or adding the following line into `custom.mk`:

46+ghc-flag -Werror. To enable this behaviour locally also, please compile

47+using `make CI=true` or adding the following line into `custom.mk`:

42`CI = true`

49`CI = true`

44−If you are only compiling for installing the most current version, you can ommit the CI flag, but please make sure you use it if you want to contribute.

51+If you are only compiling for installing the most current version, you can

52+omit the CI flag, but please make sure you use it if you want to contribute.

46## Code Generation

54## Code Generation

@@ -49,13 +57,21 @@ Idris has support for external code generators. Supplied with the distribution

49is a C code generator to compile executables, and a JavaScript code generator

57is a C code generator to compile executables, and a JavaScript code generator

50with support for node.js and browser JavaScript.

58with support for node.js and browser JavaScript.

52−At this moment in time there are two external repositories with

60+At this moment in time there are two external repositories with a

53−a [Java code generator](https://github.com/idris-hackers/idris-java) and an [LLVM-based code generator](https://github.com/idris-hackers/idris-llvm).

61+[Java code generator](https://github.com/idris-hackers/idris-java) and an

62+[LLVM-based code generator](https://github.com/idris-hackers/idris-llvm).

55## More Information

64## More Information

57−If you would like to find out more information, or ask questions, we currently have a [Wiki](https://github.com/idris-lang/Idris-dev/wiki); a [mailing list](https://groups.google.com/forum/#!forum/idris-lang), and an `IRC` channel `#idris` on freenode. To join the IRC channel, point your irc client to `chat.freenode.net` then `/join #idris`.

66+If you would like to find out more information, or ask questions, we

67+currently have a [Wiki](https://github.com/idris-lang/Idris-dev/wiki);

68+a [mailing list](https://groups.google.com/forum/#!forum/idris-lang),

69+and an `IRC` channel `#idris` on freenode. To join the IRC channel,

70+point your irc client to `chat.freenode.net` then `/join #idris`.

72+For those further interested in using Idris for projects, the

59−For those further interested in using Idris for projects, the [Idris Hackers](https://github.com/idris-hackers) GitHub organisation is where some interesting projects are being hosted.

73+[Idris Hackers](https://github.com/idris-hackers) GitHub organisation is

74+where some interesting projects are being hosted.

61−For those interested in contributing to Idris directly we kindly ask that prospective developers please consult [CONTRIBUTING.md] first.

76+For those interested in contributing to Idris directly we kindly ask that

77+prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first.

idris.cabal+3

@@ -455,6 +455,9 @@ Extra-source-files:

455 test/interactive006/input

456 test/interactive006/*.idr

457 test/interactive006/expected

458+ test/interactive007/run

459+ test/interactive007/input

460+ test/interactive007/expected

458

461

459 test/io001/run

462 test/io001/run

460 test/io001/*.idr

463 test/io001/*.idr

src/IRTS/CodegenC.hs+1−1

@@ -69,7 +69,7 @@ codegenC' defs out exec incs objs libs flags dbg

69 let args = [gccDbg dbg] ++

70 gccFlags ++

71 -- # Any flags defined here which alter the RTS API must also be added to config.mk

72− ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS",

72+ ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

73 "-I."] ++ objs ++ ["-x", "c"] ++

74 (if (exec == Executable) then [] else ["-c"]) ++

75 [tmpn] ++

src/Idris/Error.hs−1

@@ -5,7 +5,6 @@ module Idris.Error where

5import Prelude hiding (catch)

6import Idris.AbsSyntax

7import Idris.Delaborate

8−import Idris.Output

10import Idris.Core.Evaluate (ctxtAlist)

9import Idris.Core.Evaluate (ctxtAlist)

11import Idris.Core.TT

10import Idris.Core.TT

src/Idris/Parser.hs+8−9

@@ -220,10 +220,10 @@ decl' syn = fixity

220-}

221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

222syntaxDecl syn = do s <- syntaxRule syn

223− i <- get

223+ i <- get

224 put (i `addSyntax` s)

225 fc <- getFC

226− return (PSyntax fc s)

226+ return (PSyntax fc s)

227

228-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.

229addSyntax :: IState -> Syntax -> IState

@@ -1210,14 +1210,14 @@ parseProg syn fname input mrk

1210{- | Load idris module and show error if something wrong happens -}

1211loadModule :: FilePath -> Idris (Maybe String)

1212loadModule f

1213− = idrisCatch (fmap Just (loadModule' f))

1213+ = idrisCatch (loadModule' f)

1214 (\e -> do setErrSpan (getErrSpan e)

1215 ist <- getIState

1216 iWarn (getErrSpan e) $ pprintErr ist e

1217 return Nothing)

1218

1219{- | Load idris module -}

1220−loadModule' :: FilePath -> Idris String

1220+loadModule' :: FilePath -> Idris (Maybe String)

1221loadModule' f

1222 = do i <- getIState

1223 let file = takeWhile (/= ' ') f

@@ -1225,7 +1225,8 @@ loadModule' f

1225 ids <- allImportDirs

1226 fp <- findImport ids ibcsd file

1227 if file `elem` imported i

1228− then iLOG $ "Already read " ++ file

1228+ then do iLOG $ "Already read " ++ file

1229+ return Nothing

1229 else do putIState (i { imported = file : imported i })

1230 else do putIState (i { imported = file : imported i })

1230 case fp of

1231 case fp of

1231 IDR fn -> loadSource False fn Nothing

1232 IDR fn -> loadSource False fn Nothing

@@ -1236,9 +1237,7 @@ loadModule' f

1236 case src of

1237 case src of

1237 IDR sfn -> loadSource False sfn Nothing

1238 IDR sfn -> loadSource False sfn Nothing

1238 LIDR sfn -> loadSource True sfn Nothing)

1239 LIDR sfn -> loadSource True sfn Nothing)

1239− let (dir, fh) = splitFileName file

1240+ return $ Just file

1240− return (dropExtension fh)

1241−

1242

1241

1243{- | Load idris code from file -}

1242{- | Load idris code from file -}

1244loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

1243loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

@@ -1277,7 +1276,7 @@ loadSource lidr f toline

1277 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in

1276 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in

1278 ids <- allImportDirs

1277 ids <- allImportDirs

1279 ibcsd <- valIBCSubDir i

1278 ibcsd <- valIBCSubDir i

1280− mapM_ (\(re, f) ->

1279+ mapM_ (\(re, f) ->

1281 do fp <- findImport ids ibcsd f

1280 do fp <- findImport ids ibcsd f

1282 case fp of

1281 case fp of

1283 LIDR fn -> ifail $ "No ibc for " ++ f

1282 LIDR fn -> ifail $ "No ibc for " ++ f

src/Idris/REPL.hs+2−1

@@ -629,6 +629,7 @@ processInput cmd orig inputs efile

629 Success (Right Reload) ->

630 do putIState $ orig { idris_options = idris_options i

631 , idris_colourTheme = idris_colourTheme i

632+ , imported = imported i

632 }

633 }

633 clearErr

634 clearErr

634 mods <- loadInputs inputs Nothing

635 mods <- loadInputs inputs Nothing

@@ -1181,7 +1182,7 @@ process fn (SetConsoleWidth w) = setWidth w

1181

1182

1182process fn (Apropos pkgs a) =

1183process fn (Apropos pkgs a) =

1183 do orig <- getIState

1184 do orig <- getIState

1184− when (not (null pkgs)) $

1185+ when (not (null pkgs)) $

1185 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

1186 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

1186 mapM_ loadPkgIndex pkgs

1187 mapM_ loadPkgIndex pkgs

1187 ist <- getIState

1188 ist <- getIState

test/interactive007/expectednew file+1

@@ -0,0 +1 @@

1+Idris> *Data/ZZ> *Data/ZZ> *Data/ZZ> *Data/ZZ> Bye bye

test/interactive007/inputnew file+4

@@ -0,0 +1,4 @@

1+:module Data.ZZ

2+:module Data.ZZ

3+:r

4+:module Data.ZZ

test/interactive007/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris --nobanner --nocolor < input