/usr/share/acl2-6.3/books/cgen/with-timeout.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "DEFDATA" (APPEND (QUOTE (GETPROP KEY VAL FORMALS MACRO-ARGS CONST DECODE-LOGICAL-NAME VALUE LEGAL-CONSTANTP ER-LET* B* MACROEXPAND1 TRANS-EVAL SIMPLE-TRANSLATE-AND-EVAL ASSERT-EVENT LEGAL-VARIABLE-OR-CONSTANT-NAMEP F-BOUNDP-GLOBAL F-GET-GLOBAL F-PUT-GLOBAL PROOF-CHECKER EXPANSION EQUIVALENCE-RELATIONP 1+F 1-F +F -F DEFXDOC CURRENT-ACL2-WORLD E/D UNSIGNED-BYTE-P DEFREC VARIABLEP FQUOTEP FFN-SYMB FLAMBDAP FARGS LAMBDA-BODY LAMBDA-FORMALS SUBCOR-VAR DUMB-NEGATE-LIT IS-SUBTYPE IS-DISJOINT NAT-LISTP ALLP ACL2-NUMBER-LISTP NATURALS-LISTP POS-LISTP ONEOF ANYOF DATA-CONSTRUCTORS X N V INFXLST FINXLST LISTOF ENUM RECORD MAP SET NFIXG SET-ACL2S-DEFDATA-VERBOSE GET-ACL2S-DEFDATA-VERBOSE MGET MSET C REGISTER-DATA-CONSTRUCTOR DEFINE-ENUMERATION-TYPE DEFDATA-SUBTYPE DEFDATA-DISJOINT REGISTER-CUSTOM-TYPE DEFDATA DEFDATA-TESTING TEST? TOP-LEVEL-TEST? ACL2S-DEFAULTS SET-ACL2S-RANDOM-TESTING-ENABLED GET-ACL2S-RANDOM-TESTING-ENABLED DONT-PRINT-THANKS-MESSAGE-OVERRIDE-HINT NUM-TRIALS VERBOSITY-LEVEL SHOW-TESTING-OUTPUT NUM-WITNESSES NUM-COUNTEREXAMPLES SHOW-TOP-LEVEL-COUNTEREXAMPLE SAMPLING-METHOD BACKTRACK-LIMIT SUBGOAL-TIMEOUT SEARCH-STRATEGY STOPPING-CONDITION TESTING-ENABLED SYSTEM-DEBUG-FLAG INHIBIT-OUTPUT-FLAG NORMAL-OUTPUT-FLAG VERBOSE-FLAG DEBUG-FLAG)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
(INCLUDE-BOOK "std/osets/portcullis" :DIR :SYSTEM)
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (DEFXDOC WITH-TIMEOUT :PARENTS (TESTING) :SHORT "Evaluate form with a timeout (in seconds)" :LONG "Evaluate form with a timeout in seconds. The syntax of
this macro is (with-timeout <i>duration</i> <i>body</i>
<i>timeout-form</i>).
A duration of 0 seconds disables the timeout mechanism,
i.e its a no-op. Otherwise, if <i>duration</i> seconds elapse
during evaluation of <i>body</i> then the evaluation is
aborted and the value of <tt>timeout-form</tt> is returned,
otherwise returns the value of <tt>body</tt>. The signature of
<tt>body</tt> and <tt>timeout-form</tt> should be the same.
Advanced Notes:
This form should be called either at the top-level or in an environment
where state is available and <tt>body</tt> has no free variables
other than state.
If the timeout-form is a long running computation,
then the purpose of with-timeout is defeated.
<code>
Usage:
(with-timeout 5 (fibonacci 40) :timeout)
:doc with-timeout
</code>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WITH-TIMEOUT) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS TESTING) (:SHORT . "Evaluate form with a timeout (in seconds)") (:LONG . "Evaluate form with a timeout in seconds. The syntax of
this macro is (with-timeout <i>duration</i> <i>body</i>
<i>timeout-form</i>).
A duration of 0 seconds disables the timeout mechanism,
i.e its a no-op. Otherwise, if <i>duration</i> seconds elapse
during evaluation of <i>body</i> then the evaluation is
aborted and the value of <tt>timeout-form</tt> is returned,
otherwise returns the value of <tt>body</tt>. The signature of
<tt>body</tt> and <tt>timeout-form</tt> should be the same.
Advanced Notes:
This form should be called either at the top-level or in an environment
where state is available and <tt>body</tt> has no free variables
other than state.
If the timeout-form is a long running computation,
then the purpose of with-timeout is defeated.
<code>
Usage:
(with-timeout 5 (fibonacci 40) :timeout)
:doc with-timeout
</code>") (:FROM . "[books]/cgen/with-timeout.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WITH-TIMEOUT)))))))
(("/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/cgen/with-timeout.lisp" "with-timeout" "with-timeout" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:ACL2S-TIMEOUT "/usr/share/acl2-6.3/books/cgen/with-timeout.lisp"))) . 916923546) ("/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/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557))
1367842341
|