acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / oslib / logic-defs.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
(DEFPKG "U" (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) NIL ((:SYSTEM . "ihs/ihs-init.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp") (:SYSTEM . "defsort/generic-impl.lisp") (:SYSTEM . "defsort/generic.lisp") (:SYSTEM . "defsort/defsort.lisp") (:SYSTEM . "defsort/uniquep.lisp") (:SYSTEM . "defsort/duplicated-members.lisp") (:SYSTEM . "cutil/deflist.lisp") (:SYSTEM . "std/typed-lists/string-listp.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFINE OSLIB::ARGV (&OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (OSLIB::ARGUMENTS STRING-LISTP) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Get the \"application level\" command line arguments passed to ACL2." :LONG "<p>Typically, @('(argv)') is useful for writing command-line programs
atop ACL2, e.g., using @(see save-exec).</p>

<p>In the logic, this function reads from the ACL2 oracle and coerces
whatever it finds into a @(see string-listp).  In the execution, we use
whatever mechanism the host Lisp provides for reading the command line
arguments that were given to ACL2.</p>

<p>Dead simple, right?  Well, not really.</p>

<p>Usually ACL2 itself, or any custom program you build atop ACL2 using @(see
save-exec), is really just an <i>image</i> that is executed by the
<i>runtime</i> for the host Lisp.  For instance, when you build ACL2 on CCL,
you get:</p>

<ul>

<li>An ACL2 image named @('saved_acl2.lx86cl64') or similar</li>

<li>A script named @('saved_acl2') that is something like this:

@({
#!/bin/sh
export CCL_DEFAULT_DIRECTORY=/path/to/ccl
exec /path/to/ccl/lx86cl64 
  -I /path/to/saved_acl2.lx86cl64 
  -K ISO-8859-1 
  -e \"(acl2::acl2-default-restart)\"
  -- \"$@\"
})</li>

</ul>

<p>So this script is invoking the Lisp runtime, named @('lx86cl64'), and
telling it to execute the ACL2 image, @('saved_acl2.lx86cl64').</p>

<p>The important thing to note here is that command-line options like @('-I'),
@('-K'), and @('-e'), are arguments <b>to the runtime</b>, not to ACL2.  These
runtime options vary wildly from Lisp to Lisp.  So for @('argv') to be portable
and make any sense at all, we really want to exclude these Lisp-runtime
options, and only give you the \"real\", application-level options for this
invocation of your program.</p>

<p>Fortunately, most Lisps have a special mechanism to separate their runtime
options from the application options.  In Allegro, CCL, CLISP, and CMUCL, this
is done with a special @('--') option.  SBCL uses a slightly more elaborate
syntax but it's the same basic idea.</p>

<p>So on these Lisps, as long as you are running ACL2 or your save-image using
a \"proper\" shell script, @('(argv)') will work perfectly and give you exactly
the arguments to your program, no matter what options you are using, and no
matter whether the host Lisp runtime takes options with the same names.  For
details about what a \"proper\" script means, see the comments for your
particular Lisp in @('oslib/argv-raw.lsp').</p>

<p>Unfortunately, GCL and LispWorks do not have such an option, so on these
Lisps we do something very half-assed:</p>

<ul>
<li>We still expect that a \"proper\" shell script will put in a @('--') option
to separate the runtime options from the program options.</li>
<li>@('(argv)') just excludes will everything before the @('--').</li>
</ul>

<p>So even though the Lisp doesn't know about @('--') in this case, we can at
least keep the Lisp specific options out of your program.</p>

<p>But this isn't perfect.  Since the Lisp doesn't know to stop processing
options when it sees @('--'), there is a possibility of conflict if your
program happens to use the same options as the Lisp.  I don't know how to do
any better, so that's just how it is.</p>" (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRING-LISTP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV NIL STATE))) /// (DEFTHM OSLIB::TRUE-LISTP-OF-ARGV (TRUE-LISTP (MV-NTH 0 (OSLIB::ARGV))) :RULE-CLASSES :TYPE-PRESCRIPTION)) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::ARGV :PARENTS (OSLIB) :SHORT "Get the \"application level\" command line arguments passed to ACL2." :LONG "<p>Typically, @('(argv)') is useful for writing command-line programs
atop ACL2, e.g., using @(see save-exec).</p>

<p>In the logic, this function reads from the ACL2 oracle and coerces
whatever it finds into a @(see string-listp).  In the execution, we use
whatever mechanism the host Lisp provides for reading the command line
arguments that were given to ACL2.</p>

<p>Dead simple, right?  Well, not really.</p>

<p>Usually ACL2 itself, or any custom program you build atop ACL2 using @(see
save-exec), is really just an <i>image</i> that is executed by the
<i>runtime</i> for the host Lisp.  For instance, when you build ACL2 on CCL,
you get:</p>

<ul>

<li>An ACL2 image named @('saved_acl2.lx86cl64') or similar</li>

<li>A script named @('saved_acl2') that is something like this:

@({
#!/bin/sh
export CCL_DEFAULT_DIRECTORY=/path/to/ccl
exec /path/to/ccl/lx86cl64 
  -I /path/to/saved_acl2.lx86cl64 
  -K ISO-8859-1 
  -e \"(acl2::acl2-default-restart)\"
  -- \"$@\"
})</li>

</ul>

<p>So this script is invoking the Lisp runtime, named @('lx86cl64'), and
telling it to execute the ACL2 image, @('saved_acl2.lx86cl64').</p>

<p>The important thing to note here is that command-line options like @('-I'),
@('-K'), and @('-e'), are arguments <b>to the runtime</b>, not to ACL2.  These
runtime options vary wildly from Lisp to Lisp.  So for @('argv') to be portable
and make any sense at all, we really want to exclude these Lisp-runtime
options, and only give you the \"real\", application-level options for this
invocation of your program.</p>

<p>Fortunately, most Lisps have a special mechanism to separate their runtime
options from the application options.  In Allegro, CCL, CLISP, and CMUCL, this
is done with a special @('--') option.  SBCL uses a slightly more elaborate
syntax but it's the same basic idea.</p>

<p>So on these Lisps, as long as you are running ACL2 or your save-image using
a \"proper\" shell script, @('(argv)') will work perfectly and give you exactly
the arguments to your program, no matter what options you are using, and no
matter whether the host Lisp runtime takes options with the same names.  For
details about what a \"proper\" script means, see the comments for your
particular Lisp in @('oslib/argv-raw.lsp').</p>

<p>Unfortunately, GCL and LispWorks do not have such an option, so on these
Lisps we do something very half-assed:</p>

<ul>
<li>We still expect that a \"proper\" shell script will put in a @('--') option
to separate the runtime options from the program options.</li>
<li>@('(argv)') just excludes will everything before the @('--').</li>
</ul>

<p>So even though the Lisp doesn't know about @('--') in this case, we can at
least keep the Lisp specific options out of your program.</p>

<p>But this isn't perfect.  Since the Lisp doesn't know to stop processing
options when it sees @('--'), there is a possibility of conflict if your
program happens to use the same options as the Lisp.  I don't know how to do
any better, so that's just how it is.</p>" (DEFMACRO OSLIB::ARGV (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::ARGV-FN) STATE)) (DEFUND OSLIB::ARGV-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::ARGV))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRING-LISTP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV NIL STATE))))) (ADD-MACRO-ALIAS OSLIB::ARGV OSLIB::ARGV-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::ARGV-FN) (QUOTE OSLIB::ARGV)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::ARGV :FN (QUOTE OSLIB::ARGV-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::ARGV-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::ARGV))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::ARGV-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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)))) (DEFTHM OSLIB::TRUE-LISTP-OF-ARGV (TRUE-LISTP (MV-NTH 0 (OSLIB::ARGV))) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::ARGV)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::ARGV (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::ARGV-FN) STATE)) (DEFUND OSLIB::ARGV-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::ARGV))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRING-LISTP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV NIL STATE))))) (ADD-MACRO-ALIAS OSLIB::ARGV OSLIB::ARGV-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::ARGV-FN) (QUOTE OSLIB::ARGV)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::ARGV :FN (QUOTE OSLIB::ARGV-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::ARGV-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::ARGV))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::ARGV-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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)))) (DEFTHM OSLIB::TRUE-LISTP-OF-ARGV (TRUE-LISTP (MV-NTH 0 (OSLIB::ARGV))) :RULE-CLASSES :TYPE-PRESCRIPTION))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::ARGV (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::ARGV-FN) STATE)) (DEFUND OSLIB::ARGV-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::ARGV))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRING-LISTP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV NIL STATE))))) (ADD-MACRO-ALIAS OSLIB::ARGV OSLIB::ARGV-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::ARGV-FN) (QUOTE OSLIB::ARGV)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::ARGV :FN (QUOTE OSLIB::ARGV-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::ARGV-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::ARGV))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::ARGV-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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-ARGV-FN.ARGUMENTS (B* (((MV OSLIB::?ARGUMENTS ?STATE) (OSLIB::ARGV-FN STATE))) (STRING-LISTP OSLIB::ARGUMENTS)) :HINTS NIL :RULE-CLASSES :REWRITE) (DEFTHM OSLIB::RETURN-TYPE-OF-ARGV-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?ARGUMENTS ?STATE) (OSLIB::ARGV-FN STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE))) (DEFTHM OSLIB::TRUE-LISTP-OF-ARGV (TRUE-LISTP (MV-NTH 0 (OSLIB::ARGV))) :RULE-CLASSES :TYPE-PRESCRIPTION)))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::ARGV)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Get the \"application level\" command line arguments passed to ACL2.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::ARGV))) 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>Typically, @('(argv)') is useful for writing command-line programs
atop ACL2, e.g., using @(see save-exec).</p>

<p>In the logic, this function reads from the ACL2 oracle and coerces
whatever it finds into a @(see string-listp).  In the execution, we use
whatever mechanism the host Lisp provides for reading the command line
arguments that were given to ACL2.</p>

<p>Dead simple, right?  Well, not really.</p>

<p>Usually ACL2 itself, or any custom program you build atop ACL2 using @(see
save-exec), is really just an <i>image</i> that is executed by the
<i>runtime</i> for the host Lisp.  For instance, when you build ACL2 on CCL,
you get:</p>

<ul>

<li>An ACL2 image named @('saved_acl2.lx86cl64') or similar</li>

<li>A script named @('saved_acl2') that is something like this:

@({
#!/bin/sh
export CCL_DEFAULT_DIRECTORY=/path/to/ccl
exec /path/to/ccl/lx86cl64 
  -I /path/to/saved_acl2.lx86cl64 
  -K ISO-8859-1 
  -e \"(acl2::acl2-default-restart)\"
  -- \"$@\"
})</li>

</ul>

<p>So this script is invoking the Lisp runtime, named @('lx86cl64'), and
telling it to execute the ACL2 image, @('saved_acl2.lx86cl64').</p>

<p>The important thing to note here is that command-line options like @('-I'),
@('-K'), and @('-e'), are arguments <b>to the runtime</b>, not to ACL2.  These
runtime options vary wildly from Lisp to Lisp.  So for @('argv') to be portable
and make any sense at all, we really want to exclude these Lisp-runtime
options, and only give you the \"real\", application-level options for this
invocation of your program.</p>

<p>Fortunately, most Lisps have a special mechanism to separate their runtime
options from the application options.  In Allegro, CCL, CLISP, and CMUCL, this
is done with a special @('--') option.  SBCL uses a slightly more elaborate
syntax but it's the same basic idea.</p>

<p>So on these Lisps, as long as you are running ACL2 or your save-image using
a \"proper\" shell script, @('(argv)') will work perfectly and give you exactly
the arguments to your program, no matter what options you are using, and no
matter whether the host Lisp runtime takes options with the same names.  For
details about what a \"proper\" script means, see the comments for your
particular Lisp in @('oslib/argv-raw.lsp').</p>

<p>Unfortunately, GCL and LispWorks do not have such an option, so on these
Lisps we do something very half-assed:</p>

<ul>
<li>We still expect that a \"proper\" shell script will put in a @('--') option
to separate the runtime options from the program options.</li>
<li>@('(argv)') just excludes will everything before the @('--').</li>
</ul>

<p>So even though the Lisp doesn't know about @('--') in this case, we can at
least keep the Lisp specific options out of your program.</p>

<p>But this isn't perfect.  Since the Lisp doesn't know to stop processing
options when it sees @('--'), there is a possibility of conflict if your
program happens to use the same options as the Lisp.  I don't know how to do
any better, so that's just how it is.</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::ARGV) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Get the \"application level\" command line arguments passed to ACL2.") (:LONG . "<p>Typically, @('(argv)') is useful for writing command-line programs
atop ACL2, e.g., using @(see save-exec).</p>

<p>In the logic, this function reads from the ACL2 oracle and coerces
whatever it finds into a @(see string-listp).  In the execution, we use
whatever mechanism the host Lisp provides for reading the command line
arguments that were given to ACL2.</p>

<p>Dead simple, right?  Well, not really.</p>

<p>Usually ACL2 itself, or any custom program you build atop ACL2 using @(see
save-exec), is really just an <i>image</i> that is executed by the
<i>runtime</i> for the host Lisp.  For instance, when you build ACL2 on CCL,
you get:</p>

<ul>

<li>An ACL2 image named @('saved_acl2.lx86cl64') or similar</li>

<li>A script named @('saved_acl2') that is something like this:

@({
#!/bin/sh
export CCL_DEFAULT_DIRECTORY=/path/to/ccl
exec /path/to/ccl/lx86cl64 
  -I /path/to/saved_acl2.lx86cl64 
  -K ISO-8859-1 
  -e \"(acl2::acl2-default-restart)\"
  -- \"$@\"
})</li>

</ul>

<p>So this script is invoking the Lisp runtime, named @('lx86cl64'), and
telling it to execute the ACL2 image, @('saved_acl2.lx86cl64').</p>

<p>The important thing to note here is that command-line options like @('-I'),
@('-K'), and @('-e'), are arguments <b>to the runtime</b>, not to ACL2.  These
runtime options vary wildly from Lisp to Lisp.  So for @('argv') to be portable
and make any sense at all, we really want to exclude these Lisp-runtime
options, and only give you the \"real\", application-level options for this
invocation of your program.</p>

<p>Fortunately, most Lisps have a special mechanism to separate their runtime
options from the application options.  In Allegro, CCL, CLISP, and CMUCL, this
is done with a special @('--') option.  SBCL uses a slightly more elaborate
syntax but it's the same basic idea.</p>

<p>So on these Lisps, as long as you are running ACL2 or your save-image using
a \"proper\" shell script, @('(argv)') will work perfectly and give you exactly
the arguments to your program, no matter what options you are using, and no
matter whether the host Lisp runtime takes options with the same names.  For
details about what a \"proper\" script means, see the comments for your
particular Lisp in @('oslib/argv-raw.lsp').</p>

<p>Unfortunately, GCL and LispWorks do not have such an option, so on these
Lisps we do something very half-assed:</p>

<ul>
<li>We still expect that a \"proper\" shell script will put in a @('--') option
to separate the runtime options from the program options.</li>
<li>@('(argv)') just excludes will everything before the @('--').</li>
</ul>

<p>So even though the Lisp doesn't know about @('--') in this case, we can at
least keep the Lisp specific options out of your program.</p>

<p>But this isn't perfect.  Since the Lisp doesn't know to stop processing
options when it sees @('--'), there is a possibility of conflict if your
program happens to use the same options as the Lisp.  I don't know how to do
any better, so that's just how it is.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|ARGV-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-ARGV-FN.ARGUMENTS|)
@(def |OSLIB|::|RETURN-TYPE-OF-ARGV-FN.STATE|)
@(def |OSLIB|::|TRUE-LISTP-OF-ARGV|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::ARGV)))))) (VALUE-TRIPLE (QUOTE OSLIB::ARGV))))) (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::ARGV)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::ARGV-FN) (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::ARGUMENTS) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::ARGUMENTS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::ARGV) 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::ARGV)) 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>(argv &amp;optional (state 'state)) &rarr; (mv arguments state)</code></dt><dt>Returns</dt><dd><tt>arguments</tt> &mdash; <color rgb='#606060'>Type @('(string-listp arguments)').</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))))))))) (6 RECORD-EXPANSION (DEFINE OSLIB::DATE (&OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (OSLIB::DATESTAMP STRINGP :RULE-CLASSES :TYPE-PRESCRIPTION) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Get the current datestamp, like \"November 17, 2010 10:25:33\"." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we use Common Lisp's @('get-decoded-time') function to figure out
what the current date and time is.  We think this <i>should</i> work on any
Common Lisp system.</p>" (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRINGP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV "Error reading date." STATE)))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::DATE :PARENTS (OSLIB) :SHORT "Get the current datestamp, like \"November 17, 2010 10:25:33\"." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we use Common Lisp's @('get-decoded-time') function to figure out
what the current date and time is.  We think this <i>should</i> work on any
Common Lisp system.</p>" (DEFMACRO OSLIB::DATE (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::DATE-FN) STATE)) (DEFUND OSLIB::DATE-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DATE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRINGP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV "Error reading date." STATE))))) (ADD-MACRO-ALIAS OSLIB::DATE OSLIB::DATE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::DATE-FN) (QUOTE OSLIB::DATE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DATE :FN (QUOTE OSLIB::DATE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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::DATE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DATE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DATE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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::DATE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::DATE (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::DATE-FN) STATE)) (DEFUND OSLIB::DATE-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DATE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRINGP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV "Error reading date." STATE))))) (ADD-MACRO-ALIAS OSLIB::DATE OSLIB::DATE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::DATE-FN) (QUOTE OSLIB::DATE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DATE :FN (QUOTE OSLIB::DATE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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::DATE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DATE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DATE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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) (DEFMACRO OSLIB::DATE (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::DATE-FN) STATE)) (DEFUND OSLIB::DATE-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::DATE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE))) (IF (AND (NOT OSLIB::ERR) (STRINGP OSLIB::VAL)) (MV OSLIB::VAL STATE) (MV "Error reading date." STATE))))) (ADD-MACRO-ALIAS OSLIB::DATE OSLIB::DATE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::DATE-FN) (QUOTE OSLIB::DATE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::DATE :FN (QUOTE OSLIB::DATE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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::DATE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::DATE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::DATE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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-DATE-FN.DATESTAMP (B* (((MV OSLIB::?DATESTAMP ?STATE) (OSLIB::DATE-FN STATE))) (STRINGP OSLIB::DATESTAMP)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-DATE-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?DATESTAMP ?STATE) (OSLIB::DATE-FN STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::DATE)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Get the current datestamp, like \"November 17, 2010 10:25:33\".")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::DATE))) 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>In the logic this function reads from the ACL2 oracle.  In the
execution we use Common Lisp's @('get-decoded-time') function to figure out
what the current date and time is.  We think this <i>should</i> work on any
Common Lisp system.</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::DATE) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Get the current datestamp, like \"November 17, 2010 10:25:33\".") (:LONG . "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we use Common Lisp's @('get-decoded-time') function to figure out
what the current date and time is.  We think this <i>should</i> work on any
Common Lisp system.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|DATE-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-DATE-FN.DATESTAMP|)
@(def |OSLIB|::|RETURN-TYPE-OF-DATE-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::DATE)))))) (VALUE-TRIPLE (QUOTE OSLIB::DATE))))) (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::DATE)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::DATE-FN) (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::DATESTAMP) (DOC . "") (CUTIL::RETURN-TYPE STRINGP OSLIB::DATESTAMP) (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::DATE) 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::DATE)) 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>(date &amp;optional (state 'state)) &rarr; (mv datestamp state)</code></dt><dt>Returns</dt><dd><tt>datestamp</tt> &mdash; <color rgb='#606060'>Type @('(stringp datestamp)').</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::GETPID (&OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (OSLIB::PID "The Process ID for this ACL2 session on success, or
                     @('nil') on failure." (OR (NATP OSLIB::PID) (NOT OSLIB::PID)) :RULE-CLASSES :TYPE-PRESCRIPTION) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Get the current process identification (PID) number." :LONG "<p>This will just fail if called on an unsupported Lisp.</p>" (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV NIL STATE))) (MV (NFIX OSLIB::VAL) STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::GETPID :PARENTS (OSLIB) :SHORT "Get the current process identification (PID) number." :LONG "<p>This will just fail if called on an unsupported Lisp.</p>" (DEFMACRO OSLIB::GETPID (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::GETPID-FN) STATE)) (DEFUND OSLIB::GETPID-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::GETPID))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV NIL STATE))) (MV (NFIX OSLIB::VAL) STATE)))) (ADD-MACRO-ALIAS OSLIB::GETPID OSLIB::GETPID-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::GETPID-FN) (QUOTE OSLIB::GETPID)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::GETPID :FN (QUOTE OSLIB::GETPID-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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::GETPID-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::GETPID))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::GETPID-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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::GETPID)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::GETPID (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::GETPID-FN) STATE)) (DEFUND OSLIB::GETPID-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::GETPID))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV NIL STATE))) (MV (NFIX OSLIB::VAL) STATE)))) (ADD-MACRO-ALIAS OSLIB::GETPID OSLIB::GETPID-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::GETPID-FN) (QUOTE OSLIB::GETPID)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::GETPID :FN (QUOTE OSLIB::GETPID-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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::GETPID-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::GETPID))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::GETPID-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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) (DEFMACRO OSLIB::GETPID (&OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::GETPID-FN) STATE)) (DEFUND OSLIB::GETPID-FN (STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::GETPID))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV NIL STATE))) (MV (NFIX OSLIB::VAL) STATE)))) (ADD-MACRO-ALIAS OSLIB::GETPID OSLIB::GETPID-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::GETPID-FN) (QUOTE OSLIB::GETPID)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::GETPID :FN (QUOTE OSLIB::GETPID-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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::GETPID-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::GETPID))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::GETPID-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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-GETPID-FN.PID (B* (((MV OSLIB::?PID ?STATE) (OSLIB::GETPID-FN STATE))) (OR (NATP OSLIB::PID) (NOT OSLIB::PID))) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-GETPID-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?PID ?STATE) (OSLIB::GETPID-FN STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::GETPID)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Get the current process identification (PID) number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::GETPID))) 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>This will just fail if called on an unsupported Lisp.</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::GETPID) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Get the current process identification (PID) number.") (:LONG . "<p>This will just fail if called on an unsupported Lisp.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|GETPID-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-GETPID-FN.PID|)
