/usr/share/acl2-6.3/books/oslib/tempfile.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFSECTION OSLIB::TEMPFILE :PARENTS (OSLIB) :SHORT "Generate a suitable name for a temporary file." :LONG "<p>Signature: @(call tempfile) &rarr; @('(mv filename/nil
state)').</p>

<p>Example:</p>

@({
 (tempfile \"foo\") --> (\"/tmp/jared-31721-foo\" <state>)
})

<p>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 @(see defattach).</p>

<p>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').</p>

@(def tempfile)
@(def tempfile-fn)" (DEFMACRO OSLIB::TEMPFILE (OSLIB::BASENAME &OPTIONAL (STATE (QUOTE STATE))) (CONS (QUOTE OSLIB::TEMPFILE-FN) (CONS OSLIB::BASENAME (CONS STATE (QUOTE NIL))))) (ENCAPSULATE (((OSLIB::TEMPFILE-FN * STATE) OSLIB::=> (MV * STATE) :FORMALS (OSLIB::BASENAME STATE) :GUARD (STRINGP OSLIB::BASENAME))) (LOCAL (DEFUN OSLIB::TEMPFILE-FN (OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS STATE) (IGNORE OSLIB::BASENAME)) (MV "" STATE))) (DEFTHM OSLIB::TYPE-OF-TEMPFILE-FN (OR (STRINGP (MV-NTH 0 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE))) (NOT (MV-NTH 0 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE)))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::STATE-P1-OF-TEMPFILE-FN (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::TEMPFILE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::TEMPFILE (OSLIB::BASENAME &OPTIONAL (STATE (QUOTE STATE))) (CONS (QUOTE OSLIB::TEMPFILE-FN) (CONS OSLIB::BASENAME (CONS STATE (QUOTE NIL))))) (ENCAPSULATE (((OSLIB::TEMPFILE-FN * STATE) OSLIB::=> (MV * STATE) :FORMALS (OSLIB::BASENAME STATE) :GUARD (STRINGP OSLIB::BASENAME))) (LOCAL (DEFUN OSLIB::TEMPFILE-FN (OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS STATE) (IGNORE OSLIB::BASENAME)) (MV "" STATE))) (DEFTHM OSLIB::TYPE-OF-TEMPFILE-FN (OR (STRINGP (MV-NTH 0 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE))) (NOT (MV-NTH 0 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE)))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::STATE-P1-OF-TEMPFILE-FN (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (OSLIB::TEMPFILE-FN OSLIB::BASENAME STATE)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::TEMPFILE)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Generate a suitable name for a temporary file.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::TEMPFILE))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Signature: @(call tempfile) &rarr; @('(mv filename/nil
state)').</p>

<p>Example:</p>

@({
 (tempfile \"foo\") --> (\"/tmp/jared-31721-foo\" <state>)
})

<p>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 @(see defattach).</p>

<p>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').</p>

@(def tempfile)
@(def tempfile-fn)") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . OSLIB::TEMPFILE) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Generate a suitable name for a temporary file.") (:LONG . "<p>Signature: @(call tempfile) &rarr; @('(mv filename/nil
state)').</p>

<p>Example:</p>

