Rename bitops/sign-extend to bitops/fast-logext, to avoid incompatibility with
the RTL library (fixes issue 135).

Removed centaur/regression and centaur/tutorial stuff from centaur/doc, to
avoid depending on glucose and speed up building the manual.

Minor clarification to the defsection documentation.

Update issue 136

Renamed REPEAT in the std/lists library to REPLICATE.  (First step toward
resolving issue 136.)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2446 303c5b2c-9740-0410-b014-fd8f9db7be32
vl: stop gatesplit transform from complaining about unsupported gates, since it shouldn't care about them anyway

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2447 303c5b2c-9740-0410-b014-fd8f9db7be32
Rework oslib::getpid, formerly CCL-only, using the Common Lisp iolib library,
which may improve its portability.

Add some extremely basic tests of oslib::getpid, oslib::file-kind, and
oslib::date.

Add appropriate :parents for various VL lexer functions

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2448 303c5b2c-9740-0410-b014-fd8f9db7be32
Trivial doc fixes, and stop trying to certify gl/solutions.lisp to avoid
resource limitations on more modest platforms.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2449 303c5b2c-9740-0410-b014-fd8f9db7be32
Add new ccl-only cert-param for use with books like aig-sat-tests.lisp (requires tshell)

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2450 303c5b2c-9740-0410-b014-fd8f9db7be32
fix up some additional repeat issues to fix sbcl acl2(h) regression, but I don't understand why I wasn't seeing these as failures on CCL...

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2451 303c5b2c-9740-0410-b014-fd8f9db7be32

Quoting :doc note-6-5:

  The brr command, :wonp, had not been installed for use after :eval
  even though this was claimed in the documentation (see
  [brr-commands]). This has been fixed. Thanks to David Rager for
  bringing this issue to our attention.

The following feature was documented in note-6-5-books, but it seems
that cert.pl (technically, build/make_cert_help.pl) already handles
this, and Jared has pointed out that this change caused cleaning to
require that ACL2 is bound to an executable.  So I've reverted this
change (and removed this docuentation).

  Running the make command now causes an error if variable ACL2 is not
  bound to an executable.

Added a comment in GNUmakefile, warning about making "manual" with
another target when -j exceeds one.  (Perhaps "manual" should simply
be eliminated, but whoever does that should check carefully that it's
no longer referenced in documentation.)

Added centaur/doc.cert to "everything" target in GNUmakefile, with
this comment:

# Note: We add centaur/doc.cert explicitly, even though that might not
# be necessary, because at one point centaur/doc.cert was not
# otherwise made (something related to glucose).

Quoting :doc note-6-5-books:

  (File interface/emacs/inf-acl2.el) One now gets a clear error,
  suggesting a solution, when Emacs command meta-x run-acl2 cannot
  find an ACL2 executable. Thanks to Scott Staley for helpful
  correspondence leading to this fix.

Added introductory example to :doc iprint.

Improved pointers to web pages in ACL2 system documentation, taking
advantage of Jared's recent enhancement (svn revisions 2442 and 2445)
to display URLs from <a> tags even in text-rendered display.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2452 303c5b2c-9740-0410-b014-fd8f9db7be32