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

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