@(def |OSLIB|::|RETURN-TYPE-OF-GETPID-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::GETPID)))))) (VALUE-TRIPLE (QUOTE OSLIB::GETPID))))) (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::GETPID)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::GETPID-FN) (QUOTE ((:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::PID) (DOC . "The Process ID for this ACL2 session on success, or
                     @('nil') on failure.") (CUTIL::RETURN-TYPE OR (NATP OSLIB::PID) (NOT OSLIB::PID)) (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::GETPID) 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::GETPID)) 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>(getpid &amp;optional (state 'state)) &rarr; (mv pid state)</code></dt><dt>Returns</dt><dd><tt>pid</tt> &mdash; The Process ID for this ACL2 session on success, or
                     @('nil') on failure.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(or (natp pid) (not pid))').</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::REMOVE-NONSTRINGS (OSLIB::X) :RETURNS (OSLIB::FILTERED- STRING-LISTP) (COND ((ATOM OSLIB::X) NIL) ((STRINGP (CAR OSLIB::X)) (CONS (CAR OSLIB::X) (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))) (T (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X))))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::REMOVE-NONSTRINGS (DEFUND OSLIB::REMOVE-NONSTRINGS (OSLIB::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::REMOVE-NONSTRINGS))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM OSLIB::X) NIL) ((STRINGP (CAR OSLIB::X)) (CONS (CAR OSLIB::X) (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))) (T (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::REMOVE-NONSTRINGS :FN (QUOTE OSLIB::REMOVE-NONSTRINGS) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::REMOVE-NONSTRINGS) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::REMOVE-NONSTRINGS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::REMOVE-NONSTRINGS) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::REMOVE-NONSTRINGS (OSLIB::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::REMOVE-NONSTRINGS))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM OSLIB::X) NIL) ((STRINGP (CAR OSLIB::X)) (CONS (CAR OSLIB::X) (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))) (T (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::REMOVE-NONSTRINGS :FN (QUOTE OSLIB::REMOVE-NONSTRINGS) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::REMOVE-NONSTRINGS) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::REMOVE-NONSTRINGS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::REMOVE-NONSTRINGS) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND OSLIB::REMOVE-NONSTRINGS (OSLIB::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE OSLIB::REMOVE-NONSTRINGS))) (DECLARE (IGNORABLE __FUNCTION__)) (COND ((ATOM OSLIB::X) NIL) ((STRINGP (CAR OSLIB::X)) (CONS (CAR OSLIB::X) (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))) (T (OSLIB::REMOVE-NONSTRINGS (CDR OSLIB::X)))))) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::REMOVE-NONSTRINGS :FN (QUOTE OSLIB::REMOVE-NONSTRINGS) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::REMOVE-NONSTRINGS) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::REMOVE-NONSTRINGS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::REMOVE-NONSTRINGS) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::FILTERED-) (DOC . "") (CUTIL::RETURN-TYPE STRING-LISTP OSLIB::FILTERED-) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM OSLIB::RETURN-TYPE-OF-REMOVE-NONSTRINGS (LET ((OSLIB::FILTERED- (OSLIB::REMOVE-NONSTRINGS OSLIB::X))) (STRING-LISTP OSLIB::FILTERED-)) :HINTS NIL :RULE-CLASSES :REWRITE))))))))) (VALUE-TRIPLE :INVISIBLE))) (9 RECORD-EXPANSION (DEFINE OSLIB::LS-SUBDIRS ((OSLIB::PATH "Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory." STRINGP) &OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (ERROR "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc." BOOLEANP :RULE-CLASSES :TYPE-PRESCRIPTION) (OSLIB::VAL "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem." (AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR)))) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Get a subdirectory listing." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the
<b>subdirectories</b> (not ordinary files) of the given @('path').</p>

<p>The subdirectory names returned are <b>not</b> complete paths.  For
instance, if @('/home/users/jared') contains directories named @('foo') and
@('bar'), then the resulting @('val') will have @('\"foo\"') and @('\"bar\"'),
not full paths like @('\"/home/users/jared/foo\"').</p>" :IGNORE-OK T (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::LS-SUBDIRS :PARENTS (OSLIB) :SHORT "Get a subdirectory listing." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the
<b>subdirectories</b> (not ordinary files) of the given @('path').</p>

<p>The subdirectory names returned are <b>not</b> complete paths.  For
instance, if @('/home/users/jared') contains directories named @('foo') and
@('bar'), then the resulting @('val') will have @('\"foo\"') and @('\"bar\"'),
not full paths like @('\"/home/users/jared/foo\"').</p>" (DEFMACRO OSLIB::LS-SUBDIRS (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-SUBDIRS-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-SUBDIRS-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-SUBDIRS))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-SUBDIRS OSLIB::LS-SUBDIRS-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE OSLIB::LS-SUBDIRS)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-SUBDIRS :FN (QUOTE OSLIB::LS-SUBDIRS-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-SUBDIRS-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-SUBDIRS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::LS-SUBDIRS)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::LS-SUBDIRS (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-SUBDIRS-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-SUBDIRS-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-SUBDIRS))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-SUBDIRS OSLIB::LS-SUBDIRS-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE OSLIB::LS-SUBDIRS)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-SUBDIRS :FN (QUOTE OSLIB::LS-SUBDIRS-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-SUBDIRS-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-SUBDIRS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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) (DEFMACRO OSLIB::LS-SUBDIRS (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-SUBDIRS-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-SUBDIRS-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-SUBDIRS))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-SUBDIRS OSLIB::LS-SUBDIRS-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE OSLIB::LS-SUBDIRS)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-SUBDIRS :FN (QUOTE OSLIB::LS-SUBDIRS-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-SUBDIRS-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-SUBDIRS))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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-LS-SUBDIRS-FN.ERROR (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-SUBDIRS-FN OSLIB::PATH STATE))) (BOOLEANP ERROR)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-LS-SUBDIRS-FN.VAL (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-SUBDIRS-FN OSLIB::PATH STATE))) (AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR)))) :HINTS NIL :RULE-CLASSES :REWRITE) (DEFTHM OSLIB::RETURN-TYPE-OF-LS-SUBDIRS-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-SUBDIRS-FN OSLIB::PATH STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::LS-SUBDIRS)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Get a subdirectory listing.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::LS-SUBDIRS))) 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>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the
<b>subdirectories</b> (not ordinary files) of the given @('path').</p>

<p>The subdirectory names returned are <b>not</b> complete paths.  For
instance, if @('/home/users/jared') contains directories named @('foo') and
@('bar'), then the resulting @('val') will have @('\"foo\"') and @('\"bar\"'),
not full paths like @('\"/home/users/jared/foo\"').</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::LS-SUBDIRS) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Get a subdirectory listing.") (:LONG . "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the
<b>subdirectories</b> (not ordinary files) of the given @('path').</p>

<p>The subdirectory names returned are <b>not</b> complete paths.  For
instance, if @('/home/users/jared') contains directories named @('foo') and
@('bar'), then the resulting @('val') will have @('\"foo\"') and @('\"bar\"'),
not full paths like @('\"/home/users/jared/foo\"').</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|LS-SUBDIRS-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-SUBDIRS-FN.ERROR|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-SUBDIRS-FN.VAL|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-SUBDIRS-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::LS-SUBDIRS)))))) (VALUE-TRIPLE (QUOTE OSLIB::LS-SUBDIRS))))) (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::LS-SUBDIRS)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::LS-SUBDIRS-FN) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::LS-SUBDIRS) 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::LS-SUBDIRS)) 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>(ls-subdirs path &amp;optional (state 'state))
  &rarr;
(mv error val state)</code></dt><dt>Arguments</dt><dd><tt>path</tt> &mdash; Directory to list files in.  May or may not include
                           a trailing slash.  May use standard idioms like
                           @('~') or @('~jared').  The empty string means the
                           current directory.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp path)').</color></dd>
<dt>Returns</dt><dd><tt>error</tt> &mdash; Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(booleanp error)').</color></dd>
<dd><tt>val</tt> &mdash; On success: a list of subdirectory names (excludes files).
                       On failure: an error message explaining the problem.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(and (equal (stringp val) error)
     (equal (string-listp val) (not error)))
').</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))))))))) (10 RECORD-EXPANSION (DEFINE OSLIB::LS-FILES ((OSLIB::PATH "Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory." STRINGP) &OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (ERROR "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc." BOOLEANP :RULE-CLASSES :TYPE-PRESCRIPTION) (OSLIB::VAL "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem." (AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR)))) (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Get a file listing." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the <b>files</b> (not
subdirectories) of the given @('path').</p>

