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

• Vl-zip

Vl-zip-top

Top-level vl zip command.

Signature

(vl-zip-top argv &key (state 'state)) → state

Arguments

argv — Guard (string-listp argv).

Definitions and Theorems

Function: vl-zip-top-fn

(defun
     vl-zip-top-fn (argv state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (string-listp argv)))
     (let ((__function__ 'vl-zip-top))
          (declare (ignorable __function__))
          (b* (((mv errmsg opts start-files-and-plusargs)
                (parse-vl-zip-opts argv))
               ((when errmsg)
                (die "~@0~%" errmsg)
                state)
               ((mv start-files plusargs)
                (split-plusargs start-files-and-plusargs))
               (opts (change-vl-zip-opts opts
                                         :plusargs plusargs
                                         :start-files start-files))
               ((vl-zip-opts opts) opts)
               ((when opts.help)
                (vl-cw-ps-seq (vl-print *vl-zip-help*))
                (exit-ok)
                state)
               ((when opts.readme)
                (vl-cw-ps-seq (vl-print *vl-zip-readme*))
                (exit-ok)
                state)
               ((unless (consp opts.start-files))
                (die "No files to process.")
                state)
               (- (cw "VL Zip Configuration:~%"))
               (- (cw " - start files: ~x0~%"
                      opts.start-files))
               (state (must-be-regular-files! opts.start-files))
               (- (cw " - search path: ~x0~%"
                      opts.search-path))
               (state (must-be-directories! opts.search-path))
               (- (cw " - include directories: ~x0~%"
                      opts.include-dirs))
               (state (must-be-directories! opts.include-dirs))
               (- (and opts.defines
                       (cw "; defines: ~x0~%" opts.defines)))
               (- (cw " - output file: ~x0~%" opts.output))
               (- (cw "; Soft heap size ceiling: ~x0 GB~%"
                      opts.mem))
               (- (set-max-mem (* (expt 2 30) opts.mem)))
               (state (vl-zip-main opts)))
              (exit-ok)
              state)))