Attempt to find and load any missing modules.
After some initial files have been loaded, it is generally necessary to track down and load, e.g., any submodules that have been referenced but not defined. We call this process "flushing out" the description list.
To find some description
We try to load the first such
Flushing out the descriptions is necessarily an iterative process.
After we load some library module
(defun vl-flush-out-descriptions (st n state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (vl-loadstate-p st) (natp n)))) (let ((__function__ 'vl-flush-out-descriptions)) (declare (ignorable __function__)) (b* ((st (vl-loadstate-fix st)) (missing (vl-descriptions-left-to-load st)) ((unless missing) (mv st state)) ((when (zp n)) (mv (vl-loadstate-warn :type :vl-flush-failed :msg "Failed to load description~s0 ~&1 ~ because we reached the maximum number of ~ tries." :args (list (if (vl-plural-p missing) "s" "") missing)) state)) (num-prev (len (vl-loadstate->descs st))) ((mv st state) (vl-load-descriptions missing st state)) (num-new (len (vl-loadstate->descs st))) ((when (equal num-prev num-new)) (mv (vl-loadstate-warn :type :vl-search-failed :msg "Failed to find ~x0 description~s1: ~&2." :args (list (length missing) (if (vl-plural-p missing) "s" "") (mergesort missing))) state))) (vl-flush-out-descriptions st (- n 1) state))))
(defthm vl-loadstate-p-of-vl-flush-out-descriptions.st (b* (((mv ?st acl2::?state) (vl-flush-out-descriptions st n state))) (vl-loadstate-p st)) :rule-classes :rewrite)