bb4a84b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3074 from jfdm/remove-old-things

bb4a84bJan de Muijnck-Hughes11 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -9,6 +9,8 @@ New in 0.12:

9 logging level and categories, default totality check, warn reach,

10 IBC output folder, and idris path.

12+* Remove deprecated options `--ideslave` and `--ideslave-socket`. These options

13+ were replaced with `--ide-mode` and `--ide-mode-socket` in 0.9.17

13New in 0.11:

15New in 0.11:

14============

16============

man/idris.1+32−2

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

1.\" Manpage for Idris.

2.\" Contact <> to correct errors or typos.

3−.TH man 1 "06 August 2014" "0.9.14.1" "Idris man page"

3+.TH man 1 "25 March 2016" "0.11" "Idris man page"

4.SH NAME

5idris -\ a general purpose pure functional programming language with dependent types.

6.SH SYNOPSIS

@@ -45,19 +45,37 @@ should not necessarily be seen as production ready nor for industrial use.

45.SH OPTIONS

46 --nobanner Suppress the banner

47 -q,--quiet Quiet verbosity

48+ --ide-mode Run the Idris REPL with machine-readable syntax

49+ --ide-mode-socket Choose a socket for IDE mode to listen on

50+ --ideslave Deprecated version of --ide-mode

51+ --ideslave-socket Deprecated version of --ide-mode-socket

48 --log LEVEL Debugging log level

52 --log LEVEL Debugging log level

53+ --logging-categories CATS

54+ Colon separated logging categories. Use --listlogcats

55+ to see list.

56+ --nobasepkgs Do not use the given base package

57+ --noprelude Do not use the given prelude

58+ --nobuiltins Do not use the builtin functions

59+ --check Typecheck only, don't start the REPL

49 -o,--output FILE Specify output file

60 -o,--output FILE Specify output file

61+ --interface Generate interface files from ExportLists

62+ --typeintype Turn off Universe checking

50 --total Require functions to be total by default

63 --total Require functions to be total by default

51 --warnpartial Warn about undeclared partial functions

64 --warnpartial Warn about undeclared partial functions

52 --warnreach Warn about reachable but inaccessible arguments

65 --warnreach Warn about reachable but inaccessible arguments

66+ --listlogcats Display logging categories

53 --link Display link flags

67 --link Display link flags

68+ --listlibs Display installed libraries

54 --libdir Display library directory

69 --libdir Display library directory

55 --include Display the includes flags

70 --include Display the includes flags

56 -V,--verbose Loud verbosity

71 -V,--verbose Loud verbosity

57 --ibcsubdir FILE Write IBC files into sub directory

72 --ibcsubdir FILE Write IBC files into sub directory

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

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

74+ -p,--package ARG Add package as a dependency

75+ --port PORT REPL TCP port

59 --build IPKG Build package

76 --build IPKG Build package

60 --install IPKG Install package

77 --install IPKG Install package

78+ --repl IPKG Launch REPL, only for executables

61 --clean IPKG Clean package

79 --clean IPKG Clean package

62 --mkdoc IPKG Generate IdrisDoc for package

80 --mkdoc IPKG Generate IdrisDoc for package

63 --checkpkg IPKG Check package only

81 --checkpkg IPKG Check package only

@@ -65,19 +83,31 @@ should not necessarily be seen as production ready nor for industrial use.

65 -S,--codegenonly Do no further compilation of code generator output

83 -S,--codegenonly Do no further compilation of code generator output

66 -c,--compileonly Compile to object files rather than an executable

84 -c,--compileonly Compile to object files rather than an executable

67 --mvn Create a maven project (for Java codegen)

85 --mvn Create a maven project (for Java codegen)

68− --codegen TARGET Select code generator: C, Java, bytecode

86+ --codegen TARGET Select code generator: C, Javascript, Node and

87+ bytecode are bundled with Idris

88+ --cg-opt ARG Arguments to pass to code generator

69 -e,--eval EXPR Evaluate an expression without loading the REPL

89 -e,--eval EXPR Evaluate an expression without loading the REPL

70 --execute Execute as idris

90 --execute Execute as idris