@({
 (tempfile \"foo\") --> (\"/tmp/jared-31721-foo\" <state>)
})

<p>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 @(see defattach).</p>

<p>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').</p>

@(def tempfile)
@(def tempfile-fn)

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|TYPE-OF-TEMPFILE-FN|)
@(def |OSLIB|::|STATE-P1-OF-TEMPFILE-FN|)") (:FROM . "[books]/oslib/tempfile.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::TEMPFILE)))))) (VALUE-TRIPLE (QUOTE OSLIB::TEMPFILE))))) (6 RECORD-EXPANSION (DEFINE OSLIB::DEFAULT-TEMPFILE-AUX ((OSLIB::TEMPDIR STRINGP "Directory to generate the file in") (OSLIB::BASENAME STRINGP "Base name to use for the new file") STATE) :RETURNS (MV (OSLIB::TEMPFILE "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')" (OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) :RULE-CLASSES :TYPE-PRESCRIPTION) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB::TEMPFILE) :SHORT "Join together a temp directory, the user name, the PID, and the base
name to create a temporary filename." (B* (((MV OSLIB::PID STATE) (OSLIB::GETPID STATE)) ((UNLESS (NATP OSLIB::PID)) (ER OSLIB::HARD? __FUNCTION__ "getpid failed") (MV NIL STATE)) ((MV OSLIB::?ERR OSLIB::USER STATE) (GETENV$ "USER" STATE)) ((UNLESS (STRINGP OSLIB::USER)) (ER OSLIB::HARD? __FUNCTION__ "reading $USER failed") (MV NIL STATE)) (OSLIB::FILENAME (STR::CAT OSLIB::USER "-" (STR::NATSTR OSLIB::PID) "-" OSLIB::BASENAME)) (OSLIB::PATH (OSLIB::CATPATH OSLIB::TEMPDIR OSLIB::FILENAME))) (MV OSLIB::PATH STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::DEFAULT-TEMPFILE-AUX :PARENTS (OSLIB::TEMPFILE) :SHORT "Join together a temp directory, the user name, the PID, and the base
name to create a temporary filename." (DEFUND OSLIB::DEFAULT-TEMPFILE-AUX (OSLIB::TEMPDIR OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (AND (STRINGP OSLIB::TEMPDIR) (STRINGP OSLIB::BASENAME)))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::PID STATE) (OSLIB::GETPID STATE)) ((UNLESS (NATP OSLIB::PID)) (ER OSLIB::HARD? __FUNCTION__ "getpid failed") (MV NIL STATE)) ((MV OSLIB::?ERR OSLIB::USER STATE) (GETENV$ "USER" STATE)) ((UNLESS (STRINGP OSLIB::USER)) (ER OSLIB::HARD? __FUNCTION__ "reading $USER failed") (MV NIL STATE)) (OSLIB::FILENAME (STR::CAT OSLIB::USER "-" (STR::NATSTR OSLIB::PID) "-" OSLIB::BASENAME)) (OSLIB::PATH (OSLIB::CATPATH OSLIB::TEMPDIR OSLIB::FILENAME))) (MV OSLIB::PATH STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE-AUX :FN (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::TEMPDIR) (GUARD STRINGP OSLIB::TEMPDIR) (DOC . "Directory to generate the file in") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "Base name to use for the new file") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE-AUX))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPFILE-AUX (OSLIB::TEMPDIR OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (AND (STRINGP OSLIB::TEMPDIR) (STRINGP OSLIB::BASENAME)))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::PID STATE) (OSLIB::GETPID STATE)) ((UNLESS (NATP OSLIB::PID)) (ER OSLIB::HARD? __FUNCTION__ "getpid failed") (MV NIL STATE)) ((MV OSLIB::?ERR OSLIB::USER STATE) (GETENV$ "USER" STATE)) ((UNLESS (STRINGP OSLIB::USER)) (ER OSLIB::HARD? __FUNCTION__ "reading $USER failed") (MV NIL STATE)) (OSLIB::FILENAME (STR::CAT OSLIB::USER "-" (STR::NATSTR OSLIB::PID) "-" OSLIB::BASENAME)) (OSLIB::PATH (OSLIB::CATPATH OSLIB::TEMPDIR OSLIB::FILENAME))) (MV OSLIB::PATH STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE-AUX :FN (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::TEMPDIR) (GUARD STRINGP OSLIB::TEMPDIR) (DOC . "Directory to generate the file in") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "Base name to use for the new file") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE-AUX))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPFILE-AUX (OSLIB::TEMPDIR OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (AND (STRINGP OSLIB::TEMPDIR) (STRINGP OSLIB::BASENAME)))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::PID STATE) (OSLIB::GETPID STATE)) ((UNLESS (NATP OSLIB::PID)) (ER OSLIB::HARD? __FUNCTION__ "getpid failed") (MV NIL STATE)) ((MV OSLIB::?ERR OSLIB::USER STATE) (GETENV$ "USER" STATE)) ((UNLESS (STRINGP OSLIB::USER)) (ER OSLIB::HARD? __FUNCTION__ "reading $USER failed") (MV NIL STATE)) (OSLIB::FILENAME (STR::CAT OSLIB::USER "-" (STR::NATSTR OSLIB::PID) "-" OSLIB::BASENAME)) (OSLIB::PATH (OSLIB::CATPATH OSLIB::TEMPDIR OSLIB::FILENAME))) (MV OSLIB::PATH STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE-AUX :FN (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::TEMPDIR) (GUARD STRINGP OSLIB::TEMPDIR) (DOC . "Directory to generate the file in") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "Base name to use for the new file") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE-AUX))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPFILE-AUX.TEMPFILE (B* (((MV OSLIB::?TEMPFILE ?STATE) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::TEMPDIR OSLIB::BASENAME STATE))) (OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPFILE-AUX.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?TEMPFILE ?STATE) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::TEMPDIR OSLIB::BASENAME STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX)) (XDOC::PARENTS (QUOTE (OSLIB::TEMPFILE))) (XDOC::SHORT (QUOTE "Join together a temp directory, the user name, the PID, and the base
name to create a temporary filename.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . OSLIB::DEFAULT-TEMPFILE-AUX) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB::TEMPFILE) (:SHORT . "Join together a temp directory, the user name, the PID, and the base
name to create a temporary filename.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|DEFAULT-TEMPFILE-AUX|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPFILE-AUX.TEMPFILE|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPFILE-AUX.STATE|)") (:FROM . "[books]/oslib/tempfile.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::DEFAULT-TEMPFILE-AUX)))))) (VALUE-TRIPLE (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::TEMPDIR) (GUARD STRINGP OSLIB::TEMPDIR) (DOC . "Directory to generate the file in") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "Base name to use for the new file") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME')") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE OSLIB::DEFAULT-TEMPFILE-AUX)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(default-tempfile-aux tempdir basename state)
  &rarr;
