		Search-engine friendly clone of the ACL2 documentation.

Vl-gather

Vl-gather-main

Signature
(vl-gather-main opts &key (state 'state)) → state
Arguments: opts — Guard (vl-gather-opts-p opts).

Definitions and Theorems

Function: vl-gather-main-fn

(defun vl-gather-main-fn (opts state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (vl-gather-opts-p opts)))
 (let ((__function__ 'vl-gather-main))
   (declare (ignorable __function__))
   (b*
    (((vl-gather-opts opts) opts)
     ((mv ?cmdline-warnings defines)
      (vl-parse-cmdline-defines
           opts.defines
           (make-vl-location :filename "vl cmdline"
                             :line 1
                             :col 0)
           t))
     (- (or (not cmdline-warnings)
            (vl-cw-ps-seq (vl-print-warnings cmdline-warnings))))
     (loadconfig (make-vl-loadconfig :edition opts.edition
                                     :strictp opts.strict
                                     :start-files opts.start-files
                                     :plusargs opts.plusargs
                                     :search-path opts.search-path
                                     :search-exts opts.search-exts
                                     :include-dirs opts.include-dirs
                                     :defines defines
                                     :filemapp t))
     ((mv result state) (vl-load loadconfig))
     ((vl-loadresult result) result)
     ((mv ?okp design)
      (vl-design-deporder-modules result.design))
     (orig (vl-design-original-source design result.filemap))
     (- (cw "Writing output file ~x0~%"
            opts.output))
     (state (with-ps-file opts.output (vl-print orig)))
     (- (cw "All done gathering files.~%")))
    state)))