<p>The file names returned are <b>not</b> complete paths.  For instance, if
@('/home/users/jared') contains @('foo.txt'), then @('val') will contain
@('\"foo.txt\") instead of @('\"/home/users/jared/foo.txt\"').</p>" :IGNORE-OK T (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::LS-FILES :PARENTS (OSLIB) :SHORT "Get a file listing." :LONG "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the <b>files</b> (not
subdirectories) of the given @('path').</p>

<p>The file names returned are <b>not</b> complete paths.  For instance, if
@('/home/users/jared') contains @('foo.txt'), then @('val') will contain
@('\"foo.txt\") instead of @('\"/home/users/jared/foo.txt\"').</p>" (DEFMACRO OSLIB::LS-FILES (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-FILES-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-FILES-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-FILES))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-FILES OSLIB::LS-FILES-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-FILES-FN) (QUOTE OSLIB::LS-FILES)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-FILES :FN (QUOTE OSLIB::LS-FILES-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-FILES-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-FILES))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-FILES-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::LS-FILES)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::LS-FILES (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-FILES-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-FILES-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-FILES))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-FILES OSLIB::LS-FILES-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-FILES-FN) (QUOTE OSLIB::LS-FILES)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-FILES :FN (QUOTE OSLIB::LS-FILES-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-FILES-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-FILES))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-FILES-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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) (DEFMACRO OSLIB::LS-FILES (OSLIB::PATH &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::LS-FILES-FN) OSLIB::PATH STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::LS-FILES-FN (OSLIB::PATH STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::PATH))) (LET ((__FUNCTION__ (QUOTE OSLIB::LS-FILES))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) ((WHEN OSLIB::ERR) (MV T (IF (STRINGP OSLIB::VAL) OSLIB::VAL "error") STATE))) (MV NIL (OSLIB::REMOVE-NONSTRINGS OSLIB::VAL) STATE))))) (ADD-MACRO-ALIAS OSLIB::LS-FILES OSLIB::LS-FILES-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::LS-FILES-FN) (QUOTE OSLIB::LS-FILES)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::LS-FILES :FN (QUOTE OSLIB::LS-FILES-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::LS-FILES-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::LS-FILES))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::LS-FILES-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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-LS-FILES-FN.ERROR (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-FILES-FN OSLIB::PATH STATE))) (BOOLEANP ERROR)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-LS-FILES-FN.VAL (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-FILES-FN OSLIB::PATH STATE))) (AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR)))) :HINTS NIL :RULE-CLASSES :REWRITE) (DEFTHM OSLIB::RETURN-TYPE-OF-LS-FILES-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV LISP::?ERROR OSLIB::?VAL ?STATE) (OSLIB::LS-FILES-FN OSLIB::PATH STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::LS-FILES)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Get a file listing.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::LS-FILES))) 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>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the <b>files</b> (not
subdirectories) of the given @('path').</p>

