- STV to C++ compiler. (preliminary, probably buggy)

- VL update: subtle change to synthesis of ?: operators.  Previously, even
  for approx muxes we had a bizarre inconsistency, where
    X ? 0 : 0 was producing 0, but
    X ? 1 : 1 was producing X.
  To be more consistent and slightly more conservative, both versions will
  now produce X.  This change won't affect non-approx muxes.

- Removed unneeded legacy file books/certify-numbers.lsp (with Matt)



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

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2148 303c5b2c-9740-0410-b014-fd8f9db7be32
Installed a new version of models/jvm/m1/wormhole-abstraction.lisp
from J Moore, as he requested.

Executed the following command in cutil and milawa directories, to
help "svn status" give a cleaner report (see README-svn):

svn propset -R svn:ignore -F /projects/acl2/devel/books/unversioned-files.txt .


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2149 303c5b2c-9740-0410-b014-fd8f9db7be32
Attempt to revert milawa/ to svn revision 2148.  I had done the
default setting of ignore properties there (checked into svn rev 2149)
because "svn status" showed files that I expected not to be shown:

?                    milawa/doc.cert
?                    milawa/doc.lx64fsl
?                    milawa/doc.cert.out

But Jared informed me that he had done custom property setting for
milawa/.  I executed the following while standing in the milawa/
directory.

svn merge -r 2149:2148 .


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2151 303c5b2c-9740-0410-b014-fd8f9db7be32
Added these lines to centaur/esim/stv/stv2c/stv2c.lisp, avoiding
certification by ACL2 (but still allowing it for ACL2(h)):

; Added 10/17/2013 by Matt K.: Making this hons-only, because the proof of
; RETURN-TYPE-OF-STV2C-OUTPUT-STUFF-AUX seems to bog down in ACL2 as opposed to
; ACL2(h), perhaps because worse-than needs to be memoized.
; cert_param: (hons-only)


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2152 303c5b2c-9740-0410-b014-fd8f9db7be32
release aignet aiger file reader/writer

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2153 303c5b2c-9740-0410-b014-fd8f9db7be32
add outer-local book for creating events local to an external context

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2154 303c5b2c-9740-0410-b014-fd8f9db7be32
fix an outer-local bug

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2155 303c5b2c-9740-0410-b014-fd8f9db7be32
Mostly XDOC/STD updates

:XDOC now shows :FROM information and prints parents more nicely.
(fixes issue 108)

XDOC::SAVE now prints a report about redefined topics that shows you where the
redefinition occurs.  It will cause errors (by default, but you can suppress
them by just adding :REDEF-OKP T) if topics are redefined.  (fixes issue 109)

Updated some books to fix problems shown by these new XDOC warnings.
Modernized a couple of VL books in the process.

Integrated xdoc::set-default-parents into std/util macros in a more sensible
way.  (fixes issue 65)

  - Previously macros like defprojection, deflist, defmapappend, defenum,
    defalist, and defaggregate ignored the default-parents, and just used
    (acl2::undocumented) if no parents were provided.  These macros now instead
    consult default-parents before falling back to (acl2::undocumented).  Also,
    :parents nil can now be used to defeat (acl2::undocumented).

  - Previously the define macro ignored default-parents.  It now uses the
    defaults when no explicit :parents are provided.

Fix svn:ignores on top-level milawa directory, which previously had no books.

FWIW I never notice these svn:ignore problems because my ~/.subversion/config
has a line like this:
  global-ignores = *.cert *.cert.out ...
It seems easier to do this in our global configs than to have to remember
to deal with it every time we add another directory.

Update issue 66

After some deliberation, I decided NOT to have define automatically insert
:parents (acl2::undocumented), mainly because doing it the other way led to
many conflicts with XDOC's new anti-redefinition feature.



git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2156 303c5b2c-9740-0410-b014-fd8f9db7be32
fix bug with define-tests

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2157 303c5b2c-9740-0410-b014-fd8f9db7be32
test commit, please ignore

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

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2159 303c5b2c-9740-0410-b014-fd8f9db7be32
cert.pl: don't output reloc stub info when --quiet

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2160 303c5b2c-9740-0410-b014-fd8f9db7be32
Fixed a guard violation in workshops/2004/sumners-ray/support/invp.lsp.

Updated system/pseudo-good-worldp.lisp for acl2-devel soundness bug
fix that is about to be checked in.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2163 303c5b2c-9740-0410-b014-fd8f9db7be32
Added workaround for apparent bug in a :program mode function defined in clause-processors/SULFA/books/sat/local-clause-simp.lisp, which was exposed by the bug fix checked into acl2-devel svn revision 1127.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2164 303c5b2c-9740-0410-b014-fd8f9db7be32
Added support for moving the ACL2 system documentation into the XDOC
system.
**NOTE**: Please do not yet edit these files unless you're me or
          Jared!  I plan to send an announcement about all this soon.

The above support is provided by the new system/doc/ directory, which
contains files written by Jared Davis that were updated by both him
and me.  See system/doc/README.

Note that svn revision 2166 of books/xdoc/preprocess.lisp from the
jared/ branch has not yet been committed to the trunk, as Jared asked
me to wait to do that.  (However, I used the updated preprocess.lisp
to create new ACL2 source file doc.lisp.)

A separate check-in to acl2-devel will provide additional support for
moving the ACL2 system documentation into the XDOC fold.

Very minor note: In creating system/doc/acl2-doc.lisp, certification
of export-acl2doc.lisp created "hard symbol to link nicely" messages
in export-acl2doc.cert.out for the following preprocessor directives.
We might or might not want to fix these manually at some point.  I
looked at the acl2-pc::macro-command topic and found three such links,
all of which worked, so this seems like a very low priority cosmetic
issue.

  @(url ACL2-PC::UNDO)
  @(url ACL2-PC::COMM)
  @(url ACL2-PC::COMMANDS)
  @(url ACL2-PC::FORWARDCHAIN)
  @(url ACL2-PC::RETRIEVE)
  @(url ACL2-PC::UNSAVE)
  @(url ACL2-PC::SAVE)


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2168 303c5b2c-9740-0410-b014-fd8f9db7be32
gl: add optimized symbolic subtraction, logeqv

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2173 303c5b2c-9740-0410-b014-fd8f9db7be32
Actually do the merge correctly...?

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

std/util:
 - Add /// support to deflist and defprojection
 - Use with-output to reduce output from deflist and defprojection
 - Tweak defenum to avoid dependency on deflist

xdoc:
 - Add basic books release-notes topic (not yet integrated into centaur/doc)
 - Tweak fancy viewer to warn Safari users about lack of proper history.state
   api support.

Minor tweaks to .gitignore files

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2178 303c5b2c-9740-0410-b014-fd8f9db7be32
Avoid accidental, futile attempt to certify rendered-doc.lisp, by
calling it rendered-doc.lsp instead.

Updated documentation for NOTE-6-4 and DOCUMENTATION.  The latter may
be improved in the future.

Modified system/doc/render-doc.lisp so that its output file,
system/doc/rendered-doc.lsp, would be printed in the ACL2 package.
(Avoiding package prefixes can be helpful for writing Emacs tools to
browse that output file.)


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