[acl2/acl2] f323a6: Restore compilation and caching of tame compliant ...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: f323a64fd39fc7cf031f065f0e015a6a28a3ec90
https://github.com/acl2/acl2/commit/f323a64fd39fc7cf031f065f0e015a6a28a3ec90
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2018-01-15 (Mon, 15 Jan 2018)

Changed paths:
M apply-raw.lisp
M apply.lisp
M axioms.lisp
M books/system/doc/acl2-doc.lisp
A books/system/tests/apply-timings.lisp
M doc.lisp
M history-management.lisp
M interface-raw.lisp
M other-events.lisp

Log Message:
-----------
Restore compilation and caching of tame compliant lambdas for apply$.

Quoting :doc note-8-1:

Calls of the form (apply$ (lambda ...) ...) were running slowly
because an optimization failed to be installed during the ACL2
build. That optimization is now in place. (The optimization,
which compiles and caches ``tame compliant'' lambdas, had been used
in the unadvertised use of ``The Rubric'' prior to the release of
ACL2 Version 8.0.)

Added some timing tests for apply$.

[GitHub]

Branch: refs/heads/testing