71 --exec EXPR Execute as idris

91 --exec EXPR Execute as idris

72 -X,--extension EXT Turn on language extension (TypeProviders or

92 -X,--extension EXT Turn on language extension (TypeProviders or

73 ErrorReflection)

93 ErrorReflection)

94+ --no-partial-eval Switch off partial evaluation, mainly for debugging

95+ purposes

74 --target TRIPLE Select target triple (for llvm codegen)

96 --target TRIPLE Select target triple (for llvm codegen)

75 --cpu CPU Select target CPU e.g. corei7 or cortex-m3 (for LLVM

97 --cpu CPU Select target CPU e.g. corei7 or cortex-m3 (for LLVM

76 codegen)

98 codegen)

77 --color,--colour Force coloured output

99 --color,--colour Force coloured output

78 --nocolor,--nocolour Disable coloured output

100 --nocolor,--nocolour Disable coloured output

101+ --consolewidth WIDTH Select console width: auto, infinite, nat

102+ --highlight Emit source code highlighting

103+ --no-elim-deprecation-warnings

104+ Disable deprecation warnings for %elim

105+ --no-tactic-deprecation-warnings

106+ Disable deprecation warnings for the old tactic

107+ sublanguage

79 -v,--version Print version information

108 -v,--version Print version information

80 -h,--help Show this help text

109 -h,--help Show this help text

110+

81.SH SEE ALSO

111.SH SEE ALSO

112

83+ The IDRIS web site (http://idris-lang.org/

113+ The IDRIS web site (http://idris-lang.org/

src/Idris/CmdOptions.hs+71−40

@@ -28,7 +28,7 @@ runArgParser = do opts <- execParser $ info parser

28 )

29 return $ preProcOpts opts []

30 where

31− idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]

31+ idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2016"]

32 idrisProgDesc = PP.vsep [PP.empty,

33 PP.text "Idris is a general purpose pure functional programming language with dependent",

34 PP.text "types. Dependent types allow types to be predicated on values, meaning that",

@@ -76,14 +76,15 @@ parser = runA $ proc () -> do

77parseFlags :: Parser [Opt]

78parseFlags = many $

79− flag' NoBanner (long "nobanner" <> help "Suppress the banner")

79+ flag' NoBanner (long "nobanner" <> help "Suppress the banner")

80− <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

80+ <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

81+

81 -- IDE Mode Specific Flags

82 -- IDE Mode Specific Flags

82− <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")

83+ <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")

83 <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")

84 <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")

84− <|> flag' Idemode (long "ideslave" <> help "Deprecated version of --ide-mode") -- TODO: Remove in v0.9.18

85+

85− <|> flag' IdemodeSocket (long "ideslave-socket" <> help "Deprecated version of --ide-mode-socket") -- TODO: Remove in v0.9.18

86 <|> (Client <$> strOption (long "client"))

87+

87 -- Logging Flags

88 -- Logging Flags

88 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

89 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

89 <|> (OLogCats <$> option (str >>= parseLogCats)

90 <|> (OLogCats <$> option (str >>= parseLogCats)

@@ -91,71 +92,101 @@ parseFlags = many $

91 <> metavar "CATS"

92 <> metavar "CATS"

92 <> help "Colon separated logging categories. Use --listlogcats to see list."))

93 <> help "Colon separated logging categories. Use --listlogcats to see list."))

94− -- Turn off Certain libraries.

95+ -- Turn off things

95 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

96 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

96− <|> flag' NoPrelude (long "noprelude" <> help "Do not use the given prelude")

97+ <|> flag' NoPrelude (long "noprelude" <> help "Do not use the given prelude")

97 <|> flag' NoBuiltins (long "nobuiltins" <> help "Do not use the builtin functions")

98 <|> flag' NoBuiltins (long "nobuiltins" <> help "Do not use the builtin functions")

99+

98− <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

100+ <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

101+

99 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

102 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

103+

100 -- <|> flag' TypeCase (long "typecase")

104 -- <|> flag' TypeCase (long "typecase")

101− <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

105+ <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

102− <|> flag' TypeInType (long "typeintype" <> help "Turn off Universe checking")

