Merge `--help` and `--help-experimental`, remove defunct options.

Motivation

Various options for the K utilities are split into --help and --help-experimental. However, this split feels arbitrary. Several "experimental" options such as --gen-bison-parser are used very commonly. A much less commonly used, but related option --bison-lists is "non-experimental.
There are also several options that I suspect are defunct such as --documentation, --add-top-cell and --shutdown-wait-time.
Proposed changes

Merge --help and --help-experimental
Remove (or hide) defunct options
Separate remaining options into sections
This is one possible implementation for kompile.
  Core Options:

    --backend
      Choose a backend. <backend> is one of [llvm|haskell|kore|java|ocaml]. 
      Each creates the kompiled K definition.
      Default: llvm
    --directory, -d
      Path to the directory in which the output resides. An output can be 
      either a kompiled K definition or a document which depends on the type 
      of backend. The default is the directory containing the main definition 
      file. 
    --md-selector
      Preprocessor: for .md files, select only the md code blocks that match 
      the selector expression. Ex:'k&(!a|b)'.
      Default: k
    --main-module
      Specify main module in which a program starts to execute. This 
      information is used by 'krun'. The default is the name of the given K 
      definition file without the extension (.k).
    --syntax-module
      Specify main module for syntax. This information is used by 'krun'. 
      (Default: <main-module>-SYNTAX).
    --help, -h
      Print this help message

  Warnings & Debugging:

    --check-races
      Checks for races among regular rules.
      Default: false
    --coverage
      Generate coverage data when executing semantics.
      Default: false
    --debug
      Print debugging output messages and error stack traces
      Default: false
    --debug-warnings
      Print debugging output messages and error/warning stack traces
      Default: false
    --profile-rule-parsing
      Generate time in seconds to parse each rule in the semantics. Found in 
      -kompiled directory under timing.log.
      Default: false

    -W
      Enable specific warning categories. Values: [non-exhaustive-match|undeleted-temp-dir|missing-hook-ocaml|missing-hook-java|missing-syntax-module|invalid-exit-code|deprecated-backend|invalid-config-var|future-error|unused-var|proof-lint|useless-rule|unresolved-function-symbol|malformed-markdown|invalidated-cache|unused-symbol]
      Default: []
    -Wno
      Disable specific warning categories.
      Default: []
    --warnings, -w
      Warning level. Values: [all|normal|none]
      Default: NORMAL
      Possible Values: [ALL, NORMAL, NONE]
    --warnings-to-errors, -w2e
      Convert warnings to errors.
      Default: false
    -E
      Perform outer parsing and then stop and pretty print the definition to 
      standard output. Useful for converting a K definition into a completely 
      self-contained file when reporting a bug.
      Default: false

    --verbose, -v
      Print verbose output messages
      Default: false
    --version
      Print version information
      Default: false

  SMT Options (Java & Haskell backends):

    --ignore-missing-smtlib-warning
      Suppress warning when SMTLib translation fails.
      Default: false
    --smt
      SMT solver to use for checking constraints. <solver> is one of 
      [z3|none]. 
      Default: Z3
      Possible Values: [NONE, Z3]
    --smt-prelude, --smt_prelude
      Path to the SMT prelude file.
    --z3-cnstr-timeout
      The default soft timeout (in milli seconds) of Z3 for checking 
      constraint satisfiability.
      Default: 50
    --z3-impl-timeout
      The default soft timeout (in milli seconds) of Z3 for checking 
      implication. 
      Default: 5000
    --z3-jni
      Invokes Z3 as JNI library. Default is external process. JNI is slightly 
      faster, but can potentially lead to JVM crash.
      Default: false
    --z3-tactic
      The solver tactic to use to check satisfiability in Z3.

  Parser Configuration:

    --bison-lists
      Make List and NeList left associative. This is useful for creating Bison 
      parsers that use bounded stack space.
      Default: false
    --bison-file
      C file containing functions to link into bison parser.
    --bison-stack-max-depth
      Maximum size of bison parsing stack (default: 10000).
      Default: 10000
    --gen-bison-parser
      Emit bison parser for the PGM configuration variable within the syntax 
      module of your definition into the kompiled definition.
      Default: false
    --gen-glr-bison-parser
      Emit GLR bison parser for the PGM configuration variable within the 
      syntax module of your definition into the kompiled definition.
      Default: false

  LLVM backend options:

    -I
      Add a directory to the search path for requires statements.
      Default: []
    -O1
      Optimize in ways that improve performance and code size, but interfere 
      with debugging and increase compilation time slightly.
      Default: false
    -O2
      Optimize further in ways that improve performance and code size, but 
      interfere with debugging more and increase compilation time somewhat.
      Default: false
    -O3
      Optimize aggressively in ways that significantly improve performance, 
      but interfere with debugging significantly and also increase compilation 
      time and code size substantially.
      Default: false
    -Og
      Optimize as much as possible without interfering with debugging 
      experience. 
      Default: false
    -ccopt
      Add a command line option to the compiler invocation for the llvm 
      backend. 
      Default: []
    --no-llvm-kompile
      Do not invoke llvm-kompile. Useful if you want to do it yourself when 
      building with the LLVM backend.
      Default: false
    --iterated
      Generate iterated pattern matching optimization; time-consuming but 
      significantly reduces matching time.
      Default: false
    --iterated-threshold
      Threshold heuristic to use when choosing which axioms to optimize. A 
      value of 0 turns the optimization off; a value of 1 turns the 
      optimization on for every axiom. Values in between (expressed as a 
      fraction of two integers, e.g. 1/2), control the aggressiveness of the 
      optimization. Higher values increase compilation times extremely, but 
      also increase the effectiveness of the optimization. Consider decreasing 
      this threshold if compilation is too slow.
      Default: 1/2

  Java backend options:

    --transition
      <string> is a whitespace-separated list of tags designating rules to 
      become transitions.
      Default: [transition]
    --add-top-cell
      Add a top cell to configuration and all rules.
      Default: false
    --legacy-kast
      Compile with settings based on the old KAST structure
      Default: false
    --maps-as-int-array
      Abstracts map values as an array of ints.
      Default: false
    --step
      Name of the compilation phase after which the compilation process should 
      stop. 

  OCaml backend options (not supported):

    --heuristic
      A string of single characters representing a sequence of heuristics to 
      use during pattern matching compilation. Valid choices are f, d, b, a, 
      l, r, n, p, q, _, N, L, R.
      Default: qbaL
    --hook-namespaces
      <string> is a whitespace-separated list of namespaces to include in the 
      hooks defined in the definition
      Default: []
    --no-link-prelude
      Do not link interpreter binaries against constants.cmx, prelude.cmx, 
      plugin.cmx, lexer.cmx, parser.cmx, hooks.cmx and run.cmx. Do not use 
      this if you don't know what you're doing.
      Default: false
    --non-strict
      Do not add runtime sort checks for every variable's inferred sort. Only 
      has an effect with `--backend ocaml`.
      Default: false
    --ocaml-dump-exit-code
      Exit code which should trigger a dump of the configuration when using 
      --ocaml-compile. 
    --ocaml-serialize-config
      <string> is a whitespace-separated list of configuration variables to 
      precompute the value of
      Default: []
    --packages
      <string> is a whitespace-separated list of ocamlfind packages to be 
      included in the compilation of the definition
      Default: []
    --reverse-rules
      Reverse the order of rules as much as possible in order to find most 
      nondeterminism without searching.
      Default: false
    --gen-ml-only
      Do not compile definition; only generate .ml files.
      Default: false

  Other Tweaks:

    --no-exc-wrap
      Do not wrap exception messages to 80 chars. Keep long lines.
      Default: false
    --no-expand-macros
      Do not expand macros on initial configurations at runtime. Will likely 
      cause incorrect behavior if any macros are used in this term.
      Default: false
    --no-prelude
      Do not implicitly require prelude.md.
      Default: false
    --opaque-klabels
      Declare all the klabels declared by the following secondary definition.
    --shutdown-wait-time
      If option is set, a shutdown hook will be registered that, once invoked, 
      interrupts the main thread and waits its termination. The wait time is 
      the argument of this option, in format like 10ms/10s/10m/10h. Useful if 
      K is interrupted by Ctrl+C, because it allows the backend to detect 
      interruption and print diagnostics information. Currently interruption 
      detection is implemented in Java Backend. If K is invoked from KServer 
      (e.g. Nailgun), the option is ignored.
    --timeout
      If option is set, timeout for this process, in format like 
      10ms/10s/10m/10h. Using this option is preferred compared to bash 
      timeout command, which has known limitations when invoked from scripts.
    --cache-file
      Location of parse cache file. Default is $KOMPILED_DIR/cache.bin.
    --emit-json
      Emit JSON serialized version of parsed and kompiled definitions.
      Default: false
    --floats-as-po
      Abstracts floating-point values as a partial order relation.
      Default: false
    --heat-cool-by-strategies
      Control heating and cooling using strategies.
      Default: false
    --k-cells
      Cells which contain komputations.
      Default: [k]
Documentation

None
Potential Alternatives/Work-arounds

Status quo
Testing Approach
