ACL2 seminar May 12, 2010

• Release notes (plan to discuss items shown in black)
• Demo of defattach (which is still under development):
  • script.lisp
  • log.txt
• Demo of fast include-book:
  • script.lsp
  • log1.txt: Tests that illustrate order of loads, as well as warnings and errors. In the following, book1 includes book2a and book2b, which include book3a and book3b respectively, which both include book4.
    • Book book1.lisp
    • Book book2a.lisp
    • Book book2b.lisp
    • Book book3a.lisp
    • Book book3b.lisp
    • Book book4.lisp
  • log2.txt: Make sure the soundness bug related to *1* fns and :program mode is gone.
    • Book bk1.lisp
    • Book bk2.lisp
  • log3.txt: Potentially huge speed-up when there is heavy macroexpansion
    • Book speed-test1.lisp
    • Book speed-test2.lisp