106+ <|> flag' TypeInType (long "typeintype" <> help "Turn off Universe checking")

103− <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

107+ <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

104 <|> flag' DefaultPartial (long "partial")

108 <|> flag' DefaultPartial (long "partial")

105− <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")

109+ <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")

106− <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

110+ <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

107− <|> flag' NoCoverage (long "nocoverage")

111+ <|> flag' NoCoverage (long "nocoverage")

108− <|> flag' ErrContext (long "errorcontext")

112+ <|> flag' ErrContext (long "errorcontext")

113+

109 -- Show things

114 -- Show things

110− <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")

115+ <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")

111− <|> flag' ShowLibs (long "link" <> help "Display link flags")

116+ <|> flag' ShowLibs (long "link" <> help "Display link flags")

112− <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

117+ <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

113− <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

118+ <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

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

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

120+

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

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

122+

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

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

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

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

125+

118 <|> flag' WarnOnly (long "warn")

126 <|> flag' WarnOnly (long "warn")

127+

119− <|> (Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))

128+ <|> (Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))

120 <|> (Port <$> strOption (long "port" <> metavar "PORT" <> help "REPL TCP port"))

129 <|> (Port <$> strOption (long "port" <> metavar "PORT" <> help "REPL TCP port"))

130+

121 -- Package commands

131 -- Package commands

122− <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

132+ <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

123− <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

133+ <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

124− <|> (PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables"))

134+ <|> (PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables"))

125− <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

135+ <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

126− <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

136+ <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

127− <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

137+ <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

128− <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

138+ <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

139+

129 -- Misc options

140 -- Misc options

130 <|> (BCAsm <$> strOption (long "bytecode"))

141 <|> (BCAsm <$> strOption (long "bytecode"))

142+

131− <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

143+ <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

132− <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

144+ <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

133− <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")

145+ <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")

146+

134 <|> (DumpDefun <$> strOption (long "dumpdefuns"))

147 <|> (DumpDefun <$> strOption (long "dumpdefuns"))

135 <|> (DumpCases <$> strOption (long "dumpcases"))

148 <|> (DumpCases <$> strOption (long "dumpcases"))

149+

150+ <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"

151+ <> metavar "TARGET"

136− <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))

152+ <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))

153+ <|> (CodegenArgs <$> strOption (long "cg-opt"

154+ <> metavar "ARG"

137− <|> (CodegenArgs <$> strOption (long "cg-opt" <> metavar "ARG" <> help "Arguments to pass to code generator"))

155+ <> help "Arguments to pass to code generator"))

156+

138 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

157 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

158+

139 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

159 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

140− <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

160+ <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

161+

162+ <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension"

163+ <> short 'X'

164+ <> metavar "EXT"

141− <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension" <> short 'X' <> metavar "EXT" <> help "Turn on language extension (TypeProviders or ErrorReflection)"))

165+ <> help "Turn on language extension (TypeProviders or ErrorReflection)"))

166+

142 -- Optimisation Levels

167 -- Optimisation Levels

143 <|> flag' (OptLevel 3) (long "O3")

168 <|> flag' (OptLevel 3) (long "O3")

144 <|> flag' (OptLevel 2) (long "O2")

169 <|> flag' (OptLevel 2) (long "O2")

145 <|> flag' (OptLevel 1) (long "O1")

170 <|> flag' (OptLevel 1) (long "O1")

146 <|> flag' (OptLevel 0) (long "O0")

171 <|> flag' (OptLevel 0) (long "O0")

172+

147 <|> flag' (AddOpt PETransform) (long "partial-eval")

173 <|> flag' (AddOpt PETransform) (long "partial-eval")

148 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

174 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

175+

149 <|> (OptLevel <$> option auto (short 'O' <> long "level"))

176 <|> (OptLevel <$> option auto (short 'O' <> long "level"))

177+

150 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

178 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

151− <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

179+ <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

180+

152 -- Colour Options

181 -- Colour Options

153− <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

182+ <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

154 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

183 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

155

184

156 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

185 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

186+

157 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

187 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

188+

158− <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

189+ <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

159 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

190 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

160

191

161 where

192 where