Abbreviate help command

[andreiburdusa]

---

Fixes #1957
Please see also the wiki

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[andreiburdusa]

@ttuegel
Now each command description except log is at most 140 characters, and fits on a single line on my usual terminal window.

Kore (0)> help
Available commands in the Kore REPL: 
help                                     shows this help message
claim [n|<name>]                         shows the nth claim, the claim with <name> or (default) the currently focused claim
axiom <n|name>                           shows the nth axiom or the axiom with <name>
prove <n|name>                           initializes proof mode for the nth claim or for the claim with <name>
graph [view] [file] [format]             shows the current proof graph (*), 'expanded' or 'collapsed'; or saves it as jpeg, png, pdf or svg
step [n]                                 attempts to run 'n' proof steps at the current node (n=1 by default)
stepf [n]                                like step, but goes through branchings to the first interesting branching node (**)
select <n>                               select node id 'n' from the graph
config [n]                               shows the config for node 'n' (defaults to current node)
dest [n]                                 shows the destination for node 'n' (defaults to current node)
omit [cell]                              adds or removes cell to omit list (defaults to showing the omit list)
leafs                                    shows unevaluated or stuck leafs
rule [n]                                 shows the rule for node 'n' (defaults to current node)
rules <n1> <n2>                          shows the rules applied on the path between nodes n1 and n2
prec-branch [n]                          shows first preceding branch (defaults to current node)
children [n]                             shows direct children of node (defaults to current node)
label                                    shows all node labels
label <l>                                jump to a label
label <+l> [n]                           add a new label for a node (defaults to current node)
label <-l>                               remove a label
try (<a|c><num>)|<name>                  attempts <a>xiom or <c>laim at index <num> or rule with <name>
tryf (<a|c><num>)|<name>                 like try, but if successful, it will apply the axiom or claim.
clear [n]                                removes all the node's children from the proof graph (***) (defaults to current node)
save-session file                        saves the current session to file
save-partial-proof [n] file              writes a new claim with the config 'n' as its LHS and all other claims marked as trusted
alias <name> = <command>                 adds as an alias for <command>
<alias>                                  runs an existing alias
load file                                loads the file as a repl script
proof-status                             shows status for each claim
log [<severity>] "["<entry>"]"           configures logging; <severity> can be debug ... error; [<entry>] is a list formed by types below;
    <type> <switch-timestamp>            <type> can be stderr or 'file filename'; <switch-timestamp> can be (enable|disable)-log-timestamps;
debug[-type-]equation [eqId1] [eqId2] .. show debugging information for specific equations; [-type-] can be '-attempt-', '-apply-' or '-',
exit                                     exits the repl

Available modifiers:
<command> > file                         prints the output of 'command' to file
<command> >> file                        appends the output of 'command' to file
<command> | external_script              pipes command to external script and prints the result in the repl; can be redirected using > or >>

Rule names can be added in two ways:
    a) rule <k> ... </k> [label(myName)]
       - can be used as-is
       - ! do not add names which match the indexing syntax for the try command
    b) rule [myName] : <k> ... </k>
       - need to be prefixed with the module name, e.g. IMP.myName

Available entry types:
DebugAppliedRewriteRules                DebugUnification                        InfoExecDepth                           
DebugApplyEquation                      ErrorBottomTotalFunction                InfoProofDepth                          
DebugAttemptEquation                    ErrorDecidePredicateUnknown             InfoReachability                        
DebugEvaluateCondition                  ErrorException                          LogMessage                              
DebugProofState                         ErrorRewriteLoop                        WarnFunctionWithoutEvaluators           
DebugSolverRecv                         ErrorRewritesInstantiation              WarnStuckProofState                     
DebugSolverSend                         InfoAttemptUnification                  WarnSymbolSMTRepresentation             
DebugSubstitutionSimplifier             InfoExecBreadth                                                                 

(*) If an edge is labeled as Simpl/RD it means that the target node
 was reached using either the SMT solver or the Remove Destination step.
    A green node represents the proof has completed on that respective branch. 
    A red node represents a stuck configuration.
(**) An interesting branching node has at least two children which
 contain non-bottom leaves in their subtrees. If no such node exists,
 the current node is advanced to the (only) non-bottom leaf. If no such
 leaf exists (i.e the proof is complete), the current node remains the same
 and a message is emitted.
(***) The clear command doesn't allow the removal of nodes which are direct
 descendants of branchings. The steps which create branchings cannot be
 partially redone. Therefore, if this were allowed it would result in invalid proofs.

For more details see https://github.com/kframework/kore/wiki/Kore-REPL#available-commands-in-the-kore-repl