(mv tempfile state)</code></dt><dt>Arguments</dt><dd><tt>tempdir</tt> &mdash; Directory to generate the file in.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp tempdir)').</color></dd>
<dd><tt>basename</tt> &mdash; Base name to use for the new file.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp basename)').</color></dd>
<dt>Returns</dt><dd><tt>tempfile</tt> &mdash; Somethign like @('$TEMPDIR/$USER-$PID-$BASENAME').<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(or (stringp tempfile) (not tempfile))').</color></dd>
<dd><tt>state</tt> &mdash; <color rgb='#606060'>Type @('(state-p1 state)'), given @('(force (state-p1 state))').</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (7 RECORD-EXPANSION (DEFINE OSLIB::DEFAULT-TEMPDIR (STATE) :RETURNS (MV (OSLIB::TEMPDIR "Directory to use for temporary files." STRINGP :RULE-CLASSES :TYPE-PRESCRIPTION) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB::TEMPFILE) :SHORT "Figure out what directory to use for temporary files." :LONG "<p>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').</p>" (B* (((MV OSLIB::?ERR OSLIB::TEMPDIR STATE) (GETENV$ "TMPDIR" STATE)) ((MV OSLIB::?ERR OSLIB::TEMP STATE) (GETENV$ "TEMP" STATE))) (MV (OR (AND (STRINGP OSLIB::TEMPDIR) OSLIB::TEMPDIR) (AND (STRINGP OSLIB::TEMP) OSLIB::TEMP) "/tmp") STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::DEFAULT-TEMPDIR :PARENTS (OSLIB::TEMPFILE) :SHORT "Figure out what directory to use for temporary files." :LONG "<p>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').</p>" (DEFUND OSLIB::DEFAULT-TEMPDIR (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::?ERR OSLIB::TEMPDIR STATE) (GETENV$ "TMPDIR" STATE)) ((MV OSLIB::?ERR OSLIB::TEMP STATE) (GETENV$ "TEMP" STATE))) (MV (OR (AND (STRINGP OSLIB::TEMPDIR) OSLIB::TEMPDIR) (AND (STRINGP OSLIB::TEMP) OSLIB::TEMP) "/tmp") STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPDIR :FN (QUOTE OSLIB::DEFAULT-TEMPDIR) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPDIR) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPDIR) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPDIR)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPDIR (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::?ERR OSLIB::TEMPDIR STATE) (GETENV$ "TMPDIR" STATE)) ((MV OSLIB::?ERR OSLIB::TEMP STATE) (GETENV$ "TEMP" STATE))) (MV (OR (AND (STRINGP OSLIB::TEMPDIR) OSLIB::TEMPDIR) (AND (STRINGP OSLIB::TEMP) OSLIB::TEMP) "/tmp") STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPDIR :FN (QUOTE OSLIB::DEFAULT-TEMPDIR) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPDIR) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPDIR) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPDIR (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::?ERR OSLIB::TEMPDIR STATE) (GETENV$ "TMPDIR" STATE)) ((MV OSLIB::?ERR OSLIB::TEMP STATE) (GETENV$ "TEMP" STATE))) (MV (OR (AND (STRINGP OSLIB::TEMPDIR) OSLIB::TEMPDIR) (AND (STRINGP OSLIB::TEMP) OSLIB::TEMP) "/tmp") STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPDIR :FN (QUOTE OSLIB::DEFAULT-TEMPDIR) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPDIR) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPDIR) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPDIR.TEMPDIR (B* (((MV OSLIB::?TEMPDIR ?STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (STRINGP OSLIB::TEMPDIR)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPDIR.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?TEMPDIR ?STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::DEFAULT-TEMPDIR)) (XDOC::PARENTS (QUOTE (OSLIB::TEMPFILE))) (XDOC::SHORT (QUOTE "Figure out what directory to use for temporary files.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPDIR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>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').</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . OSLIB::DEFAULT-TEMPDIR) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB::TEMPFILE) (:SHORT . "Figure out what directory to use for temporary files.") (:LONG . "<p>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').</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|DEFAULT-TEMPDIR|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPDIR.TEMPDIR|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPDIR.STATE|)") (:FROM . "[books]/oslib/tempfile.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::DEFAULT-TEMPDIR)))))) (VALUE-TRIPLE (QUOTE OSLIB::DEFAULT-TEMPDIR))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPDIR)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPDIR) (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPDIR) (DOC . "Directory to use for temporary files.") (CUTIL::RETURN-TYPE STRINGP OSLIB::TEMPDIR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE OSLIB::DEFAULT-TEMPDIR) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE OSLIB::DEFAULT-TEMPDIR)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(default-tempdir state) &rarr; (mv tempdir state)</code></dt><dt>Returns</dt><dd><tt>tempdir</tt> &mdash; Directory to use for temporary files.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(stringp tempdir)').</color></dd>
<dd><tt>state</tt> &mdash; <color rgb='#606060'>Type @('(state-p1 state)'), given @('(force (state-p1 state))').</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (8 RECORD-EXPANSION (DEFINE OSLIB::DEFAULT-TEMPFILE ((OSLIB::BASENAME STRINGP) STATE) :RETURNS (MV (OSLIB::TEMPFILE (OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) :RULE-CLASSES :TYPE-PRESCRIPTION) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB::TEMPFILE) :SHORT "Default way to generate temporary file names." (B* (((MV OSLIB::DIR STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::DIR OSLIB::BASENAME STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::DEFAULT-TEMPFILE :PARENTS (OSLIB::TEMPFILE) :SHORT "Default way to generate temporary file names." (DEFUND OSLIB::DEFAULT-TEMPFILE (OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::BASENAME))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::DIR STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::DIR OSLIB::BASENAME STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE :FN (QUOTE OSLIB::DEFAULT-TEMPFILE) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPFILE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPFILE (OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::BASENAME))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::DIR STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::DIR OSLIB::BASENAME STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE :FN (QUOTE OSLIB::DEFAULT-TEMPFILE) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::DEFAULT-TEMPFILE (OSLIB::BASENAME STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::BASENAME))) (LET ((__FUNCTION__ (QUOTE OSLIB::DEFAULT-TEMPFILE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::DIR STATE) (OSLIB::DEFAULT-TEMPDIR STATE))) (OSLIB::DEFAULT-TEMPFILE-AUX OSLIB::DIR OSLIB::BASENAME STATE)))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DEFAULT-TEMPFILE :FN (QUOTE OSLIB::DEFAULT-TEMPFILE) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::DEFAULT-TEMPFILE) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DEFAULT-TEMPFILE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DEFAULT-TEMPFILE) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPFILE.TEMPFILE (B* (((MV OSLIB::?TEMPFILE ?STATE) (OSLIB::DEFAULT-TEMPFILE OSLIB::BASENAME STATE))) (OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-DEFAULT-TEMPFILE.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?TEMPFILE ?STATE) (OSLIB::DEFAULT-TEMPFILE OSLIB::BASENAME STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::DEFAULT-TEMPFILE)) (XDOC::PARENTS (QUOTE (OSLIB::TEMPFILE))) (XDOC::SHORT (QUOTE "Default way to generate temporary file names.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DEFAULT-TEMPFILE))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . OSLIB::DEFAULT-TEMPFILE) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB::TEMPFILE) (:SHORT . "Default way to generate temporary file names.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|DEFAULT-TEMPFILE|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPFILE.TEMPFILE|)
@(def |OSLIB|::|RETURN-TYPE-OF-DEFAULT-TEMPFILE.STATE|)") (:FROM . "[books]/oslib/tempfile.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::DEFAULT-TEMPFILE)))))) (VALUE-TRIPLE (QUOTE OSLIB::DEFAULT-TEMPFILE))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPFILE)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::DEFAULT-TEMPFILE) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::BASENAME) (GUARD STRINGP OSLIB::BASENAME) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::TEMPFILE) (DOC . "") (CUTIL::RETURN-TYPE OR (STRINGP OSLIB::TEMPFILE) (NOT OSLIB::TEMPFILE)) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . STATE) (DOC . "") (CUTIL::RETURN-TYPE STATE-P1 STATE) (CUTIL::HYP FORCE (STATE-P1 STATE)) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE OSLIB::DEFAULT-TEMPFILE) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE OSLIB::DEFAULT-TEMPFILE)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(default-tempfile basename state) &rarr; (mv tempfile state)</code></dt><dt>Arguments</dt><dd><tt>basename</tt> &mdash; <color rgb='#606060'>Guard @('(stringp basename)').</color></dd>
<dt>Returns</dt><dd><tt>tempfile</tt> &mdash; <color rgb='#606060'>Type @('(or (stringp tempfile) (not tempfile))').</color></dd>
<dd><tt>state</tt> &mdash; <color rgb='#606060'>Type @('(state-p1 state)'), given @('(force (state-p1 state))').</color></dd>
</dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))))
(("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/oslib/tempfile.lisp" "tempfile" "tempfile" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:OSLIB "/usr/share/acl2-6.3/books/oslib/getpid.lisp"))) . 1899850051) ("/usr/share/acl2-6.3/books/str/natstr.lisp" "str/natstr" "natstr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1696407817) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 248299501)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915259697)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 732116275)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105657945)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 864029516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 750113408)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1374753694)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122664565)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013733040)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061645425)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619080936)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 972646001)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 384804126)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1113724693)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 483566967)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 457663279)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134470975)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 784695287)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2126151702)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653127144)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1661395704)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1273493319)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 508744284)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061889192)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153949377)) ("/usr/share/acl2-6.3/books/str/digitp.lisp" "digitp" "digitp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479290421) ("/usr/share/acl2-6.3/books/oslib/catpath.lisp" "catpath" "catpath" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 153544286) ("/usr/share/acl2-6.3/books/oslib/getpid.lisp" "getpid" "getpid" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:OSLIB "/usr/share/acl2-6.3/books/oslib/getpid.lisp"))) . 710596962) ("/usr/share/acl2-6.3/books/oslib/logic-defs.lisp" "logic-defs" "logic-defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 24663906) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/string-listp.lisp" "std/typed-lists/string-listp" "string-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 988699164)) (LOCAL ("/usr/share/acl2-6.3/books/cutil/deflist.lisp" "cutil/deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857676809)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "std/osets/under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) (LOCAL ("/usr/share/acl2-6.3/books/cutil/maybe-defthm.lisp" "maybe-defthm" "maybe-defthm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 169275099)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/duplicated-members.lisp" "defsort/duplicated-members" "duplicated-members" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720301003)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/uniquep.lisp" "uniquep" "uniquep" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1350027706)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort" "defsort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 284418813)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic.lisp" "generic" "generic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 992283938)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic-impl.lisp" "generic-impl" "generic-impl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 154835353)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-lemmas.lisp" "ihs/ihs-lemmas" "ihs-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685360399)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-lemmas.lisp" "logops-lemmas" "logops-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 998280003)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-definitions.lisp" "logops-definitions" "logops-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2048680937)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/basic-definitions.lisp" "basic-definitions" "basic-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1383521171)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 603178913)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2130795727)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1617928370)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1992988803)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/utilities.lisp" "data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1536684829)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1486104990)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-doc-topic.lisp" "ihs-doc-topic" "ihs-doc-topic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 664631734)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/no-duplicatesp.lisp" "std/lists/no-duplicatesp" "no-duplicatesp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 334869696)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "std/lists/revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "std/lists/duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/top.lisp" "std/osets/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2045504100)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "std/lists/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/sort.lisp" "sort" "sort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 335087178)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/outer.lisp" "outer" "outer" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883866964)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/cardinality.lisp" "cardinality" "cardinality" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 101478632)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/difference.lisp" "difference" "difference" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1211437825)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/intersect.lisp" "intersect" "intersect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 464592124)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/union.lisp" "union" "union" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 895011797)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/delete.lisp" "delete" "delete" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 929878553)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48714967)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392002111)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 537896665)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1528243117)) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order.lisp" "misc/total-order" "total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619824963)) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order-bsd.lisp" "total-order-bsd" "total-order-bsd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449327279)) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 285905462)) ("/usr/share/acl2-6.3/books/tools/include-raw.lisp" "tools/include-raw" "include-raw" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 438153625) ("/usr/share/acl2-6.3/books/cutil/define.lisp" "cutil/define" "define" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1768331178) ("/usr/share/acl2-6.3/books/str/cat.lisp" "str/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140) ("/usr/share/acl2-6.3/books/xdoc/fmt-to-str.lisp" "xdoc/fmt-to-str" "fmt-to-str" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 717243077) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "oslib/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/usr/share/acl2-6.3/books/centaur/bridge/portcullis.lisp" "centaur/bridge/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661758845) ("/usr/share/acl2-6.3/books/cutil/returnspecs.lisp" "returnspecs" "returnspecs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 722876511) ("/usr/share/acl2-6.3/books/cutil/formals.lisp" "formals" "formals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 606017704) ("/usr/share/acl2-6.3/books/cutil/da-base.lisp" "da-base" "da-base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 517345789) ("/usr/share/acl2-6.3/books/cutil/look-up.lisp" "look-up" "look-up" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1505505915) ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718) ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/oslib/read-acl2-oracle.lisp" "oslib/read-acl2-oracle" "read-acl2-oracle" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 429726279) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1434314572
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / oslib / tempfile.cert
