Incorporated fix from Sol Swords for :logic definition of fast-alist-clean.  This was a soundness bug (mine) but was not in Version 6.4.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1341 5d84a466-a78b-0930-a311-59b22171a541
Added (declaim (inline min-fixnum)) as suggested by Jared.

Fixed comment in split-at-position (thanks to Jared for pointing out a
mistake in that comment).

Fixed a comment typo.

Updated doc.lisp to match books/system/doc/acl2-doc.lisp.

Improved a warning in chk-acceptable-linear-rule2 to clarify that only
relevant triggers are a problem for free variables.

Added function find-symbol-in-current-package, and used it to speed up (we
think) some printing routines.  Thanks to Jared Davis for pointing out
potential value of such a change.



git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1344 5d84a466-a78b-0930-a311-59b22171a541
Quoting :doc note-6-5:

  (GCL only) Arranged for state global 'tmp-dir to be set to GCL's
  si::*tmp-dir*, even on Windows; this may be important for
  compilation on Windows. Thanks to Camm Maguire for pointing out the
  need to set 'tmp-dir for ACL2 built on GCL on mingw.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1346 5d84a466-a78b-0930-a311-59b22171a541
Quoting :doc note-6-5:

  (GCL only) Arranged for state global 'tmp-dir to be set to GCL's
  si::*tmp-dir*, even on Windows; this may be important for
  compilation on Windows. Thanks to Camm Maguire for pointing out the
  need to set 'tmp-dir for ACL2 built on GCL on mingw.

  (GCL only) Now, [gc$] may be called with no arguments, in which case
  the missing argument for system::gc is t.

Fixed a bug in memoize-raw.lisp, function
memoize-summary-after-compute-calls-and-times, found in a GCL-based
regression of ACL2(h).  At some point I should note this in :doc
note-6-5, but perhaps instead there will be a more sweeping comment
there about revising memoize-raw.lisp.

Temporarily modified print-alist to work around an apparent bug in
check-type in GCL 2.6.10.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1347 5d84a466-a78b-0930-a311-59b22171a541
**NOTE 1**:
Two proofs in the regression originally failed due to the bug
discussed below, but have been fixed.  You may wish to update your
development copy of ACL2 soon.

**NOTE 2**:
It wouldn't surprise me if there is a Version 6.5 release within a few
days.  If you have any pending commits to the books, you may wish to
get them in soon.

Quoting :doc note-6-5:

  We fixed a soundness bug in how the [tau-system] processed calls of
  if. Thanks to Dmitry Nadezhin for reporting this bug by sending a
  simple example that exploited it to prove nil. To see that example,
  see the comment about ``tau soundess bug'' in the form (defxdoc
  note-6-5 ...) in [community-books] file
  books/system/doc/acl2-doc.lisp.



