• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
          • Vl-lint
          • Vl-server
          • Vl-gather
          • Vl-zip
          • Vl-main
            • Vl-toolkit-other-command
            • Vl-help
              • Vl-toolkit-help-message
          • Split-plusargs
          • Vl-shell
          • Vl-json
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Vl-main

Vl-help

Show help on how to use VL kit commands.

Signature
(vl-help args &key (state 'state)) → state
Arguments
args — Guard (string-listp args).

This just implements the vl help command.

Definitions and Theorems

Function: vl-help-fn

(defun vl-help-fn (args state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (string-listp args)))
       (let ((__function__ 'vl-help))
            (declare (ignorable __function__))
            (b* (((unless (or (atom args) (atom (cdr args))))
                  (die "Usage: vl help <command>~%")
                  state)
                 (command (if (atom args) "help" (car args)))
                 (help (vl-toolkit-help-message command))
                 ((unless help)
                  (die "Unknown command ~s0." command)
                  state))
                (vl-cw-ps-seq (vl-print help))
                state)))

Subtopics

Vl-toolkit-help-message
Look up the help message for a VL kit program.