[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)

A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.

Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.

This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.

* [ repl ] Use unlines for detailed help (see #2087)

  Ideally, the lines affected should be multiline strings. But for some
  arcane reason, newlines in those get swallowed in Nix and Windows
  **CI** only Ô.o
  This was already documented in issue #2087.

* [ new ] --except for golden testing lib

  To allow CI to pass despite #2087

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

.github/workflows/ci-idris2.yml

@@ -301,7 +301,7 @@ jobs:
       - name: Build self-hosted
         run: make all IDRIS2_BOOT="idris2 -Werror" && make install
       - name: Test self-hosted
-        run: make test INTERACTIVE=''
+        run: make ci-ubuntu-test INTERACTIVE=''
 
   macos-self-host-chez:
     needs: macos-bootstrap-chez
@@ -326,7 +326,7 @@ jobs:
         run: make all IDRIS2_BOOT="idris2 -Werror" && make install
         shell: bash
       - name: Test self-hosted
-        run: make test INTERACTIVE=''
+        run: make ci-macos-test INTERACTIVE=''
         shell: bash
 
   # RACKET
@@ -353,7 +353,7 @@ jobs:
       - name: Build self-hosted
         run: make all IDRIS2_BOOT="idris2 -Werror" && make install
       - name: Test self-hosted
-        run: make test INTERACTIVE=''
+        run: make ci-ubuntu-test INTERACTIVE=''
 
   ubuntu-self-host-previous-version:
     needs: quick-check
@@ -381,7 +381,7 @@ jobs:
       - name: Build self-hosted from previous version
         run: make all IDRIS2_BOOT="idris2 -Werror" && make install
       - name: Test self-hosted from previous version
-        run: make test INTERACTIVE=''
+        run: make ci-ubuntu-test INTERACTIVE=''
       - name: Artifact Idris2
         uses: actions/upload-artifact@v2
         with:
@@ -440,7 +440,7 @@ jobs:
           c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make"
       # TODO: fix the broken tests!
       # - name: Test
-      #  run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make test"
+      #  run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make ci-windows-test"
       - name: Install
         run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make install"
 

CHANGELOG.md

@@ -11,6 +11,8 @@
   set with `:set evaltiming`.
 * Renames `:lp/loadpackage` to `:package`.
 * Adds `:import`, with the same functionality as `:module`.
+* Adds the ability to request detailed help via `:help <replCmd>`, e.g.
+  `:help :help` or `:help :let`. This also works with the `:?` and `:h` aliases.
 
 ### Language changes
 

Makefile

@@ -133,12 +133,18 @@ testenv:
 testenv-clean:
 	$(RM) -r ${TEST_PREFIX}/${NAME_VERSION}
 
+ci-ubuntu-test: test
+ci-macos-test: test
+ci-windows-test:
+	@${MAKE} test except="idris2/repl005"
+
 test: testenv
 	@echo
 	@echo "NOTE: \`${MAKE} test\` does not rebuild Idris or the libraries packaged with it; to do that run \`${MAKE}\`"
 	@if [ ! -x "${TARGET}" ]; then echo "ERROR: Missing IDRIS2 executable. Cannot run tests!\n"; exit 1; fi
 	@echo
-	@${MAKE} -C tests only=$(only) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
+	@${MAKE} -C tests only=$(only) except=$(except) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
+
 
 retest: testenv
 	@echo

libs/test/Test/Golden.idr

@@ -64,7 +64,7 @@
 |||   [--failure-file PATH]
 |||   [--threads N]
 |||   [--cg CODEGEN]
-|||   [--only [NAMES]]
+|||   [[--only|--except] [NAMES]]
 |||```
 |||
 ||| assuming that the test runner is compiled to an executable named `runtests`.
@@ -135,7 +135,7 @@ usage = unwords
   , "[--threads N]"
   , "[--failure-file PATH]"
   , "[--only-file PATH]"
-  , "[--only [NAMES]]"
+  , "[[--only|--except] [NAMES]]"
   ]
 
 export
@@ -144,9 +144,20 @@ fail err
     = do putStrLn err
          exitWith (ExitFailure 1)
 
-optionsTestsFilter : List String -> Maybe (String -> Bool)
-optionsTestsFilter [] = Nothing
-optionsTestsFilter xs = Just $ \name => any (`isInfixOf` name) xs
+optionsTestsFilter : List String -> List String -> Maybe (String -> Bool)
+optionsTestsFilter [] [] = Nothing
+optionsTestsFilter only except = Just $ \ name =>
+  let onlyCheck = null only || any (`isInfixOf` name) only in
+  let exceptCheck = all (not . (`isInfixOf` name)) except in
+  onlyCheck && exceptCheck
+
+record Acc where
+  constructor MkAcc
+  onlyFile : Maybe String
+  onlyNames : List String
+  exceptNames : List String
+initAcc : Acc
+initAcc = MkAcc Nothing [] []
 
 ||| Process the command line options.
 export
@@ -157,39 +168,35 @@ options args = case args of
 
   where
 
-    go : List String -> Maybe String -> Options -> Maybe (Maybe String, Options)
-    go rest only opts = case rest of
-      []                            => pure (only, opts)
-      ("--timing" :: xs)            => go xs only ({ timing := True} opts)
-      ("--interactive" :: xs)       => go xs only ({ interactive := True } opts)
-      ("--color"  :: xs)            => go xs only ({ color := True } opts)
-      ("--colour" :: xs)            => go xs only ({ color := True } opts)
-      ("--no-color"  :: xs)         => go xs only ({ color := False } opts)
-      ("--no-colour" :: xs)         => go xs only ({ color := False } opts)
-      ("--cg" :: cg :: xs)          => go xs only ({ codegen := Just cg } opts)
+    go : List String -> Acc -> Options -> Maybe (Acc, Options)
+    go rest acc opts = case rest of
+      []                            => pure (acc, opts)
+      ("--timing" :: xs)            => go xs acc ({ timing := True} opts)
+      ("--interactive" :: xs)       => go xs acc ({ interactive := True } opts)
+      ("--color"  :: xs)            => go xs acc ({ color := True } opts)
+      ("--colour" :: xs)            => go xs acc ({ color := True } opts)
+      ("--no-color"  :: xs)         => go xs acc ({ color := False } opts)
+      ("--no-colour" :: xs)         => go xs acc ({ color := False } opts)
+      ("--cg" :: cg :: xs)          => go xs acc ({ codegen := Just cg } opts)
       ("--threads" :: n :: xs)      => do let pos : Nat = !(parsePositive n)
-                                          go xs only ({ threads := pos } opts)
-      ("--failure-file" :: p :: xs) => go  xs only ({ failureFile := Just p } opts)
-      ("--only" :: xs)              => pure (only, { onlyNames := optionsTestsFilter xs } opts)
-      ("--only-file" :: p :: xs)    => go xs (Just p) opts
+                                          go xs acc ({ threads := pos } opts)
+      ("--failure-file" :: p :: xs) => go  xs acc ({ failureFile := Just p } opts)
+      ("--only" :: p :: xs)         => go xs ({ onlyNames $= (words p ++) } acc) opts
+      ("--except" :: p :: xs)       => go xs ({ exceptNames $= (words p ++) } acc) opts
+      ("--only-file" :: p :: xs)    => go xs ({ onlyFile := Just p } acc) opts
       _ => Nothing
 
     mkOptions : String -> List String -> IO (Maybe Options)
     mkOptions exe rest
       = do color <- (Just "DUMB" /=) <$> getEnv "TERM"
-           let Just (mfp, opts) = go rest Nothing (initOptions exe color)
+           let Just (acc, opts) = go rest initAcc (initOptions exe color)
                  | Nothing => pure Nothing
-           let Just fp = mfp
-                 | Nothing => pure (Just opts)
-           Right only <- readFile fp
-             | Left err => fail (show err)
-           pure $ Just $ { onlyNames $= mergeOnlys $ optionsTestsFilter (lines only) } opts
-      where
-        mergeOnlys : Maybe (String -> Bool) -> Maybe (String -> Bool) -> Maybe (String -> Bool)
-        mergeOnlys Nothing   Nothing   = Nothing
-        mergeOnlys (Just f1) Nothing   = Just f1
-        mergeOnlys Nothing   (Just f2) = Just f2
-        mergeOnlys (Just f1) (Just f2) = Just $ \x => f1 x || f2 x
+           extraOnlyNames <- the (IO (List String)) $ case acc.onlyFile of
+                               Nothing => pure []
+                               Just fp => do Right only <- readFile fp
+                                               | Left err => fail (show err)
+                                             pure (lines only)
+           pure $ Just $ { onlyNames := optionsTestsFilter (extraOnlyNames ++ acc.onlyNames) acc.exceptNames } opts
 
 ||| Normalise strings between different OS.
 |||

src/Idris/IDEMode/REPL.idr

@@ -330,6 +330,8 @@ displayIDEResult outf i  (REPL $ REPLError err)
   = printIDEError outf i err
 displayIDEResult outf i  (REPL RequestedHelp  )
   = printIDEResult outf i $ AString displayHelp
+displayIDEResult outf i  (REPL $ RequestedDetails details)
+  = printIDEResult outf i $ AString details
 displayIDEResult outf i  (REPL $ Evaluated x Nothing)
   = printIDEResultWithHighlight outf i
   $ mapFst AString

src/Idris/Parser.idr

@@ -11,8 +11,10 @@ import public Libraries.Text.Parser
 import Data.Either
 import Libraries.Data.IMaybe
 import Data.List
+import Data.List.Quantifiers
 import Data.List1
 import Data.Maybe
+import Data.So
 import Data.Nat
 import Data.SnocList
 import Data.String
@@ -1943,6 +1945,17 @@ replCmd (c :: cs)
   <|> symbol c
   <|> replCmd cs
 
+cmdName : String -> Rule String
+cmdName str = do
+  _ <- optional (symbol ":")
+  terminal ("Unrecognised REPL command '" ++ str ++ "'") $
+           \case
+              (Ident s)       => if s == str then Just s else Nothing
+              (Keyword kw)    => if kw == str then Just kw else Nothing
+              (Symbol "?")    => Just "?"
+              (Symbol ":?")   => Just "?"   -- `:help :?` is a special case
+              _ => Nothing
+
 export
 data CmdArg : Type where
      ||| The command takes no arguments.
@@ -2021,11 +2034,142 @@ mutual
     show (Args args) = showSep " " (map show args)
     show arg = "<" ++ showCmdArg arg ++ ">"
 
+public export
+knownCommands : List (String, String)
+knownCommands =
+  explain ["t", "type"] "Check the type of an expression" ++
+  [ ("ti", "Check the type of an expression, showing implicit arguments")
+  , ("printdef", "Show the definition of a pattern-matching function")
+  ] ++
+  explain ["s", "search"] "Search for values by type" ++
+  [ ("di", "Show debugging information for a name")
+  ] ++
+  explain ["module", "import"] "Import an extra module" ++
+  [ ("package", "Import every module of the package")
+  ] ++
+  explain ["q", "quit", "exit"] "Exit the Idris system" ++
+  [ ("cwd", "Displays the current working directory")
+  , ("cd", "Change the current working directory")
+  , ("sh", "Run a shell command")
+  , ("set"
+    , unlines   -- FIXME: this should be a multiline string (see #2087)
+      [ "Set an option"
+      , "  eval                specify what evaluation mode to use:"
+      , "                        typecheck|tc"
+      , "                        normalise|normalize|normal"
+      , "                        execute|exec"
+      , "                        scheme"
+      , ""
+      , "  editor              specify the name of the editor command"
+      , ""
+      , "  cg                  specify the codegen/backend to use"
+      , "                      builtin codegens are:"
+      , "                        chez"
+      , "                        racket"
+      , "                        refc"
+      , "                        node"
+      , ""
+      , "  showimplicits       enable displaying implicit arguments as part of the"
+      , "                      output"
+      , ""
+      , "  shownamespace       enable displaying namespaces as part of the output"
+      , ""
+      , "  showmachinenames    enable displaying machine names as part of the"
+      , "                      output"
+      , ""
+      , "  showtypes           enable displaying the type of the term as part of"
+      , "                      the output"
+      , ""
+      , "  profile"
+      , ""
+      , "  evaltiming          enable timing how long evaluation takes and"
+      , "                      displaying this before the printing of the output"
+      ]
+    )
+  , ("unset", "Unset an option")
+  , ("opts", "Show current options settings")
+  ] ++
+  explain ["c", "compile"] "Compile to an executable" ++
+  [ ("exec", "Compile to an executable and run")
+  , ("directive", "Set a codegen-specific directive")
+  ] ++
+  explain ["l", "load"] "Load a file" ++
+  explain ["r", "reload"] "Reload current file" ++
+  explain ["e", "edit"] "Edit current file using $EDITOR or $VISUAL" ++
+  explain ["miss", "missing"] "Show missing clauses" ++
+  [ ("total", "Check the totality of a name")
+  , ("doc", "Show documentation for a keyword, a name, or a primitive")
+  , ("browse", "Browse contents of a namespace")
+  ] ++
+  explain ["log", "logging"] "Set logging level" ++
+  [ ("consolewidth", "Set the width of the console output (0 for unbounded) (auto by default)")
+  ] ++
+  explain ["colour", "color"] "Whether to use colour for the console output (enabled by default)" ++
+  explain ["m", "metavars"] "Show remaining proof obligations (metavariables or holes)" ++
+  [ ("typeat", "Show type of term <n> defined on line <l> and column <c>")
+  ] ++
+  explain ["cs", "casesplit"] "Case split term <n> defined on line <l> and column <c>" ++
+  explain ["ac", "addclause"] "Add clause to term <n> defined on line <l>" ++
+  explain ["ml", "makelemma"] "Make lemma for term <n> defined on line <l>" ++
+  explain ["mc", "makecase"] "Make case on term <n> defined on line <l>" ++
+  explain ["mw", "makewith"] "Add with expression on term <n> defined on line <l>" ++
+  [ ("intro", "Introduce unambiguous constructor in hole <n> defined on line <l>")
+  , ("refine", "Refine hole <h> with identifier <n> on line <l> and column <c>")
+  ] ++
+  explain ["ps", "proofsearch"] "Search for a proof" ++
+  [ ("psnext", "Show next proof")
+  , ("gd", "Try to generate a definition using proof-search")
+  , ("gdnext", "Show next definition")
+  , ("version", "Display the Idris version")
+  ] ++
+  explain ["?", "h", "help"] (unlines     -- FIXME: this should be a multiline string (see #2087)
+        [ "Display help text, optionally of a specific command.\n"
+        , "If run without arguments, lists all the REPL commands along with their"
+        , "initial line of help text.\n"
+        , "More detailed help can then be obtained by running the :help command"
+        , "with another command as an argument, e.g."
+        , "  > :help :help"
+        , "  > :help :set"
+        , "(the leading ':' in the command argument is optional)"
+        ] ) ++
+  [ ( "let"
+    , """
+      Define a new value.
+
+      First, declare the type of your new value, e.g.
+        :let myValue : List Nat
+
+      Then, define the value:
+        :let myValue = [1, 2, 3]
+
+      Now the value is in scope at the REPL:
+        > map (+ 2) myValue
+        [3, 4, 5]
+      """
+    )
+  ] ++
+  explain ["fs", "fsearch"] "Search for global definitions by sketching the names distribution of the wanted type(s)."
+  where
+    explain : List String -> String -> List (String, String)
+    explain cmds expl = map (\s => (s, expl)) cmds
+
+public export
+KnownCommand : String -> Type
+KnownCommand cmd = IsJust (lookup cmd knownCommands)
+
 export
 data ParseCmd : Type where
-     ParseREPLCmd : List String -> ParseCmd
-     ParseKeywordCmd : List String -> ParseCmd
-     ParseIdentCmd : String -> ParseCmd
+     ParseREPLCmd :  (cmds : List String)
+                  -> {auto 0 _ : All KnownCommand cmds}
+                  -> ParseCmd
+
+     ParseKeywordCmd :  (cmds : List String)
+                     -> {auto 0 _ : All KnownCommand cmds}
+                     -> ParseCmd
+
+     ParseIdentCmd :  (cmd : String)
+                   -> {auto 0 _ : KnownCommand cmd}
+                   -> ParseCmd
 
 public export
 CommandDefinition : Type
@@ -2084,6 +2228,31 @@ stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
       s <- mustWork simpleStr
       pure (command s)
 
+getHelpType : EmptyRule HelpType
+getHelpType = do
+  optCmd <- optional $ choice $ (cmdName . fst) <$> knownCommands
+  pure $
+    case optCmd of
+         Nothing => GenericHelp
+         Just cmd => DetailedHelp $ fromMaybe "Unrecognised command '\{cmd}'"
+                                  $ lookup cmd knownCommands
+
+helpCmd :  ParseCmd
+        -> (HelpType -> REPLCmd)
+        -> String
+        -> CommandDefinition
+helpCmd parseCmd command doc = (names, StringArg, doc, parse)
+  where
+    names : List String
+    names = extractNames parseCmd
+
+    parse : Rule REPLCmd
+    parse = do
+      symbol ":"
+      runParseCmd parseCmd
+      helpType <- getHelpType
+      pure (command helpType)
+
 moduleArgCmd : ParseCmd -> (ModuleIdent -> REPLCmd) -> String -> CommandDefinition
 moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
   where
@@ -2348,53 +2517,59 @@ editLineNameOptionArgCmd parseCmd command doc =
     nreject <- fromInteger <$> option 0 intLit
     pure (Editing $ command upd line n nreject)
 
+firstHelpLine : (cmd : String) -> {auto 0 _ : KnownCommand cmd} -> String
+firstHelpLine cmd =
+  head . (split ((==) '\n')) $
+  fromMaybe "Failed to look up '\{cmd}' (SHOULDN'T HAPPEN!)" $
+  lookup cmd knownCommands
+
 export
 parserCommandsForHelp : CommandTable
 parserCommandsForHelp =
-  [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
-  , exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits "Check the type of an expression, showing implicit arguments"
-  , exprArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
-  , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch "Search for values by type"
-  , nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
-  , moduleArgCmd (ParseKeywordCmd ["module", "import"]) ImportMod "Import an extra module"
-  , stringArgCmd (ParseREPLCmd ["package"]) ImportPackage "Import every module of the package"
-  , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
-  , noArgCmd (ParseREPLCmd ["cwd"]) CWD "Displays the current working directory"
-  , stringArgCmd (ParseREPLCmd ["cd"]) CD "Change the current working directory"
-  , stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand "Run a shell command"
-  , optArgCmd (ParseIdentCmd "set") SetOpt True "Set an option"
-  , optArgCmd (ParseIdentCmd "unset") SetOpt False "Unset an option"
-  , noArgCmd (ParseREPLCmd ["opts"]) GetOpts "Show current options settings"
-  , compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile "Compile to an executable"
-  , exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
-  , stringArgCmd (ParseIdentCmd "directive") CGDirective "Set a codegen-specific directive"
-  , stringArgCmd (ParseREPLCmd ["l", "load"]) Load "Load a file"
-  , noArgCmd (ParseREPLCmd ["r", "reload"]) Reload "Reload current file"
-  , noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
-  , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
-  , nameArgCmd (ParseKeywordCmd ["total"]) Total "Check the totality of a name"
-  , docArgCmd (ParseIdentCmd "doc") Doc "Show documentation for a keyword, a name, or a primitive"
-  , moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) "Browse contents of a namespace"
-  , loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog "Set logging level"
-  , autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth "Set the width of the console output (0 for unbounded) (auto by default)"
-  , onOffArgCmd (ParseREPLCmd ["color", "colour"]) SetColor "Whether to use color for the console output (enabled by default)"
-  , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
-  , editLineColNameArgCmd (ParseREPLCmd ["typeat"]) (const TypeAt) "Show type of term <n> defined on line <l> and column <c>"
-  , editLineColNameArgCmd (ParseREPLCmd ["cs", "casesplit"]) CaseSplit "Case split term <n> defined on line <l> and column <c>"
-  , editLineNameArgCmd (ParseREPLCmd ["ac", "addclause"]) AddClause "Add clause to term <n> defined on line <l>"
-  , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma "Make lemma for term <n> defined on line <l>"
-  , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase "Make case on term <n> defined on line <l>"
-  , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith "Add with expression on term <n> defined on line <l>"
-  , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro "Introduce unambiguous constructor in hole <n> defined on line <l>"
-  , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine "Refine hole <h> with identifier <n> on line <l> and column <c>"
-  , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch "Search for a proof"
-  , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) "Show next proof"
-  , editLineNameOptionArgCmd (ParseREPLCmd ["gd"]) GenerateDef "Search for a proof"
-  , noArgCmd (ParseREPLCmd ["gdnext"]) (Editing GenerateDefNext) "Show next definition"
-  , noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
-  , noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
-  , declsArgCmd (ParseKeywordCmd ["let"]) NewDefn "Define a new value"
-  , exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch "Search for global definitions by sketching the names distribution of the wanted type(s)."
+  [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check (firstHelpLine "t")
+  , exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits (firstHelpLine "ti")
+  , exprArgCmd (ParseREPLCmd ["printdef"]) PrintDef (firstHelpLine "printdef")
+  , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch (firstHelpLine "s")
+  , nameArgCmd (ParseIdentCmd "di") DebugInfo (firstHelpLine "di")
+  , moduleArgCmd (ParseKeywordCmd ["module", "import"]) ImportMod (firstHelpLine "module")
+  , stringArgCmd (ParseREPLCmd ["package"]) ImportPackage (firstHelpLine "package")
+  , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit (firstHelpLine "q")
+  , noArgCmd (ParseREPLCmd ["cwd"]) CWD (firstHelpLine "cwd")
+  , stringArgCmd (ParseREPLCmd ["cd"]) CD (firstHelpLine "cd")
+  , stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand (firstHelpLine "sh")
+  , optArgCmd (ParseIdentCmd "set") SetOpt True (firstHelpLine "set")
+  , optArgCmd (ParseIdentCmd "unset") SetOpt False (firstHelpLine "unset")
+  , noArgCmd (ParseREPLCmd ["opts"]) GetOpts (firstHelpLine "opts")
+  , compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile (firstHelpLine "c")
+  , exprArgCmd (ParseIdentCmd "exec") Exec (firstHelpLine "exec")
+  , stringArgCmd (ParseIdentCmd "directive") CGDirective (firstHelpLine "directive")
+  , stringArgCmd (ParseREPLCmd ["l", "load"]) Load (firstHelpLine "l")
+  , noArgCmd (ParseREPLCmd ["r", "reload"]) Reload (firstHelpLine "r")
+  , noArgCmd (ParseREPLCmd ["e", "edit"]) Edit (firstHelpLine "e")
+  , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing (firstHelpLine "miss")
+  , nameArgCmd (ParseKeywordCmd ["total"]) Total (firstHelpLine "total")
+  , docArgCmd (ParseIdentCmd "doc") Doc (firstHelpLine "doc")
+  , moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) (firstHelpLine "browse")
+  , loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog (firstHelpLine "log")
+  , autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth (firstHelpLine "consolewidth")
+  , onOffArgCmd (ParseREPLCmd ["colour", "color"]) SetColor (firstHelpLine "colour")
+  , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars (firstHelpLine "m")
+  , editLineColNameArgCmd (ParseREPLCmd ["typeat"]) (const TypeAt) (firstHelpLine "typeat")
+  , editLineColNameArgCmd (ParseREPLCmd ["cs", "casesplit"]) CaseSplit (firstHelpLine "cs")
+  , editLineNameArgCmd (ParseREPLCmd ["ac", "addclause"]) AddClause (firstHelpLine "ac")
+  , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma (firstHelpLine "ml")
+  , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase (firstHelpLine "mc")
+  , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith (firstHelpLine "mw")
+  , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro (firstHelpLine "intro")
+  , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine (firstHelpLine "refine")
+  , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch (firstHelpLine "ps")
+  , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) (firstHelpLine "psnext")
+  , editLineNameOptionArgCmd (ParseREPLCmd ["gd"]) GenerateDef (firstHelpLine "gd")
+  , noArgCmd (ParseREPLCmd ["gdnext"]) (Editing GenerateDefNext) (firstHelpLine "gdnext")
+  , noArgCmd (ParseREPLCmd ["version"]) ShowVersion (firstHelpLine "version")
+  , helpCmd (ParseREPLCmd ["?", "h", "help"]) Help (firstHelpLine "?")
+  , declsArgCmd (ParseKeywordCmd ["let"]) NewDefn (firstHelpLine "let")
+  , exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch (firstHelpLine "fs")
   ]
 
 export
@@ -2421,5 +2596,8 @@ command : EmptyRule REPLCmd
 command
     = eoi $> NOP
   <|> nonEmptyCommand
-  <|> symbol ":?" $> Help -- special case, :? doesn't fit into above scheme
+  <|> (do symbol ":?" -- special case, :? doesn't fit into above scheme
+          helpType <- getHelpType
+          pure $ Help helpType)
   <|> eval
+

src/Idris/REPL.idr

@@ -972,8 +972,10 @@ process (Compile ctm outfile)
     = compileExp ctm outfile
 process (Exec ctm)
     = execExp ctm
-process Help
+process (Help GenericHelp)
     = pure RequestedHelp
+process (Help (DetailedHelp details))
+    = pure (RequestedDetails details)
 process (TypeSearch searchTerm)
     = do defs <- branch
          let curr = currentNS defs
@@ -1254,6 +1256,7 @@ mutual
   displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))
   displayResult (VersionIs x) = printResult (pretty0 (showVersion True x))
   displayResult (RequestedHelp) = printResult (pretty0 displayHelp)
+  displayResult (RequestedDetails details) = printResult (pretty0 details)
   displayResult (Edited (DisplayEdit Empty)) = pure ()
   displayResult (Edited (DisplayEdit xs)) = printResult xs
   displayResult (Edited (EditError x)) = printResult x

src/Idris/REPL/Common.idr

@@ -214,6 +214,7 @@ data REPLResult : Type where
   REPLError : Doc IdrisAnn -> REPLResult
   Executed : PTerm -> REPLResult
   RequestedHelp : REPLResult
+  RequestedDetails : String -> REPLResult
   Evaluated : IPTerm -> Maybe IPTerm -> REPLResult
   Printed : Doc IdrisAnn -> REPLResult
   PrintedDoc : Doc IdrisDocAnn -> REPLResult

src/Idris/Syntax.idr

@@ -582,6 +582,11 @@ data DocDirective : Type where
   ||| A module name
   AModule : ModuleIdent -> DocDirective
 
+public export
+data HelpType : Type where
+  GenericHelp : HelpType
+  DetailedHelp : (details : String) -> HelpType
+
 public export
 data REPLCmd : Type where
      NewDefn : List PDecl -> REPLCmd
@@ -595,7 +600,7 @@ data REPLCmd : Type where
      Edit : REPLCmd
      Compile : PTerm -> String -> REPLCmd
      Exec : PTerm -> REPLCmd
-     Help : REPLCmd
+     Help : HelpType -> REPLCmd
      TypeSearch : PTerm -> REPLCmd
      FuzzyTypeSearch : PTerm -> REPLCmd
      DebugInfo : Name -> REPLCmd

tests/Main.idr

@@ -187,7 +187,7 @@ idrisTestsEvaluator = MkTestPool "Evaluation" [] Nothing
 
 idrisTestsREPL : TestPool
 idrisTestsREPL = MkTestPool "REPL commands and help" [] Nothing
-      [ "repl001", "repl002"
+      [ "repl001", "repl002", "repl003", "repl004", "repl005"
       ]
 
 idrisTestsAllSchemes : Requirement -> TestPool

tests/Makefile

@@ -4,10 +4,10 @@ threads ?= $(shell (nproc || sysctl -n hw.ncpu) 2>/dev/null || echo 1)
 .PHONY: testbin test
 
 test:
-	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --timing --failure-file failures --threads $(threads) --only $(only)
+	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --timing --failure-file failures --threads $(threads) --only $(only) --except $(except)
 
 retest:
-	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --timing --failure-file failures --threads $(threads) --only-file failures --only $(only)
+	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --timing --failure-file failures --threads $(threads) --only-file failures --only $(only) --except $(except)
 
 testbin:
 	${IDRIS2} --build tests.ipkg

tests/idris2/repl001/expected

@@ -1,7 +1,7 @@
 Main>  <expr>                                                Evaluate an expression
  :t :type          <expr>                              Check the type of an expression
  :ti               <expr>                              Check the type of an expression, showing implicit arguments
- :printdef         <expr>                              Show the definition of a function
+ :printdef         <expr>                              Show the definition of a pattern-matching function
  :s :search        <expr>                              Search for values by type
  :di               <name>                              Show debugging information for a name
  :module :import   <module>                            Import an extra module
@@ -25,7 +25,7 @@ Main>  <expr>                                                Evaluate an express
  :browse           <module>                            Browse contents of a namespace
  :log :logging     <string> <number>                   Set logging level
  :consolewidth     <number|auto>                       Set the width of the console output (0 for unbounded) (auto by default)
- :color :colour    (on|off)                            Whether to use color for the console output (enabled by default)
+ :colour :color    (on|off)                            Whether to use colour for the console output (enabled by default)
  :m :metavars                                          Show remaining proof obligations (metavariables or holes)
  :typeat           <l:number> <c:number> <n:string>    Show type of term <n> defined on line <l> and column <c>
  :cs :casesplit    <l:number> <c:number> <n:string>    Case split term <n> defined on line <l> and column <c>
@@ -37,11 +37,101 @@ Main>  <expr>                                                Evaluate an express
  :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
  :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
  :psnext                                               Show next proof
- :gd               <l:number> <n:string> <r:number|0>  Search for a proof
+ :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search
  :gdnext                                               Show next definition
  :version                                              Display the Idris version
- :? :h :help                                           Display this help text
- :let              <decls>                             Define a new value
+ :? :h :help       <string>                            Display help text, optionally of a specific command.
+ :let              <decls>                             Define a new value.
+ :fs :fsearch      <expr>                              Search for global definitions by sketching the names distribution of the wanted type(s).
+Main>  <expr>                                                Evaluate an expression
+ :t :type          <expr>                              Check the type of an expression
+ :ti               <expr>                              Check the type of an expression, showing implicit arguments
+ :printdef         <expr>                              Show the definition of a pattern-matching function
+ :s :search        <expr>                              Search for values by type
+ :di               <name>                              Show debugging information for a name
+ :module :import   <module>                            Import an extra module
+ :package          <string>                            Import every module of the package
+ :q :quit :exit                                        Exit the Idris system
+ :cwd                                                  Displays the current working directory
+ :cd               <string>                            Change the current working directory
+ :sh               <string>                            Run a shell command
+ :set              <option>                            Set an option
+ :unset            <option>                            Unset an option
+ :opts                                                 Show current options settings
+ :c :compile       <file> <expr>                       Compile to an executable
+ :exec             <expr>                              Compile to an executable and run
+ :directive        <string>                            Set a codegen-specific directive
+ :l :load          <string>                            Load a file
+ :r :reload                                            Reload current file
+ :e :edit                                              Edit current file using $EDITOR or $VISUAL
+ :miss :missing    <name>                              Show missing clauses
+ :total            <name>                              Check the totality of a name
+ :doc              <keyword|expr>                      Show documentation for a keyword, a name, or a primitive
+ :browse           <module>                            Browse contents of a namespace
+ :log :logging     <string> <number>                   Set logging level
+ :consolewidth     <number|auto>                       Set the width of the console output (0 for unbounded) (auto by default)
+ :colour :color    (on|off)                            Whether to use colour for the console output (enabled by default)
+ :m :metavars                                          Show remaining proof obligations (metavariables or holes)
+ :typeat           <l:number> <c:number> <n:string>    Show type of term <n> defined on line <l> and column <c>
+ :cs :casesplit    <l:number> <c:number> <n:string>    Case split term <n> defined on line <l> and column <c>
+ :ac :addclause    <l:number> <n:string>               Add clause to term <n> defined on line <l>
+ :ml :makelemma    <l:number> <n:string>               Make lemma for term <n> defined on line <l>
+ :mc :makecase     <l:number> <n:string>               Make case on term <n> defined on line <l>
+ :mw :makewith     <l:number> <n:string>               Add with expression on term <n> defined on line <l>
+ :intro            <l:number> <n:string>               Introduce unambiguous constructor in hole <n> defined on line <l>
+ :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
+ :psnext                                               Show next proof
+ :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search
+ :gdnext                                               Show next definition
+ :version                                              Display the Idris version
+ :? :h :help       <string>                            Display help text, optionally of a specific command.
+ :let              <decls>                             Define a new value.
+ :fs :fsearch      <expr>                              Search for global definitions by sketching the names distribution of the wanted type(s).
+Main>  <expr>                                                Evaluate an expression
+ :t :type          <expr>                              Check the type of an expression
+ :ti               <expr>                              Check the type of an expression, showing implicit arguments
+ :printdef         <expr>                              Show the definition of a pattern-matching function
+ :s :search        <expr>                              Search for values by type
+ :di               <name>                              Show debugging information for a name
+ :module :import   <module>                            Import an extra module
+ :package          <string>                            Import every module of the package
+ :q :quit :exit                                        Exit the Idris system
+ :cwd                                                  Displays the current working directory
+ :cd               <string>                            Change the current working directory
+ :sh               <string>                            Run a shell command
+ :set              <option>                            Set an option
+ :unset            <option>                            Unset an option
+ :opts                                                 Show current options settings
+ :c :compile       <file> <expr>                       Compile to an executable
+ :exec             <expr>                              Compile to an executable and run
+ :directive        <string>                            Set a codegen-specific directive
+ :l :load          <string>                            Load a file
+ :r :reload                                            Reload current file
+ :e :edit                                              Edit current file using $EDITOR or $VISUAL
+ :miss :missing    <name>                              Show missing clauses
+ :total            <name>                              Check the totality of a name
+ :doc              <keyword|expr>                      Show documentation for a keyword, a name, or a primitive
+ :browse           <module>                            Browse contents of a namespace
+ :log :logging     <string> <number>                   Set logging level
+ :consolewidth     <number|auto>                       Set the width of the console output (0 for unbounded) (auto by default)
+ :colour :color    (on|off)                            Whether to use colour for the console output (enabled by default)
+ :m :metavars                                          Show remaining proof obligations (metavariables or holes)
+ :typeat           <l:number> <c:number> <n:string>    Show type of term <n> defined on line <l> and column <c>
+ :cs :casesplit    <l:number> <c:number> <n:string>    Case split term <n> defined on line <l> and column <c>
+ :ac :addclause    <l:number> <n:string>               Add clause to term <n> defined on line <l>
+ :ml :makelemma    <l:number> <n:string>               Make lemma for term <n> defined on line <l>
+ :mc :makecase     <l:number> <n:string>               Make case on term <n> defined on line <l>
+ :mw :makewith     <l:number> <n:string>               Add with expression on term <n> defined on line <l>
+ :intro            <l:number> <n:string>               Introduce unambiguous constructor in hole <n> defined on line <l>
+ :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
+ :psnext                                               Show next proof
+ :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search
+ :gdnext                                               Show next definition
+ :version                                              Display the Idris version
+ :? :h :help       <string>                            Display help text, optionally of a specific command.
+ :let              <decls>                             Define a new value.
  :fs :fsearch      <expr>                              Search for global definitions by sketching the names distribution of the wanted type(s).
 Main> 
 Bye for now!

tests/idris2/repl001/input

@@ -1 +1,3 @@
+:?
+:h
 :help

tests/idris2/repl003/expected

@@ -0,0 +1,8 @@
+Main> Check the type of an expression
+Main> Check the type of an expression
+Main> Check the type of an expression
+Main> Check the type of an expression
+Main> Check the type of an expression
+Main> Check the type of an expression
+Main> 
+Bye for now!

tests/idris2/repl003/input

@@ -0,0 +1,6 @@
+:? :t
+:h :t
+:help :t
+:? t
+:h t
+:help t

tests/idris2/repl003/run

@@ -0,0 +1 @@
+$1 --no-color --console-width 0 --no-banner < input

tests/idris2/repl004/expected

@@ -0,0 +1,126 @@
+Main> Set an option
+  eval                specify what evaluation mode to use:
+                        typecheck|tc
+                        normalise|normalize|normal
+                        execute|exec
+                        scheme
+
+  editor              specify the name of the editor command
+
+  cg                  specify the codegen/backend to use
+                      builtin codegens are:
+                        chez
+                        racket
+                        refc
+                        node
+
+  showimplicits       enable displaying implicit arguments as part of the
+                      output
+
+  shownamespace       enable displaying namespaces as part of the output
+
+  showmachinenames    enable displaying machine names as part of the
+                      output
+
+  showtypes           enable displaying the type of the term as part of
+                      the output
+
+  profile
+
+  evaltiming          enable timing how long evaluation takes and
+                      displaying this before the printing of the output
+Main> Set an option
+  eval                specify what evaluation mode to use:
+                        typecheck|tc
+                        normalise|normalize|normal
+                        execute|exec
+                        scheme
+
+  editor              specify the name of the editor command
+
+  cg                  specify the codegen/backend to use
+                      builtin codegens are:
+                        chez
+                        racket
+                        refc
+                        node
+
+  showimplicits       enable displaying implicit arguments as part of the
+                      output
+
+  shownamespace       enable displaying namespaces as part of the output
+
+  showmachinenames    enable displaying machine names as part of the
+                      output
+
+  showtypes           enable displaying the type of the term as part of
+                      the output
+
+  profile
+
+  evaltiming          enable timing how long evaluation takes and
+                      displaying this before the printing of the output
+Main> Set an option
+  eval                specify what evaluation mode to use:
+                        typecheck|tc
+                        normalise|normalize|normal
+                        execute|exec
+                        scheme
+
+  editor              specify the name of the editor command
+
+  cg                  specify the codegen/backend to use
+                      builtin codegens are:
+                        chez
+                        racket
+                        refc
+                        node
+
+  showimplicits       enable displaying implicit arguments as part of the
+                      output
+
+  shownamespace       enable displaying namespaces as part of the output
+
+  showmachinenames    enable displaying machine names as part of the
+                      output
+
+  showtypes           enable displaying the type of the term as part of
+                      the output
+
+  profile
+
+  evaltiming          enable timing how long evaluation takes and
+                      displaying this before the printing of the output
+Main> Set an option
+  eval                specify what evaluation mode to use:
+                        typecheck|tc
+                        normalise|normalize|normal
+                        execute|exec
+                        scheme
+
+  editor              specify the name of the editor command
+
+  cg                  specify the codegen/backend to use
+                      builtin codegens are:
+                        chez
+                        racket
+                        refc
+                        node
+
+  showimplicits       enable displaying implicit arguments as part of the
+                      output
+
+  shownamespace       enable displaying namespaces as part of the output
+
+  showmachinenames    enable displaying machine names as part of the
+                      output
+
+  showtypes           enable displaying the type of the term as part of
+                      the output
+
+  profile
+
+  evaltiming          enable timing how long evaluation takes and
+                      displaying this before the printing of the output
+Main> 
+Bye for now!

tests/idris2/repl004/input

@@ -0,0 +1,4 @@
+:? :set
+:help :set
+:? set
+:help set

tests/idris2/repl004/run

@@ -0,0 +1 @@
+$1 --no-color --console-width 0 --no-banner < input

tests/idris2/repl005/expected

@@ -0,0 +1,46 @@
+Main> Define a new value.
+
+First, declare the type of your new value, e.g.
+  :let myValue : List Nat
+
+Then, define the value:
+  :let myValue = [1, 2, 3]
+
+Now the value is in scope at the REPL:
+  > map (+ 2) myValue
+  [3, 4, 5]
+Main> Define a new value.
+
+First, declare the type of your new value, e.g.
+  :let myValue : List Nat
+
+Then, define the value:
+  :let myValue = [1, 2, 3]
+
+Now the value is in scope at the REPL:
+  > map (+ 2) myValue
+  [3, 4, 5]
+Main> Define a new value.
+
+First, declare the type of your new value, e.g.
+  :let myValue : List Nat
+
+Then, define the value:
+  :let myValue = [1, 2, 3]
+
+Now the value is in scope at the REPL:
+  > map (+ 2) myValue
+  [3, 4, 5]
+Main> Define a new value.
+
+First, declare the type of your new value, e.g.
+  :let myValue : List Nat
+
+Then, define the value:
+  :let myValue = [1, 2, 3]
+
+Now the value is in scope at the REPL:
+  > map (+ 2) myValue
+  [3, 4, 5]
+Main> 
+Bye for now!

tests/idris2/repl005/input

@@ -0,0 +1,4 @@
+:? :let
+:help :let
+:? let
+:help let

tests/idris2/repl005/run

@@ -0,0 +1 @@
+$1 --no-color --console-width 0 --no-banner < input