0 | module Pack.CmdLn.Types
2 | import Data.List.Elem
4 | import Pack.Config.Types
5 | import Pack.Database.Types
12 | data QueryMode = PkgName | Dependency | Module
16 | record PkgQuery where
23 | argDesc_ = "[mode] <query>"
25 | readArg ("dep" :: s :: t) = Just (MkQ Dependency s, t)
26 | readArg ("module" :: s :: t) = Just (MkQ Module s, t)
27 | readArg [s] = Just (MkQ PkgName s, [])
31 | record FuzzyQuery where
37 | Arg FuzzyQuery where
38 | argDesc_ = "[<pkgs>] <query>"
40 | readArg (ps :: s :: t) =
41 | let pkgs = map MkPkgName $
forget $
split (',' ==) ps
42 | in Just (MkFQ pkgs s, t)
43 | readArg [s] = Just (MkFQ [] s, [])
44 | readArg [] = Nothing
49 | data TrivialCmd : Type where
51 | CompletionScript : TrivialCmd
56 | data ConfiguredCmd : Type where
58 | Build : ConfiguredCmd
59 | BuildDeps : ConfiguredCmd
60 | Typecheck : ConfiguredCmd
61 | Clean : ConfiguredCmd
62 | CleanBuild : ConfiguredCmd
63 | Repl : ConfiguredCmd
64 | Exec : ConfiguredCmd
67 | Install : ConfiguredCmd
68 | InstallApp : ConfiguredCmd
69 | Remove : ConfiguredCmd
70 | RemoveApp : ConfiguredCmd
72 | Test : ConfiguredCmd
74 | Update : ConfiguredCmd
75 | Fetch : ConfiguredCmd
78 | PackagePath : ConfiguredCmd
79 | LibsPath : ConfiguredCmd
80 | DataPath : ConfiguredCmd
81 | AppPath : ConfiguredCmd
84 | Switch : ConfiguredCmd
85 | UpdateDB : ConfiguredCmd
86 | CollectGarbage : ConfiguredCmd
89 | Info : ConfiguredCmd
90 | Query : ConfiguredCmd
91 | Fuzzy : ConfiguredCmd
94 | Completion : ConfiguredCmd
98 | Uninstall : ConfiguredCmd
101 | PrintHelp : ConfiguredCmd
107 | data Cmd = Trivial TrivialCmd
108 | | Configured ConfiguredCmd
112 | name : Cmd -> String
114 | namespace Configured
119 | commands : List ConfiguredCmd
154 | name : ConfiguredCmd -> String
155 | name (Build ) = "build"
156 | name (BuildDeps ) = "install-deps"
157 | name (Typecheck ) = "typecheck"
158 | name (Clean ) = "clean"
159 | name (CleanBuild ) = "cleanbuild"
160 | name (Repl ) = "repl"
161 | name (Exec ) = "exec"
162 | name (Install ) = "install"
163 | name (InstallApp ) = "install-app"
164 | name (Remove ) = "remove"
165 | name (RemoveApp ) = "remove-app"
166 | name (Run ) = "run"
167 | name (Test ) = "test"
168 | name (New ) = "new"
169 | name (Update ) = "update"
170 | name (Fetch ) = "fetch"
171 | name (PackagePath ) = "package-path"
172 | name (LibsPath ) = "libs-path"
173 | name (DataPath ) = "data-path"
174 | name (AppPath ) = "app-path"
175 | name (Switch ) = "switch"
176 | name (UpdateDB ) = "update-db"
177 | name (CollectGarbage ) = "gc"
178 | name (Info ) = "info"
179 | name (Query ) = "query"
180 | name (Fuzzy ) = "fuzzy"
181 | name (Completion ) = "completion"
182 | name (Uninstall ) = "uninstall"
183 | name (PrintHelp ) = "help"
187 | namesAndCommands : List (String, ConfiguredCmd)
188 | namesAndCommands = map (\c => (name c, c)) commands
192 | cmdDesc : ConfiguredCmd -> String
193 | cmdDesc (Build) = """
194 | Build a local package given as an `.ipkg` file or package name.
195 | When no package is given, try to find the only one in the current directory.
196 | This will also install the package's dependencies.
199 | cmdDesc (BuildDeps) = """
200 | Install the dependencies of a local package given as an `.ipkg` file
201 | or package name. When no package is given, try to find the only one
202 | in the current directory.
205 | cmdDesc (Typecheck) = """
206 | Typecheck a local package given as an `.ipkg` file or package name.
207 | When no package is given, try to find the only one in the current directory.
210 | cmdDesc (Clean) = """
211 | Clean up a local package by removing its build directory.
212 | When no package is given, try to find the only one in the current directory.
215 | cmdDesc (CleanBuild) = """
216 | Convenience combination of `clean` followed by `build`.
219 | cmdDesc (Repl) = """
220 | Start a REPL session loading an optional `.idr` file.
221 | Use command line option `--with-ipkg` to load settings
222 | and packages from an `.ipkg` file. Option `--no-ipkg` can be used
223 | to not go looking for an `.ipkg` file. The default behavior
224 | is for pack to use the first `.ipkg` file it can find in the
225 | current directory or one of its parent directories.
227 | In order to start the REPL session with the `rlwrap` utility, use
228 | the `--rlwrap` command-line option or set flag `repl.rlwrap` in one
229 | of your `pack.toml` files either to `true` or to a string containing
230 | additional arguments to be used when running `rlwrap`.
233 | cmdDesc (Exec) = """
234 | Compile the given Idris source file and execute its main function
235 | with the given list of arguments. This will look for `.ipkg` files
236 | in the source file's parent directories and will apply the settings
239 | To change the name of the generated executable, use the `-o` command-line
242 | To change the codegen to use, use the `--cg` command-line option.
245 | cmdDesc (Install) = "Install the given packages."
247 | cmdDesc (InstallApp) = "Install the given applications."
249 | cmdDesc (Remove) = "Uninstall the given libraries."
251 | cmdDesc (RemoveApp) = "Uninstall the given applications."
253 | cmdDesc (Run) = """
254 | Run an application from the package collection or a local `.ipkg`
255 | file passing it the given command line arguments.
256 | When no package and no arguments are given, try to find the only one
257 | in the current directory.
259 | Note: This will install remote apps before running them without
260 | generating an entry in `$PACK_DIR/bin`.
261 | Local apps and applications specified as mere `.ipkg` files
262 | will be built and run locally without installing them.
264 | To change the codegen to use, use the `--cg` command-line option.
267 | cmdDesc (Test) = """
268 | Run a test suite as specified in a package description's `test` field.
270 | The `test` field should consist of a file path relative to a package's
271 | root directory point to the test suite's `.ipkg` file:
277 | test = "test/test.ipkg"
280 | cmdDesc (New) = """
281 | Create a new package in the current directory
282 | consisting of a source directory, a default module, a skeleton test suite, a local pack.toml file and a .ipkg file.
284 | Passing the `--git-init` command line option will
285 | create a .gitignore file and a .git directory.
287 | Note: Since module names with a hyphen ('-') are not supported by
288 | Idris, any hyphen in the package name will be replaced with an
289 | underscore ('_') in the generated module name.
292 | cmdDesc (Update) = """
293 | Update the pack installation by downloading and building
294 | the current main branch of
295 | https://github.com/stefan-hoeck/idris2-pack.
297 | In order to specify a different commit or repository to use, adjust
298 | settings `pack.url` and `pack.commit` in one of your `pack.toml`
301 | Note: This uses the current package collection, which might be
302 | too outdated to build the latest pack. If this fails, try using
303 | the latest nightly.
306 | cmdDesc (Fetch) = """
307 | Fetch the latest commit hashes from a repository for Git packages with a
308 | commit entry of "latest:branch".
311 | cmdDesc (PackagePath) = """
312 | Return a colon-separated list of paths where Idris packages are
313 | installed. This is useful for programs like `idris2-lsp`,
314 | which need to know where to look for installed packages.
317 | cmdDesc (LibsPath) = """
318 | Return a colon-separated list of paths where libraries
319 | for code generation are installed.
322 | cmdDesc (DataPath) = """
323 | Return a colon-separated list of paths where data files
327 | cmdDesc (AppPath) = """
328 | Return the absolute path to the given application managed by pack.
329 | `pack app-path idris2` returns the path to the current Idris compiler
332 | cmdDesc (Switch) = """
333 | Switch to the given package collection. This will adjust your
334 | `$PACK_DIR/user/pack.toml` file to use the given package
335 | collection. It will also install all auto libs and apps from the
336 | given package collection.
338 | Note: It is also possible to switch to the latest package
339 | collection by using "latest" as the collection name.
342 | cmdDesc (UpdateDB) = """
343 | Update the pack data base by downloading the package collections
344 | from https://github.com/stefan-hoeck/idris2-pack-db.
347 | cmdDesc (CollectGarbage) = """
348 | Clean up installations of older package collections by removing
349 | all sub-directories of `$PACK_STATE_DIR/install` not belonging to the
350 | currently used compiler commit.
352 | In case the `--gc-purge` option is set, this will also remove all
353 | outdated libraries installed with the current compiler commit.
356 | cmdDesc (Info) = """
357 | Print general information about the current package
358 | collection and list installed applications and libraries.
361 | cmdDesc (Query) = """
362 | Query the package collection for the given name.
363 | Several command line options exist to specify the type
364 | of information printed. The optional mode argument
365 | defines the type of query to use:
367 | * `dep` : Search a package by its dependencies. For
368 | instance, `pack query dep sop` will list all packages,
369 | which have a dependency on the sop library. Only exact
370 | matches will be listed.
372 | * `module` : Search a package by its modules. For
373 | instance, `pack query module Data.List` will list all packages,
374 | which export module `Data.List`. Only exact matches will
377 | * none : List packages whose names have the query
378 | string as a substring.
380 | The following command-line options affect the kind of information displayed
381 | for each found package:
383 | -d --dependencies : Prints the dependencies of each query result
384 | --tree : Prints a dependency tree of a queried package
385 | --reverse-tree : Prints a tree of packages depending on a queried package
386 | -s --short-desc : Prints the `brief` description from each package's
388 | -l --long-desc : Prints detailed description of each query result
391 | cmdDesc (Fuzzy) = """
392 | Run a fuzzy search by type over a comma-separated list of packages.
393 | If no packages are given, all installed packages will be queried
394 | (which might take several minutes).
396 | Example: fuzzy base "HasIO -> Bool", will find functions taking
397 | an argument of type `HasIO` and returning a boolean result in the
401 | cmdDesc (Completion) = """
402 | Returns a list of possible completion strings for the given arguments.
403 | This is invoked by the shell script returned by `pack \{name $ Trivial CompletionScript}`.
404 | See the installation instructions about how to enable TAB-completion
408 | cmdDesc (Uninstall) = """
410 | Deletes the $PACK_DIR directory.
413 | cmdDesc (PrintHelp) = """
414 | Without an additional <cmd> argument, this prints general information
415 | about using pack, including a list of available command-line options
416 | and a description of what each of them does.
418 | If an explicit command is given, this gives some detail about what
419 | the command in question does and what additional arguments it takes.
421 | Available commands:
422 | \{unlines $ map (indent 2 . fst) namesAndCommands}
430 | commands : List TrivialCmd
437 | name : TrivialCmd -> String
438 | name (CompletionScript) = "completion-script"
442 | namesAndCommands : List (String, TrivialCmd)
443 | namesAndCommands = map (\c => (name c, c)) commands
447 | cmdDesc : TrivialCmd -> String
448 | cmdDesc (CompletionScript) = """
449 | Prints a shell script, which can be used for BASH-like TAB-completion.
450 | See the installation instructions about how to enable TAB-completion
458 | name (Trivial cmd) = Trivial.name cmd
459 | name (Configured cmd) = Configured.name cmd
463 | namesAndCommands : List (String, Cmd)
465 | map (\c => (name c, Configured c)) Configured.commands
466 | ++ map (\c => (name c, Trivial c)) Trivial.commands
469 | Arg ConfiguredCmd where
472 | readArg = parseSingleMaybe (`lookup` namesAndCommands)
475 | Arg TrivialCmd where
478 | readArg = parseSingleMaybe (`lookup` namesAndCommands)
484 | readArg = parseSingleMaybe (`lookup` namesAndCommands)
490 | 0 configuredCmdInCommands : (c : ConfiguredCmd) -> Elem c Configured.commands
491 | configuredCmdInCommands (Build ) = %search
492 | configuredCmdInCommands (BuildDeps ) = %search
493 | configuredCmdInCommands (Typecheck ) = %search
494 | configuredCmdInCommands (Clean ) = %search
495 | configuredCmdInCommands (CleanBuild ) = %search
496 | configuredCmdInCommands (Repl ) = %search
497 | configuredCmdInCommands (Exec ) = %search
498 | configuredCmdInCommands (Install ) = %search
499 | configuredCmdInCommands (InstallApp ) = %search
500 | configuredCmdInCommands (Remove ) = %search
501 | configuredCmdInCommands (RemoveApp ) = %search
502 | configuredCmdInCommands (Run ) = %search
503 | configuredCmdInCommands (Test ) = %search
504 | configuredCmdInCommands (New ) = %search
505 | configuredCmdInCommands (Update ) = %search
506 | configuredCmdInCommands (Fetch ) = %search
507 | configuredCmdInCommands (PackagePath ) = %search
508 | configuredCmdInCommands (LibsPath ) = %search
509 | configuredCmdInCommands (DataPath ) = %search
510 | configuredCmdInCommands (AppPath ) = %search
511 | configuredCmdInCommands (Switch ) = %search
512 | configuredCmdInCommands (UpdateDB ) = %search
513 | configuredCmdInCommands (CollectGarbage ) = %search
514 | configuredCmdInCommands (Info ) = %search
515 | configuredCmdInCommands (Query ) = %search
516 | configuredCmdInCommands (Fuzzy ) = %search
517 | configuredCmdInCommands (Completion ) = %search
518 | configuredCmdInCommands (Uninstall ) = %search
519 | configuredCmdInCommands (PrintHelp ) = %search
521 | 0 trivialCmdInCommands : (c : TrivialCmd) -> Elem c Trivial.commands
522 | trivialCmdInCommands (CompletionScript) = %search