		Search-engine friendly clone of the ACL2 documentation.

Tempfile

Default-tempdir

Figure out what directory to use for temporary files.

Signature
(default-tempdir state) → (mv tempdir new-state)
Returns: tempdir — Directory to use for temporary files.
Type (stringp tempdir).; new-state — Type (state-p1 new-state), given (force (state-p1 state)).

We think it's conventional for Linux programs to look at the value of the TMPDIR environment variable. On Windows, apparently programs should use TEMP. If either of these is set, we try to respect the choice. Otherwise, we just default to /tmp.

Definitions and Theorems

Function: default-tempdir

(defun default-tempdir (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'default-tempdir))
    (declare (ignorable __function__))
    (b* (((mv ?err tempdir state)
          (getenv$ "TMPDIR" state))
         ((mv ?err temp state)
          (getenv$ "TEMP" state))
         (tmpdir (or (and (stringp tempdir) tempdir)
                     (and (stringp temp)
                          (pathname-to-unix temp))
                     "/tmp")))
      (mv tmpdir state))))

Theorem: stringp-of-default-tempdir.tempdir

(defthm stringp-of-default-tempdir.tempdir
  (b* (((mv ?tempdir ?new-state)
        (default-tempdir state)))
    (stringp tempdir))
  :rule-classes :type-prescription)

Theorem: state-p1-of-default-tempdir.new-state

(defthm state-p1-of-default-tempdir.new-state
  (implies (force (state-p1 state))
           (b* (((mv ?tempdir ?new-state)
                 (default-tempdir state)))
             (state-p1 new-state)))
  :rule-classes :rewrite)

Theorem: w-state-of-default-tempdir

(defthm w-state-of-default-tempdir
  (b* (((mv ?tempdir ?new-state)
        (default-tempdir state)))
    (equal (w new-state) (w state))))