git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1348 5d84a466-a78b-0930-a311-59b22171a541
Clarified what is meant by book references to LICENSE file.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1350 5d84a466-a78b-0930-a311-59b22171a541
Updated doc.lisp to match broken-link update in books/system/doc/acl2-doc.lisp.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1351 5d84a466-a78b-0930-a311-59b22171a541
Incorporated into doc.lisp change from Jared to books/system/doc/acl2-doc.lisp, about building books/system/doc/rendered-doc-combined.lsp.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1352 5d84a466-a78b-0930-a311-59b22171a541
Fixed an ACL2(h) bug (probably mine) that showed up during safety-3 testing.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1353 5d84a466-a78b-0930-a311-59b22171a541
Rearranged axioms.lisp in order for "make proofs" to succeed.
Also removed an obsolete comment from axioms.lisp (perhaps
dating from before Version 1.8!).


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1354 5d84a466-a78b-0930-a311-59b22171a541
Made further improvements to invariant-risk handling.  For one thing,
mv-let-for-with-local-stobj had a soundness bug (introduced after
Version 6.4):

  (in-package "ACL2")

  (defstobj st fld)

  (defun foo ()
    (declare (xargs :verify-guards nil))
    (with-local-stobj
     st
     (mv-let (result st)
	     (mv (mbe :logic 'logic :exec 'exec) st)
	     result)))

  (defthm wrong
    (equal (foo) 'logic)
    :hints (("Goal" :in-theory (disable (foo))))
    :rule-classes nil)

  (defthm contradiction
    nil
    :hints (("Goal" :use wrong))
    :rule-classes nil)

For another bug, see the comment at the end of this sequence of
events.

  (defun f-log () (mbe :logic 'logic :exec 'exec))
  (defstobj st (fld :type integer :initially 0))
  (defun f-prog (st)
    (declare (xargs :stobjs st :mode :program))
    (let ((st (update-fld 3 st)))
      (mv (f-log) st)))
  (f-prog st)
  (defun f-prog2 (st)
    (declare (xargs :stobjs st :mode :program))
    (let ((st (update-fld 3 st)))
      (mv (ec-call (f-log)) st)))
  ; The following should return
  ; (LOGIC <st>)
  ; and now it does, but previously it returned
  ; (EXEC <st>).
  (f-prog2 st)

Also, improved comments and :doc note-6-5 item about invariant-risk.

As far as I know, invariant-risk handling is perfect (!) now.  But I
may look into speeding up code.  Consider event MAX6-PROOF from
books/workshops/2009/sumners/support/examples.lisp.  The time reported
on my laptop has been (and I think this is virtually the same
regardless of whether we use ACL2(h) before or after this check-in).

; 29.21 seconds realtime, 26.03 seconds runtime
; (4,772,821,600 bytes allocated).

But if first I execute (setq *ignore-invariant-risk* t) in raw Lisp,
to defeat handling of invariant-risk (by restricting some execution to
*1* functions), then I get:

; 0.66 seconds realtime, 0.16 seconds runtime
; (24,119,776 bytes allocated).


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1355 5d84a466-a78b-0930-a311-59b22171a541
Updating doc.lisp for invariant-risk change to :doc note-6-5 in books/system/doc/acl2-doc.lisp

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1356 5d84a466-a78b-0930-a311-59b22171a541
Added guard to all-but-last and put it in guard-verified :logic mode, as requested by Warren Hunt.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1357 5d84a466-a78b-0930-a311-59b22171a541
Added reference to non-parallel-book from :doc
set-waterfall-parallelism.



git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1358 5d84a466-a78b-0930-a311-59b22171a541
Incorporated mods to :doc note-6-5.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1359 5d84a466-a78b-0930-a311-59b22171a541
(Affects ACL2(r) only) Installed patch from Ruben Gamboa for ACL2(r)
bug.

Updated some comments in GNUmakefile.  Thanks to Harsh Raju Chamarthi
for feedback that led me to make these updates.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1360 5d84a466-a78b-0930-a311-59b22171a541
Miscellaneous updates to installation instructions, including pointing to acl2.org for tarballs.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1361 5d84a466-a78b-0930-a311-59b22171a541
NOTE: Unless I encounter unforeseen problems, this should be the last
check-in to acl2-devel until the release of ACL2 Version 6.5.

Quoting :doc note-6-5 (belatedly added now for the change committed in
acl2-devel svn revision 1360, which went with acl2-books svn revisions
2892-3):

  For ACL2(r), Ruben Gamboa found a bug in constraints for functions
  introduced with defun-std, and also kindly provided a fix, which
  has been incorporated.

Fixed a bug in the creation of *1* functions.  This bug was introduced
after Version 6.4 in the implementation of reducing the "rolling back"
of the logical world (see :doc note-6-5).  A comment in binding of
cl-compliant-p-optimization explains the bug and its fix.  Amazingly,
this bug survived many regressions and uses in industry; I found it
while attempting to certify some old books from Rockwell that I use
for testing just before each release.

Updated workshops.html with recent info.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1362 5d84a466-a78b-0930-a311-59b22171a541
NOTE: Unless I encounter unforeseen problems, this should be the last
check-in to acl2-devel until the release of ACL2 Version 6.5.
[Yeah, I know I said that just a few minutes ago....]

Incorporated small :doc fixes from books/system/doc/acl2-doc.lisp:

  Updated :doc real to avoid obsolete reference to nonstd-6.4.tar.gz.

  Updated :doc books-certification-alt to avoid mention of obsolete
  `make' target regression-nonstd.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1363 5d84a466-a78b-0930-a311-59b22171a541
Merge pull request #1 from acl2/master

ragerdl merging in kini's automerge