		Search-engine friendly clone of the ACL2 documentation.

Vl-loadconfig

Vl-loadconfig-clean

Normalize a load configuration to avoid, e.g., redundant search paths and extensions.

Signature
(vl-loadconfig-clean config) → new-config
Arguments: config — Guard (vl-loadconfig-p config).
Returns: new-config — Type (vl-loadconfig-p new-config).

We clean up the load configuration in a couple of ways. This is partially an optimization that will help us to avoid looking in the same directories multiple times. It also helps to prevent spurious "ambiguous load" warnings that could arise if someone gives the same search extensions multiple times.

Definitions and Theorems

Function: vl-loadconfig-clean

(defun vl-loadconfig-clean (config)
 (declare (xargs :guard (vl-loadconfig-p config)))
 (let ((__function__ 'vl-loadconfig-clean))
  (declare (ignorable __function__))
  (b* (((vl-loadconfig config)))
   (change-vl-loadconfig
     config
     :start-names (mergesort config.start-names)
     :search-path (remove-duplicates-equal config.search-path)
     :search-exts (vl-clean-search-extensions config.search-exts)
     :include-dirs (remove-duplicates-equal config.include-dirs)))))

Theorem: vl-loadconfig-p-of-vl-loadconfig-clean

(defthm vl-loadconfig-p-of-vl-loadconfig-clean
  (b* ((new-config (vl-loadconfig-clean config)))
    (vl-loadconfig-p new-config))
  :rule-classes :rewrite)

Subtopics

Vl-clean-search-extensions-aux: (vl-clean-search-extensions-aux x) maps vl-clean-search-extension across a list.
Vl-clean-search-extension: Normalize search extensions so that they don't have leading dots.
Vl-clean-search-extensions