Determine which descriptions we still need to load.
(vl-descriptions-left-to-load st) → names
For loading to be completely done, we want to have:
This function computes the names of descriptions that we want for the above reasons, but which we do not yet have loaded. These are the descriptions we'll need to search for.
(defun vl-descriptions-left-to-load (st) (declare (xargs :guard (vl-loadstate-p st))) (let ((__function__ 'vl-descriptions-left-to-load)) (declare (ignorable __function__)) (b* (((vl-loadstate st) st) ((vl-loadconfig config) st.config) (current-mods (vl-collect-modules-from-descriptions st.descs)) (things-we-want-loaded (mergesort (append config.start-names (vl-modulelist-everinstanced current-mods)))) (things-we-have-loaded (mergesort (vl-descriptionlist->names st.descs)))) (difference things-we-want-loaded things-we-have-loaded))))
(defthm string-listp-of-vl-descriptions-left-to-load (b* ((names (vl-descriptions-left-to-load st))) (string-listp names)) :rule-classes :rewrite)