0 | module Pack.CmdLn.Opts
  1 |
  2 | import Data.SortedMap
  3 | import Pack.CmdLn.Types
  4 | import Pack.Core
  5 | import Pack.Database
  6 | import Pack.Config.Types
  7 | import System.GetOpts
  8 | import System
  9 |
 10 | %default total
 11 |
 12 | -- Function for adjusting the config based on a command
 13 | -- line option. This first argument is the current directory
 14 | -- from which the application was invoked.
 15 | 0 AdjConf : Type
 16 | AdjConf = CurDir -> MetaConfig -> Either PackErr MetaConfig
 17 |
 18 | debug : AdjConf
 19 | debug _ = Right . {logLevel := Debug}
 20 |
 21 | quiet : AdjConf
 22 | quiet _ = Right . {logLevel := Silence}
 23 |
 24 | loglevel : String -> AdjConf
 25 | loglevel str _ c = map (\ll => {logLevel := ll} c) (readLogLevel str)
 26 |
 27 | withSrc : AdjConf
 28 | withSrc _ = Right . {withSrc := True}
 29 |
 30 | withDocs : AdjConf
 31 | withDocs _ = Right . {withDocs := True}
 32 |
 33 | useKatla : AdjConf
 34 | useKatla _ = Right . {useKatla := True}
 35 |
 36 | setDB : String -> AdjConf
 37 | setDB s _ c = map (\db => {collection := db} c) $ readDBName s
 38 |
 39 | setOutput : String -> AdjConf
 40 | setOutput s _ c = map (\o => {output := o} c) $ readBody s
 41 |
 42 | setQuery : QueryType -> AdjConf
 43 | setQuery s _ = Right . {queryType := s}
 44 |
 45 | setPrompt : Bool -> AdjConf
 46 | setPrompt b _ = Right . {safetyPrompt := b}
 47 |
 48 | setGCPrompt : Bool -> AdjConf
 49 | setGCPrompt b _ = Right . {gcPrompt := b}
 50 |
 51 | setGCPurge : Bool -> AdjConf
 52 | setGCPurge b _ = Right . {gcPurge := b}
 53 |
 54 | setWarnDepends : Bool -> AdjConf
 55 | setWarnDepends b _ = Right . {warnDepends := b}
 56 |
 57 | setSkipTests : Bool -> AdjConf
 58 | setSkipTests b _ = Right . {skipTests := b}
 59 |
 60 | setScheme : String -> AdjConf
 61 | setScheme s _ = Right . {scheme := fromString s}
 62 |
 63 | setBootstrap : Bool -> AdjConf
 64 | setBootstrap b _ = Right . {bootstrap := b}
 65 |
 66 | setBootstrapStage3 : Bool -> AdjConf
 67 | setBootstrapStage3 b _ = Right . {bootstrapStage3 := b}
 68 |
 69 | setRlwrap : Maybe String -> AdjConf
 70 | setRlwrap args _ = Right . {rlwrap := UseRlwrap $ maybe [] (\s => [NoEscape s]) args}
 71 |
 72 | addExtraArgs : String -> AdjConf
 73 | addExtraArgs args _ = Right . {extraArgs $= (++ [NoEscape args])}
 74 |
 75 | setIpkg : String -> AdjConf
 76 | setIpkg v (CD dir) c = case readAbsFile dir v of
 77 |   Right af => Right $ {withIpkg := Use af} c
 78 |   Left err => Left err
 79 |
 80 | setPkgs : String -> AdjConf
 81 | setPkgs str _ c =
 82 |   let ps = map MkPkgName . forget $ split (',' ==) str
 83 |    in Right $ {autoLoad := ForcePkgs ps} c
 84 |
 85 | noIpkg : AdjConf
 86 | noIpkg _ = Right . {withIpkg := None}
 87 |
 88 | codegen : String -> AdjConf
 89 | codegen v _ = Right . {codegen := fromString v}
 90 |
 91 | setGitInit : AdjConf
 92 | setGitInit _ = Right . {gitInit := True}
 93 |
 94 | -- command line options with description
 95 | descs : List $ OptDescr AdjConf
 96 | descs =
 97 |   [ MkOpt ['p'] ["package-set"]   (ReqArg setDB "<db>")
 98 |       "Set the curated package set to use."
 99 |   , MkOpt [] ["cg"]   (ReqArg codegen "<codgen>")
100 |       """
101 |       Sets the backend to use when building Idris executables
102 |       or running the REPL. The default is to use the `chez`
103 |       code generator.
104 |       """
105 |   , MkOpt [] ["scheme"]   (ReqArg setScheme "<exec>")
106 |       """
107 |       Sets the scheme executable for installing the Idris2 compiler.
108 |       As a default, this is set to `scheme`.
109 |       """
110 |   , MkOpt ['P'] ["packages"]  (ReqArg setPkgs "<packages>")
111 |       """
112 |       Load the given (comma-separated) list of packages into the REPL
113 |       session.
114 |       """
115 |   , MkOpt ['s'] ["short-desc"]   (NoArg $ setQuery ShortDesc)
116 |       """
117 |       Print the short description stored in an `.ipkg` file for
118 |       each query result.
119 |       """
120 |   , MkOpt ['l'] ["long-desc"]   (NoArg $ setQuery Details)
121 |       "Print a detailed description of a package known to pack"
122 |   , MkOpt [] ["tree"]   (NoArg $ setQuery Tree)
123 |       "Print a dependency tree of a package known to pack"
124 |   , MkOpt [] ["reverse-tree"]   (NoArg $ setQuery ReverseTree)
125 |       """
126 |       Print a tree of packages depending on a package know to pack.
127 |       Use this to find all packages transitively depending on a specific
128 |       library
129 |       """
130 |   , MkOpt ['d'] ["dependencies"]   (NoArg $ setQuery Dependencies)
131 |       "Print the dependencies of each query result."
132 |   , MkOpt ['o'] ["output"]   (ReqArg  setOutput "<file>")
133 |       """
134 |       Name of the output file when compiling or running single Idris source files
135 |       This defaults to `_tmppack` if not specified explicitly"
136 |       """
137 |   , MkOpt [] ["ipkg"]   (NoArg $ setQuery Ipkg)
138 |       "Print the full `.ipkg` file of each query result."
139 |   , MkOpt [] ["prompt"]   (NoArg $ setPrompt True)
140 |       """
141 |       Prompt before installing a potentially unsafe package
142 |       with custom build hooks.
143 |       """
144 |   , MkOpt [] ["no-prompt"]   (NoArg $ setPrompt False)
145 |       """
146 |       Don't prompt before installing a potentially unsafe package
147 |       with custom build hooks.
148 |       """
149 |   , MkOpt [] ["gc-prompt"]   (NoArg $ setGCPrompt True)
150 |       """
151 |       Prompt before deleting directories when running command `gc`.
152 |       """
153 |   , MkOpt [] ["gc-purge"]   (NoArg $ setGCPurge True)
154 |       """
155 |       Remove *all* outdated libraries during garbage collection.
156 |       """
157 |   , MkOpt [] ["no-gc-prompt"]   (NoArg $ setGCPrompt False)
158 |       """
159 |       Don't prompt before deleting directories when running command `gc`.
160 |       """
161 |   , MkOpt [] ["no-gc-purge"]   (NoArg $ setGCPurge False)
162 |       """
163 |       Only remove libraries built with an outdated compiler but not
164 |       outdated libraries built with the current compiler during garbage
165 |       collection.
166 |       """
167 |   , MkOpt [] ["bootstrap"]   (NoArg $ setBootstrap True)
168 |       """
169 |       Use the bootstrap compiler for building Idris2. This takes longer
170 |       than without bootstrapping, but it will even work if no Idris2
171 |       compiler or an outdated one is on the `$PATH`.
172 |       """
173 |   , MkOpt [] ["no-bootstrap"]   (NoArg $ setBootstrap False)
174 |       """
175 |       Use an existing version of Idris2 when building the compiler.
176 |       This will fail if `idris2` is not on the computer's `$PATH` or
177 |       is too old to build the current version of the compiler.
178 |       """
179 |   , MkOpt [] ["bootstrap-stage3"]   (NoArg $ setBootstrapStage3 True)
180 |       """
181 |       When bootstrapping, rebuilds the compiler once more using the newly
182 |       built compiler to produce a more optimised final version.
183 |       """
184 |   , MkOpt [] ["no-bootstrap-stage3"]   (NoArg $ setBootstrapStage3 False)
185 |       """
186 |       Don't perform an additional compiler rebuild during bootstrapping.
187 |       """
188 |   , MkOpt [] ["warn-depends"]   (NoArg $ setWarnDepends True)
189 |       """
190 |       Issue a warning in precense of a local `depends` directory, which might
191 |       interfere with the libraries managed by pack.
192 |       """
193 |   , MkOpt [] ["no-warn-depends"]   (NoArg $ setWarnDepends False)
194 |       """
195 |       Don't issue a warning in precense of a local `depends` directory.
196 |       """
197 |   , MkOpt [] ["skip-tests"]   (NoArg $ setSkipTests True)
198 |       """
199 |       Don't run library tests during collection checking.
200 |       This currently only affects the pack-admin utility.
201 |       """
202 |   , MkOpt [] ["with-src"]   (NoArg withSrc)
203 |       """
204 |       Include the source code of a library when installing
205 |       it. This allows some editor plugins to jump to the
206 |       definitions of functions and data types in other
207 |       modules.
208 |       """
209 |   , MkOpt [] ["with-docs"]   (NoArg withDocs)
210 |       """
211 |       Include the API documentation when installing libraries.
212 |       """
213 |   , MkOpt [] ["use-katla"]   (NoArg useKatla)
214 |       """
215 |       Use katla to add links to the semantically highlighted API sources.
216 |       """
217 |   , MkOpt [] ["with-ipkg"]   (ReqArg setIpkg "<.ipkg>")
218 |       """
219 |       Use settings and packages from the given `.ipkg` file when
220 |       starting a REPL session.
221 |       """
222 |   , MkOpt [] ["no-ipkg"]   (NoArg noIpkg)
223 |       """
224 |       Don't look for an `.ipkg` file in scope when starting a REPL session.
225 |       """
226 |   , MkOpt [] ["rlwrap"]   (OptArg setRlwrap "<rlwrap args>")
227 |       "Run a REPL session in `rlwrap`."
228 |   , MkOpt [] ["extra-args"] (ReqArg addExtraArgs "<idris2 args>")
229 |       "Any extra arguments to pass to Idris2."
230 |   , MkOpt ['v'] ["verbose"]   (NoArg debug)
231 |       "Print debugging information"
232 |   , MkOpt ['q'] ["quiet"]   (NoArg quiet)
233 |       "Quiet mode"
234 |   , MkOpt [] ["log-level"]   (ReqArg loglevel "<log level>")
235 |       """
236 |       Specify the logging level to use. Accepted values are:
237 |       \{joinBy ", " $ show . fst <$> logLevels}.
238 |       """
239 |   , MkOpt [] ["git-init"] (NoArg setGitInit)
240 |       """
241 |       Initialize git for a pack project.
242 |       """
243 |   ]
244 |
245 | ||| Names of all command line options (prefixed with "-" in case of
246 | ||| single-character option names and with "--" in case of multi-character
247 | ||| option names.
248 | export
249 | optionNames : List String
250 | optionNames = foldMap names descs
251 |
252 |   where
253 |     names : OptDescr a -> List String
254 |     names (MkOpt sns lns _ _) =
255 |       map (\c => "-\{String.singleton c}") sns ++ map ("--" ++) lns
256 |
257 | ||| A Package of the current directory, current command, its arguments, and the
258 | ||| options.
259 | public export
260 | record ParsedArgs (0 c : Type) {auto 0 prf : Command c} where
261 |   constructor MkParsedArgs
262 |   curDir : CurDir
263 |   cmd    : CommandWithArgs c
264 |   opts   : List AdjConf
265 |
266 | ||| Get the arguments (not including the defacto first argument that is the
267 | ||| name of the binary).
268 | export
269 | getArgs' : HasIO io => io (List String)
270 | getArgs' = drop 1 <$> getArgs
271 |
272 | ||| Given the current directory (from which pack was
273 | ||| invoked) parse the arguments into a command, positional arguments, and
274 | ||| options.
275 | export
276 | parseOpts :
277 |      (0 c : Type)
278 |   -> {auto _ : Command c}
279 |   -> (curDir : CurDir)
280 |   -> (args : List String)
281 |   -> Either PackErr (ParsedArgs c)
282 | parseOpts c dir args =
283 |   case getOpt RequireOrder descs args of
284 |     MkResult opts n  []      []       => do
285 |       cmd <- readCommand c dir n
286 |       pure $ MkParsedArgs dir cmd opts
287 |     MkResult _    _ (u :: _) _        => Left (UnknownArg u)
288 |     MkResult _    _ _        (e :: _) => Left (ErroneousArg e)
289 |
290 | ||| Given the current directory (from which pack was invoked)
291 | ||| and an initial config assembled from the `pack.toml` files
292 | ||| in scope, generates the application
293 | ||| config and command to run from a list of command
294 | ||| line arguments.
295 | |||
296 | ||| @ c      : Type representing the command to run
297 | |||            We abstract over this type, because pack and
298 | |||            pack-admin accept different kinds of commands,
299 | |||            and both applications use this function to parse
300 | |||            the command line args
301 | |||
302 | ||| @ curDir : Current working directory
303 | ||| @ init   : Initial config (possibly assebled from `pack.toml` files)
304 | ||| @ args   : List of command line arguments
305 | export
306 | applyArgs :
307 |      (0 c : Type)
308 |   -> {auto _ : Command c}
309 |   -> (init   : MetaConfig)
310 |   -> (args   : ParsedArgs c)
311 |   -> Either PackErr MetaConfig
312 | applyArgs c init args = do
313 |   let lvl_m := lookup (cmdName $ fst args.cmd) init.levels
314 |       dflt  := defaultLevel $ fst args.cmd
315 |
316 |       init' = {logLevel := fromMaybe dflt lvl_m} init
317 |   foldlM (\c,f => f args.curDir c) init' args.opts
318 |
319 | --------------------------------------------------------------------------------
320 | --          Usage Info
321 | --------------------------------------------------------------------------------
322 |
323 | ||| Application info printed with the `help` action.
324 | export
325 | usageInfo : String
326 | usageInfo = """
327 |   Options:
328 |   \{usageInfo "" descs}
329 |
330 |   Run `pack help <cmd>` to get detailed information about a command.
331 |
332 |   Available commands:
333 |   \{unlines $ map (indent 2 . fst) Types.namesAndCommands}
334 |   """
335 |