/usr/share/acl2-6.3/books/make-event/eval-tests.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 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (MUST-SUCCEED (DEFTHM EVAL-BAR (EQUAL X (CAR (CONS X Y))) :RULE-CLASSES NIL)) (VALUE-TRIPLE (QUOTE T))) (4 RECORD-EXPANSION (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X))))) (VALUE-TRIPLE (QUOTE T))) (5 RECORD-EXPANSION (MUST-SUCCEED (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))) (VALUE-TRIPLE (QUOTE T))) (6 RECORD-EXPANSION (MUST-SUCCEED (WITH-OUTPUT :OFF :ALL (PPROGN (F-PUT-GLOBAL (QUOTE SAVED-WORLD-LENGTH) (LENGTH (W STATE)) STATE) (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF :ALL (THM (EQUAL X (CONS X X)))))))))) (VALUE-TRIPLE (QUOTE T))) (7 RECORD-EXPANSION (MUST-SUCCEED (DEFTHM TEMP (EQUAL (CAR (CONS X Y)) X))) (VALUE-TRIPLE (QUOTE T))) (8 RECORD-EXPANSION (MUST-FAIL (MV (EQUAL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))) NIL STATE)) (VALUE-TRIPLE (QUOTE T))) (9 RECORD-EXPANSION (MUST-SUCCEED (WITH-OUTPUT :OFF ERROR (COND ((NOT (EQL (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE)))) (WITH-OUTPUT :ON ERROR (ER SOFT (QUOTE TEST-FAILURE) "World length changed from ~x0 to ~x1." (F-GET-GLOBAL (QUOTE SAVED-WORLD-LENGTH) STATE) (LENGTH (W STATE))))) (T (MUST-FAIL (MUST-FAIL (MUST-FAIL (WITH-OUTPUT :OFF ERROR (THM (EQUAL X (CONS X X))))))))))) (VALUE-TRIPLE (QUOTE T))) (10 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL))))) (VALUE-TRIPLE (QUOTE T))) (11 RECORD-EXPANSION (MUST-SUCCEED (MAKE-EVENT (MV NIL (QUOTE (VALUE-TRIPLE NIL)) STATE))) (VALUE-TRIPLE (QUOTE T))) (12 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV T NIL STATE))) (VALUE-TRIPLE (QUOTE T))) (13 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV "Sample Expansion Error" NIL STATE))) (VALUE-TRIPLE (QUOTE T))) (14 RECORD-EXPANSION (MUST-FAIL (MAKE-EVENT (MV (MSG "Sample Expansion Error: ~x0, ~@1" 17 (MSG "howdy ~x0" 23)) NIL STATE))) (VALUE-TRIPLE (QUOTE T))))
NIL
(("/usr/share/acl2-6.3/books/make-event/eval-tests.lisp" "eval-tests" "eval-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653391125) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "misc/eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
1981589227
|