/usr/share/acl2-6.3/books/parallel/matrix-multiplication-parallel.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
((6 RECORD-EXPANSION (ASSERT! (EQUAL (GET-MIDPOINTS 4 6) (CONS 5 6))) (VALUE-TRIPLE :SUCCESS)) (7 RECORD-EXPANSION (ASSERT! (EQUAL (GET-MIDPOINTS 4 7) (CONS 5 6))) (VALUE-TRIPLE :SUCCESS)) (10 RECORD-EXPANSION (OBSERVE$ "Running simple matrix multiplcation test.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (11 RECORD-EXPANSION (ASSERT! (LET ((MINI-MATRIX (QUOTE ((1 2 3) (4 5 6) (7 8 9))))) (EQUAL (PMULTIPLY-MATRICES MINI-MATRIX MINI-MATRIX 3 3 3 3) (QUOTE ((14 32 50) (32 77 122) (50 122 194)))))) (VALUE-TRIPLE :SUCCESS)) (12 RECORD-EXPANSION (OBSERVE$ "Generating 32 bit source matrices A and B (parallel case).") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (13 RECORD-EXPANSION (ASSIGN$ A (MAKE-MATRIX *A-ROWS* *A-COLS* NIL)) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (14 RECORD-EXPANSION (ASSIGN$ B (MAKE-MATRIX *B-ROWS* *B-COLS* NIL)) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (15 RECORD-EXPANSION (OBSERVE$ "Testing the time it takes to transpose B.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (16 RECORD-EXPANSION (ASSIGN$ B-TRANSPOSED (TIME$ (TRANSPOSE-FAST (@ B)))) (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE NIL))) (17 RECORD-EXPANSION (OBSERVE$ "Testing the time it takes to generate the results (parallel case). ~
It has taken approximately 10.0 seconds on an 8-core machine.") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))) (18 RECORD-EXPANSION (ASSERT-WHEN-PARALLEL (TIME$ (PMULTIPLY-MATRICES (@ A) (@ B-TRANSPOSED) *A-ROWS* *A-COLS* *B-ROWS* *B-COLS*))) (VALUE-TRIPLE :SUCCESS)) (19 RECORD-EXPANSION (OBSERVE$ "Done testing matrix multiplication (parallel case).") (WITH-OUTPUT :OFF SUMMARY (VALUE-TRIPLE :INVISIBLE))))
NIL
(("/usr/share/acl2-6.3/books/parallel/matrix-multiplication-parallel.lisp" "matrix-multiplication-parallel" "matrix-multiplication-parallel" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1312434800) ("/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))
1032469817
|