<p>The file names returned are <b>not</b> complete paths.  For instance, if
@('/home/users/jared') contains @('foo.txt'), then @('val') will contain
@('\"foo.txt\") instead of @('\"/home/users/jared/foo.txt\"').</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::LS-FILES) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Get a file listing.") (:LONG . "<p>In the logic this function reads from the ACL2 oracle.  In the
execution we query the file system to obtain a listing of the <b>files</b> (not
subdirectories) of the given @('path').</p>

<p>The file names returned are <b>not</b> complete paths.  For instance, if
@('/home/users/jared') contains @('foo.txt'), then @('val') will contain
@('\"foo.txt\") instead of @('\"/home/users/jared/foo.txt\"').</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|LS-FILES-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-FILES-FN.ERROR|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-FILES-FN.VAL|)
@(def |OSLIB|::|RETURN-TYPE-OF-LS-FILES-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::LS-FILES)))))) (VALUE-TRIPLE (QUOTE OSLIB::LS-FILES))))) (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::LS-FILES)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::LS-FILES-FN) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::PATH) (GUARD STRINGP OSLIB::PATH) (DOC . "Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory.") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . ERROR) (DOC . "Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.") (CUTIL::RETURN-TYPE BOOLEANP ERROR) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :TYPE-PRESCRIPTION)) (:RETURN-SPEC (CUTIL::NAME . OSLIB::VAL) (DOC . "On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.") (CUTIL::RETURN-TYPE AND (EQUAL (STRINGP OSLIB::VAL) ERROR) (EQUAL (STRING-LISTP OSLIB::VAL) (NOT ERROR))) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)) (: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::LS-FILES) 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::LS-FILES)) 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>(ls-files path &amp;optional (state 'state))
  &rarr;
(mv error val state)</code></dt><dt>Arguments</dt><dd><tt>path</tt> &mdash; Directory to list files in.  May or may not include
                         a trailing slash.  May use standard idioms like
                         @('~') or @('~jared').  The empty string means the
                         current directory.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp path)').</color></dd>
<dt>Returns</dt><dd><tt>error</tt> &mdash; Success indicator.  We can fail if @('path') does not
                       exist or isn't readable, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(booleanp error)').</color></dd>
