Skip to content

Commit a0876de

Browse files
andreiburdusarv-jenkins
andreiburdusa
and
rv-jenkins
authored
Abbreviate help command (#1999)
* Abbreviate help command * Add \n * Shorten description to one line (140 characters) * Remove space * Rebuild Co-authored-by: rv-jenkins <admin@runtimeverification.com>
1 parent 9401b56 commit a0876de

File tree

1 file changed

+61
-84
lines changed

1 file changed

+61
-84
lines changed

‎kore/src/Kore/Repl/Data.hs‎

Lines changed: 61 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ module Kore.Repl.Data
4242
, debugAttemptEquationTransformer
4343
, debugApplyEquationTransformer
4444
, debugEquationTransformer
45+
, entriesForHelp
4546
) where
4647

4748
import Prelude.Kore
@@ -59,7 +60,7 @@ import Data.Graph.Inductive.PatriciaTree
5960
)
6061
import qualified Data.GraphViz as Graph
6162
import Data.List
62-
( intercalate
63+
( sort
6364
)
6465
import Data.List.NonEmpty
6566
( NonEmpty (..)
@@ -400,28 +401,20 @@ helpText =
400401
"Available commands in the Kore REPL: \n\
401402
\help shows this help message\n\
402403
\claim [n|<name>] shows the nth claim, the claim with\
403-
\ <name> or if used without args\
404-
\ shows the currently focused claim\
405-
\ in the form: LHS => (modality) RHS \n\
404+
\ <name> or (default) the currently\
405+
\ focused claim\n\
406406
\axiom <n|name> shows the nth axiom or the axiom\
407407
\ with <name>\n\
408408
\prove <n|name> initializes proof mode for the nth\
409409
\ claim or for the claim with <name>\n\
410-
\graph [view] [file] [format] shows the current proof graph (*)(**);\
411-
\ optional view argument can be either\
412-
\ 'expanded' or 'collapsed'; default is collapsed\n\
413-
\ (saves image in [format] if file\
414-
\ argument is given; default is .svg\
415-
\ in order to support large graphs;\n\
416-
\ file extension is added automatically);\
417-
\ accepted formats: svg, jpeg, png, pdf;\n\
410+
\graph [view] [file] [format] shows the current proof graph (*),\
411+
\ 'expanded' or 'collapsed';\
412+
\ or saves it as jpeg, png, pdf or svg\n\
418413
\step [n] attempts to run 'n' proof steps at\
419414
\ the current node (n=1 by default)\n\
420-
\stepf [n] attempts to run 'n' proof steps at\
421-
\ the current node, stepping through\
422-
\ branchings (n=1 by default);\n\
423-
\ current node is advanced to the first\
424-
\ interesting branching node (***)\n\
415+
\stepf [n] like step, but goes through\
416+
\ branchings to the first\
417+
\ interesting branching node (**)\n\
425418
\select <n> select node id 'n' from the graph\n\
426419
\config [n] shows the config for node 'n'\
427420
\ (defaults to current node)\n\
@@ -446,94 +439,78 @@ helpText =
446439
\label <-l> remove a label\n\
447440
\try (<a|c><num>)|<name> attempts <a>xiom or <c>laim at\
448441
\ index <num> or rule with <name>\n\
449-
\tryf (<a|c><num>)|<name> attempts <a>xiom or <c>laim at\
450-
\ index <num> or rule with <name>,\
451-
\ and if successful, it will apply it.\n\
442+
\tryf (<a|c><num>)|<name> like try, but if successful, it will apply the axiom or claim.\n\
452443
\clear [n] removes all the node's children from the\
453-
\ proof graph (****)\n\
454-
\ (defaults to current node)\n\
444+
\ proof graph (***)\
445+
\ (defaults to current node)\n\
455446
\save-session file saves the current session to file\n\
456-
\save-partial-proof [n] file creates a file, <file>.kore, containing a kore module\
457-
\ with the name uppercase(<file>)-SPEC, a new claim\n\
458-
\ with the current config (or config <n>) as its LHS\
459-
\ and all other claims (including the original claim)\
460-
\ marked as trusted\n\
447+
\save-partial-proof [n] file writes a new claim with the\
448+
\ config 'n' as its LHS and all\
449+
\ other claims marked as trusted\n\
461450
\alias <name> = <command> adds as an alias for <command>\n\
462451
\<alias> runs an existing alias\n\
463452
\load file loads the file as a repl script\n\
464453
\proof-status shows status for each claim\n\
465-
\log <severity> \"[\"<entry>\"]\" <type> configures the logging output\n\
466-
\ <switch-timestamp> <severity> can be debug, info,\
467-
\ warning, error, or critical;\
468-
\ is optional and defaults to warning\n\
469-
\ [<entry>] is the list of entries\
470-
\ separated by white spaces or\
471-
\ commas, e.g. '[entry1, entry2]';\n\
472-
\ these entries are used for filtering\
473-
\ the logged information, for example,\
474-
\ '[]' will log all entries with <severity>;\n\
475-
\ '[entry1, entry2]' will only log entries of\
476-
\ types entry1 or entry2 as well as entries of\
477-
\ severity <severity>.\n\
478-
\ See available entry types below.\n\
479-
\ <type> can be 'stderr' or 'file filename'\n\
480-
\ <switch-timestamp> can be enable-log-timestamps\
481-
\ or disable-log-timestamps\n\
482-
\debug-[type]-equation [eqId1] [eqId2] .. show debugging information for multiple specific equations;\
483-
\ [type] can be 'attempt' or 'apply', or nothing\
484-
\ meaning both, as follows ('debug-equation');\n\
485-
\ example usage: 'debug-attempt-equation eqId',\
486-
\ 'debug-equation eqId1 eqId2'; without arguments it will\
487-
\ will disable showing the info, for example: 'debug-apply-equation';\n\
488-
\ repl command counterparts of the equation command line options;\
489-
\ see command line help text for more information;\n\
454+
\log [<severity>] \"[\"<entry>\"]\" configures logging; <severity> can be debug ... error; [<entry>] is a list formed by types below;\n\
455+
\ <type> <switch-timestamp> <type> can be stderr or 'file filename'; <switch-timestamp> can be (enable|disable)-log-timestamps;\n\
456+
\debug[-type-]equation [eqId1] [eqId2] .. show debugging information for specific equations;\
457+
\ [-type-] can be '-attempt-', '-apply-' or '-',\n\
490458
\exit exits the repl\
491459
\\n\n\
492460
\Available modifiers:\n\
493461
\<command> > file prints the output of 'command'\
494462
\ to file\n\
495463
\<command> >> file appends the output of 'command'\
496464
\ to file\n\
497-
\<command> | external script pipes command to external script\
465+
\<command> | external_script pipes command to external script\
498466
\ and prints the result in the\
499-
\ repl\n\
500-
\<command> | external script > file pipes and then redirects the output\
501-
\ of the piped command to a file\n\
502-
\<command> | external script >> file pipes and then appends the output\
503-
\ of the piped command to a file\n\
467+
\ repl; can be redirected using > or >>\n\
504468
\\n\
505-
\(*) If an edge is labeled as Simpl/RD it means that either the target node\n\
506-
\ was reached using the SMT solver or it was reached through the Remove \n\
507-
\ Destination step.\n\
508-
\(**) A green node represents the proof has completed on\
469+
\Rule names can be added in two ways:\n\
470+
\ a) rule <k> ... </k> [label(myName)]\n\
471+
\ - can be used as-is\n\
472+
\ - ! do not add names which match the indexing syntax for the try command\n\
473+
\ b) rule [myName] : <k> ... </k>\n\
474+
\ - need to be prefixed with the module name, e.g. IMP.myName\n\
475+
\\nAvailable entry types:\n"
476+
<> entriesForHelp
477+
<>
478+
"\n\
479+
\(*) If an edge is labeled as Simpl/RD it means that the target node\n\
480+
\ was reached using either the SMT solver or the Remove Destination step.\n\
481+
\ A green node represents the proof has completed on\
509482
\ that respective branch. \n\
510-
\ A red node represents a stuck configuration.\n\
511-
\(***) An interesting branching node has at least two children which\n\
483+
\ A red node represents a stuck configuration.\n\
484+
\(**) An interesting branching node has at least two children which\n\
512485
\ contain non-bottom leaves in their subtrees. If no such node exists,\n\
513486
\ the current node is advanced to the (only) non-bottom leaf. If no such\n\
514487
\ leaf exists (i.e the proof is complete), the current node remains the same\n\
515488
\ and a message is emitted.\n\
516-
\ (****) The clear command doesn't allow the removal of nodes which are direct\n\
489+
\(***) The clear command doesn't allow the removal of nodes which are direct\n\
517490
\ descendants of branchings. The steps which create branchings cannot be\n\
518-
\ partially redone. Therefore, if this were allowed it would result in invalid proofs.\n\
519-
\\n\n\
520-
\Rule names can be added in two ways:\n\
521-
\ a) rule <k> ... </k> [label(myName)]\n\
522-
\ b) rule [myName] : <k> ... </k>\n\
523-
\Names added via a) can be used as-is. Note that names which match the\n\
524-
\ indexing syntax for the try and tryf commands shouldn't be added\n\
525-
\ (e.g. a5 as a rule name).\n\
526-
\Names added via b) need to be prefixed with the module name followed by\n\
527-
\ dot, e.g. IMP.myName\n\
528-
\Available entry types:\n "
529-
<> intercalate "\n " Log.getEntryTypesAsText
530-
<> "\n\n\
531-
\For logging the succesfully applied equations, attempted equations, or both,\n\
532-
\launch kore-repl with the appropriate flags:\n\
533-
\--debug-apply-equation EQUATION_IDENTIFIER\n\
534-
\--debug-attempt-equation EQUATION_IDENTIFIER\n\
535-
\--debug-equation EQUATION_IDENTIFIER;\n\
536-
\For more details run: kore-repl --help\n"
491+
\ partially redone. Therefore, if this were allowed it would result in invalid proofs.\n"
492+
<> "\nFor more details see https://github.com/kframework/kore/wiki/Kore-REPL#available-commands-in-the-kore-repl\n"
493+
494+
495+
entriesForHelp :: String
496+
entriesForHelp =
497+
zipWith3
498+
(\e1 e2 e3 -> align e1 <> align e2 <> align e3)
499+
column1
500+
column2
501+
column3
502+
& unlines
503+
where
504+
entries :: [String]
505+
entries =
506+
Log.entryTypeReps
507+
& fmap show
508+
& sort
509+
& (<> ["", ""])
510+
align entry = entry <> replicate (40 - length entry) ' '
511+
columnLength = length entries `div` 3
512+
(column1And2, column3) = splitAt (2 * columnLength) entries
513+
(column1, column2) = splitAt columnLength column1And2
537514

538515
-- | Determines whether the command needs to be stored or not. Commands that
539516
-- affect the outcome of the proof are stored.

0 commit comments

Comments
 (0)