• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
      • Argv
      • Copy
      • Catpath
      • Universal-time
      • Ls
      • Basename
      • Tempfile
        • Default-tempfile-aux
        • Default-tempdir
        • Default-tempfile
      • Dirname
      • Copy!
      • Mkdir
      • Ls-files
      • Lisp-version
      • Rmtree
      • Ls-subdirs
      • Lisp-type
      • Date
      • Getpid
      • Basenames
      • Dirnames
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Basename!
      • Catpaths
      • Mkdir!
      • Ls!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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.