<dd><tt>val</tt> &mdash; On success: a list of file names (excluding directories).
                     On failure: an error message explaining the problem.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(and (equal (stringp val) error)
     (equal (string-listp val) (not error)))
').</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))))))))) (11 RECORD-EXPANSION (DEFINE OSLIB::MKDIR ((OSLIB::DIR "The path that you want to create, e.g., @('./foo/bar')" STRINGP) &OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (OSLIB::SUCCESSP BOOLEANP :RULE-CLASSES :TYPE-PRESCRIPTION "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Make new directories if they don't already exist, like @('mkdir -p'),
and return a success indicator so you can recover from errors." :LONG "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to create directories using the
Common Lisp function @('ensure-directories-exist'), and capture any
errors.</p>" :IGNORE-OK T (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::MKDIR :PARENTS (OSLIB) :SHORT "Make new directories if they don't already exist, like @('mkdir -p'),
and return a success indicator so you can recover from errors." :LONG "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to create directories using the
Common Lisp function @('ensure-directories-exist'), and capture any
errors.</p>" (DEFMACRO OSLIB::MKDIR (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::MKDIR-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::MKDIR OSLIB::MKDIR-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR-FN) (QUOTE OSLIB::MKDIR)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR :FN (QUOTE OSLIB::MKDIR-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::MKDIR)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::MKDIR (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::MKDIR-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::MKDIR OSLIB::MKDIR-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR-FN) (QUOTE OSLIB::MKDIR)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR :FN (QUOTE OSLIB::MKDIR-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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) (DEFMACRO OSLIB::MKDIR (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::MKDIR-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::MKDIR OSLIB::MKDIR-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR-FN) (QUOTE OSLIB::MKDIR)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR :FN (QUOTE OSLIB::MKDIR-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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-MKDIR-FN.SUCCESSP (B* (((MV OSLIB::?SUCCESSP ?STATE) (OSLIB::MKDIR-FN OSLIB::DIR STATE))) (BOOLEANP OSLIB::SUCCESSP)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-MKDIR-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?SUCCESSP ?STATE) (OSLIB::MKDIR-FN OSLIB::DIR STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::MKDIR)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Make new directories if they don't already exist, like @('mkdir -p'),
and return a success indicator so you can recover from errors.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::MKDIR))) 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>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to create directories using the
Common Lisp function @('ensure-directories-exist'), and capture any
errors.</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::MKDIR) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Make new directories if they don't already exist, like @('mkdir -p'),
and return a success indicator so you can recover from errors.") (:LONG . "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to create directories using the
Common Lisp function @('ensure-directories-exist'), and capture any
errors.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|MKDIR-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-MKDIR-FN.SUCCESSP|)
@(def |OSLIB|::|RETURN-TYPE-OF-MKDIR-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::MKDIR)))))) (VALUE-TRIPLE (QUOTE OSLIB::MKDIR))))) (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::MKDIR)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::MKDIR-FN) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::MKDIR) 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::MKDIR)) 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>(mkdir dir &amp;optional (state 'state)) &rarr; (mv successp state)</code></dt><dt>Arguments</dt><dd><tt>dir</tt> &mdash; The path that you want to create, e.g., @('./foo/bar').<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp dir)').</color></dd>
<dt>Returns</dt><dd><tt>successp</tt> &mdash; Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(booleanp successp)').</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))))))))) (12 RECORD-EXPANSION (DEFINE OSLIB::MKDIR! ((OSLIB::DIR "The path that you want to create, e.g., @('./foo/bar')" STRINGP) &OPTIONAL (STATE (QUOTE STATE))) :RETURNS (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE))) :PARENTS (OSLIB) :SHORT "Make new directories if they don't already exist, like @('mkdir -p'),
or cause a hard error if there is any problem." :LONG "<p>This is just a wrapper for @(see mkdir) that causes an error on any
failure.</p>" (B* (((MV OSLIB::SUCCESSP STATE) (OSLIB::MKDIR OSLIB::DIR STATE)) ((UNLESS OSLIB::SUCCESSP) (RAISE "Failed to create ~s0." OSLIB::DIR) STATE)) STATE)) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::MKDIR! :PARENTS (OSLIB) :SHORT "Make new directories if they don't already exist, like @('mkdir -p'),
or cause a hard error if there is any problem." :LONG "<p>This is just a wrapper for @(see mkdir) that causes an error on any
failure.</p>" (DEFMACRO OSLIB::MKDIR! (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR!-FN) OSLIB::DIR STATE)) (DEFUND OSLIB::MKDIR!-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR!))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::SUCCESSP STATE) (OSLIB::MKDIR OSLIB::DIR STATE)) ((UNLESS OSLIB::SUCCESSP) (RAISE "Failed to create ~s0." OSLIB::DIR) STATE)) STATE))) (ADD-MACRO-ALIAS OSLIB::MKDIR! OSLIB::MKDIR!-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR!-FN) (QUOTE OSLIB::MKDIR!)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR! :FN (QUOTE OSLIB::MKDIR!-FN) :RETURNS (QUOTE ((: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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR!-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR!))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR!-FN) (QUOTE ((: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::MKDIR!)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::MKDIR! (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR!-FN) OSLIB::DIR STATE)) (DEFUND OSLIB::MKDIR!-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR!))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::SUCCESSP STATE) (OSLIB::MKDIR OSLIB::DIR STATE)) ((UNLESS OSLIB::SUCCESSP) (RAISE "Failed to create ~s0." OSLIB::DIR) STATE)) STATE))) (ADD-MACRO-ALIAS OSLIB::MKDIR! OSLIB::MKDIR!-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR!-FN) (QUOTE OSLIB::MKDIR!)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR! :FN (QUOTE OSLIB::MKDIR!-FN) :RETURNS (QUOTE ((: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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR!-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR!))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR!-FN) (QUOTE ((: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) (DEFMACRO OSLIB::MKDIR! (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::MKDIR!-FN) OSLIB::DIR STATE)) (DEFUND OSLIB::MKDIR!-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::MKDIR!))) (DECLARE (IGNORABLE __FUNCTION__)) (B* (((MV OSLIB::SUCCESSP STATE) (OSLIB::MKDIR OSLIB::DIR STATE)) ((UNLESS OSLIB::SUCCESSP) (RAISE "Failed to create ~s0." OSLIB::DIR) STATE)) STATE))) (ADD-MACRO-ALIAS OSLIB::MKDIR! OSLIB::MKDIR!-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::MKDIR!-FN) (QUOTE OSLIB::MKDIR!)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::MKDIR! :FN (QUOTE OSLIB::MKDIR!-FN) :RETURNS (QUOTE ((: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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::MKDIR!-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::MKDIR!))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::MKDIR!-FN) (QUOTE ((: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-MKDIR!-FN (IMPLIES (FORCE (STATE-P1 STATE)) (LET ((STATE (OSLIB::MKDIR!-FN OSLIB::DIR STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::MKDIR!)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Make new directories if they don't already exist, like @('mkdir -p'),
or cause a hard error if there is any problem.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::MKDIR!))) 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>This is just a wrapper for @(see mkdir) that causes an error on any
failure.</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::MKDIR!) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Make new directories if they don't already exist, like @('mkdir -p'),
or cause a hard error if there is any problem.") (:LONG . "<p>This is just a wrapper for @(see mkdir) that causes an error on any
failure.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|MKDIR!-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-MKDIR!-FN|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::MKDIR!)))))) (VALUE-TRIPLE (QUOTE OSLIB::MKDIR!))))) (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::MKDIR!)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::MKDIR!-FN) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to create, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((: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::MKDIR!) 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::MKDIR!)) 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>(mkdir! dir &amp;optional (state 'state)) &rarr; state</code></dt><dt>Arguments</dt><dd><tt>dir</tt> &mdash; The path that you want to create, e.g., @('./foo/bar').<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp dir)').</color></dd>
<dt>Returns</dt><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))))))))) (13 RECORD-EXPANSION (DEFINE OSLIB::RMTREE ((OSLIB::DIR "The path that you want to remove, e.g., @('./foo/bar')" STRINGP) &OPTIONAL (STATE (QUOTE STATE))) :RETURNS (MV (OSLIB::SUCCESSP BOOLEANP :RULE-CLASSES :TYPE-PRESCRIPTION "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (STATE STATE-P1 :HYP (FORCE (STATE-P1 STATE)))) :PARENTS (OSLIB) :SHORT "Recursively delete files, like the shell command @('rm -rf'), and
return a success indicator so you can recover from errors." :LONG "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to delete the requested path, and
detect errors.</p>" :IGNORE-OK T (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))) (PROGN (RECORD-EXPANSION (DEFSECTION OSLIB::RMTREE :PARENTS (OSLIB) :SHORT "Recursively delete files, like the shell command @('rm -rf'), and
return a success indicator so you can recover from errors." :LONG "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to delete the requested path, and
detect errors.</p>" (DEFMACRO OSLIB::RMTREE (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::RMTREE-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::RMTREE-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::RMTREE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::RMTREE OSLIB::RMTREE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::RMTREE-FN) (QUOTE OSLIB::RMTREE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::RMTREE :FN (QUOTE OSLIB::RMTREE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to remove, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::RMTREE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::RMTREE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::RMTREE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::RMTREE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO OSLIB::RMTREE (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::RMTREE-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::RMTREE-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::RMTREE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::RMTREE OSLIB::RMTREE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::RMTREE-FN) (QUOTE OSLIB::RMTREE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::RMTREE :FN (QUOTE OSLIB::RMTREE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to remove, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::RMTREE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::RMTREE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::RMTREE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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) (DEFMACRO OSLIB::RMTREE (OSLIB::DIR &OPTIONAL (STATE (QUOTE STATE))) (LIST (QUOTE OSLIB::RMTREE-FN) OSLIB::DIR STATE)) (ENCAPSULATE NIL (SET-IGNORE-OK T) (DEFUND OSLIB::RMTREE-FN (OSLIB::DIR STATE) (DECLARE (XARGS :STOBJS (STATE))) (DECLARE (XARGS :GUARD (STRINGP OSLIB::DIR))) (LET ((__FUNCTION__ (QUOTE OSLIB::RMTREE))) (DECLARE (IGNORABLE __FUNCTION__)) (B* ((- (RAISE "Raw Lisp definition not installed?")) ((MV OSLIB::ERR OSLIB::VAL STATE) (READ-ACL2-ORACLE STATE)) (OSLIB::OKP (AND (NOT OSLIB::ERR) (BOOLEANP OSLIB::VAL) OSLIB::VAL))) (MV OSLIB::OKP STATE))))) (ADD-MACRO-ALIAS OSLIB::RMTREE OSLIB::RMTREE-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE OSLIB::RMTREE-FN) (QUOTE OSLIB::RMTREE)) (CUTIL::EXTEND-DEFINE-TABLE OSLIB::RMTREE :FN (QUOTE OSLIB::RMTREE-FN) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to remove, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE OSLIB::RMTREE-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE OSLIB::RMTREE))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE OSLIB::RMTREE-FN) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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-RMTREE-FN.SUCCESSP (B* (((MV OSLIB::?SUCCESSP ?STATE) (OSLIB::RMTREE-FN OSLIB::DIR STATE))) (BOOLEANP OSLIB::SUCCESSP)) :HINTS NIL :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM OSLIB::RETURN-TYPE-OF-RMTREE-FN.STATE (IMPLIES (FORCE (STATE-P1 STATE)) (B* (((MV OSLIB::?SUCCESSP ?STATE) (OSLIB::RMTREE-FN OSLIB::DIR STATE))) (STATE-P1 STATE))) :HINTS NIL :RULE-CLASSES :REWRITE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE OSLIB::RMTREE)) (XDOC::PARENTS (QUOTE (OSLIB))) (XDOC::SHORT (QUOTE "Recursively delete files, like the shell command @('rm -rf'), and
return a success indicator so you can recover from errors.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE OSLIB::RMTREE))) 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>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to delete the requested path, and
detect errors.</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::RMTREE) (:BASE-PKG . OSLIB::ACL2-PKG-WITNESS) (:PARENTS OSLIB) (:SHORT . "Recursively delete files, like the shell command @('rm -rf'), and
return a success indicator so you can recover from errors.") (:LONG . "<p>In the logic this function reads from the ACL2 oracle to determine
if it succeeds.  In the execution, we attempt to delete the requested path, and
detect errors.</p>

<h3>Definitions and Theorems</h3>@(def |OSLIB|::|RMTREE-FN|)
@(def |OSLIB|::|RETURN-TYPE-OF-RMTREE-FN.SUCCESSP|)
@(def |OSLIB|::|RETURN-TYPE-OF-RMTREE-FN.STATE|)") (:FROM . "[books]/oslib/logic-defs.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC OSLIB::RMTREE)))))) (VALUE-TRIPLE (QUOTE OSLIB::RMTREE))))) (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::RMTREE)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE OSLIB::RMTREE-FN) (QUOTE ((:FORMAL (CUTIL::NAME . OSLIB::DIR) (GUARD STRINGP OSLIB::DIR) (DOC . "The path that you want to remove, e.g., @('./foo/bar')") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . STATE) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . OSLIB::SUCCESSP) (DOC . "Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.") (CUTIL::RETURN-TYPE BOOLEANP OSLIB::SUCCESSP) (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::RMTREE) 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::RMTREE)) 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>(rmtree dir &amp;optional (state 'state)) &rarr; (mv successp state)</code></dt><dt>Arguments</dt><dd><tt>dir</tt> &mdash; The path that you want to remove, e.g., @('./foo/bar').<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Guard @('(stringp dir)').</color></dd>
<dt>Returns</dt><dd><tt>successp</tt> &mdash; Success indicator.  We might fail due to file system
                          permissions, illegal file names, etc.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Type @('(booleanp successp)').</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/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))
317160729