/usr/share/acl2-6.3/books/parallel/matrix-multiplication-serial.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 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((7 RECORD-EXPANSION (OBSERVE$ "Running simple matrix multiplcation test.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (8 RECORD-EXPANSION (ASSERT! (LET ((MINI-MATRIX (QUOTE ((1 2 3) (4 5 6) (7 8 9))))) (EQUAL (MULTIPLY-MATRICES MINI-MATRIX MINI-MATRIX) (QUOTE ((14 32 50) (32 77 122) (50 122 194)))))) (VALUE-TRIPLE :SUCCESS)) (9 RECORD-EXPANSION (OBSERVE$ "Generating 32 bit source matrices A and B (serial case).") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (10 RECORD-EXPANSION (ASSIGN$ A (MAKE-MATRIX *A-ROWS* *A-COLS* NIL)) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (11 RECORD-EXPANSION (ASSIGN$ B (MAKE-MATRIX *B-ROWS* *B-COLS* NIL)) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (12 RECORD-EXPANSION (OBSERVE$ "Testing the time it takes to transpose B.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (13 RECORD-EXPANSION (ASSIGN$ B-TRANSPOSED (TIME$ (TRANSPOSE-FAST (@ B)))) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (14 RECORD-EXPANSION (OBSERVE$ "Testing the time it takes to generate the results (serial case). ~
It takes approximately 22.6 seconds on our machine.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (15 RECORD-EXPANSION (ASSERT-WHEN-PARALLEL (TIME$ (MULTIPLY-MATRICES (@ A) (@ B-TRANSPOSED)))) (VALUE-TRIPLE :SUCCESS)) (16 RECORD-EXPANSION (OBSERVE$ "Done testing matrix multiplication (serial case).") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))))
NIL
(("/usr/share/acl2-6.3/books/parallel/matrix-multiplication-serial.lisp" "matrix-multiplication-serial" "matrix-multiplication-serial" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2018833486) ("/usr/share/acl2-6.3/books/parallel/matrix-multiplication-setup.lisp" "matrix-multiplication-setup" "matrix-multiplication-setup" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 455783142) ("/usr/share/acl2-6.3/books/make-event/embeddable-event-forms.lisp" "make-event/embeddable-event-forms" "embeddable-event-forms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1882374340) ("/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))
2020209464
|