		Search-engine friendly clone of the ACL2 documentation.

Oslib

Tempfile

Generate a suitable name for a temporary file.

Signature: (tempfile basename &optional (state 'state)) → (mv filename/nil state).

Example:

(tempfile "foo") --> ("/tmp/jared-31721-foo" <state>)

Note: this function is attachable. If you need to generate temporary file names using some other scheme, you can define your own strategy and attach it to tempfile-fn; see defattach.

The intent is that this function should produce a good filename to use for the name of a temporary file. To allow tempfile implementations to fail for whatever reason, filename may be nil.

Macro: tempfile

(defmacro tempfile (basename &optional (state 'state))
  (cons 'tempfile-fn
        (cons basename (cons state 'nil))))

Definition: tempfile-fn

(encapsulate (((tempfile-fn * state)
               => (mv * state)
               :formals (basename state)
               :guard (stringp basename)))
  (local (value-triple :elided))
  (defthm type-of-tempfile-fn
    (or (stringp (mv-nth 0 (tempfile-fn basename state)))
        (not (mv-nth 0 (tempfile-fn basename state))))
    :rule-classes :type-prescription)
  (defthm state-p1-of-tempfile-fn
    (implies (force (state-p1 state))
             (state-p1 (mv-nth 1 (tempfile-fn basename state)))))
  (defthm w-state-of-tempfile-fn
    (equal (w (mv-nth 1 (tempfile-fn basename state)))
           (w state))))

Definitions and Theorems

Theorem: type-of-tempfile-fn

(defthm type-of-tempfile-fn
  (or (stringp (mv-nth 0 (tempfile-fn basename state)))
      (not (mv-nth 0 (tempfile-fn basename state))))
  :rule-classes :type-prescription)

Theorem: state-p1-of-tempfile-fn

(defthm state-p1-of-tempfile-fn
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1 (tempfile-fn basename state)))))

Theorem: w-state-of-tempfile-fn

(defthm w-state-of-tempfile-fn
  (equal (w (mv-nth 1 (tempfile-fn basename state)))
         (w state)))

Subtopics

Default-tempfile-aux: Join together a temp directory, the user name, the PID, and the base name to create a temporary filename.
Default-tempdir: Figure out what directory to use for temporary files.
Default-tempfile: Default way to generate temporary file names.