VL updates for better linting

  - Put *vl-ops-table* behind a disabled function and fix fallout
  - Slightly rework fussy size warnings to better show the two
    disagreeing sizes
  - Extend origexprs to more of the parse tree
vl: various tweaks to improve linting
Merge linting changes
Adding some references to std::strict-list-recognizers and documenting append-without-guard (and adding a reference to it from append).
fix up botched expr-size commit
Merge remote-tracking branch 'remotes/origin/master'
vl linter tweak to blank arg warning
Sped ACL2(h) up a bit by eliminating a special variable.

Quoting a comment in (defvar *aokp* ...):

; Before Version_7.0, *aokp* was Boolean and a separate special variable,
; *attached-fn-called*, was used for holding a function symbol whose
; attachement has been called.  By folding that role into *aokp* we reduced the
; time for (defthm spec-body ...) in
; books/misc/misc2/reverse-by-separation.lisp from 188 seconds to 181 seconds,
; a savings of about 4%.

I might add a corresponding item to :doc note-7-0 after I get a bit
more data about the speed-up from this change.
Minor vl-lint bugfixes

  - We were eliminating unused variables before argresolve, which could lead us
    to not realize that a variable was used in SystemVerilog .*- and .foo-style
    port connections.  This could cause spurious and confusing warnings about
    .* style connections that appeared to be missing variables.

  - Clean up new blank arg warning.  It had been printing the raw port
    structure, which was ugly.
Added Codewalker as requested by J Moore.  Also, updated some documentation.

Quoting :doc note-7-0-books:

  The new projects/codewalker/ directory contains Codewalker, a utility
  for exploring code in any programming language specified by an ACL2
  model to discover certain properties of the code. Demos of
  Codewalker are also in that directory.

Added this to :doc note-7-0 for preceding commit/push:

  We made a low-level implementation tweak that resulted in a speed-up
  of 2.6% in wall-clock time for a CCL-based regression (using
  ``make'' with -j 8 and target ``everything''). (Technical note: We
  eliminated the Lisp special variable *attached-fn-called*, using
  another variable *aokp* instead. Special variable bindings can
  apparently be expensive!)

Also, fixed recent mod to :doc coerce, thanks in part to feedback from
J.
vl: major speedups to a couple of lint transforms

The new vl-context stuff was, in some cases, extremely expensive, so this is
just some reworking things to avoid that expensive.  Also sped up duplicate
expression checking in the leftright check.
Minor vl-lint bugfixes

  - We were eliminating unused variables before argresolve, which could lead us
    to not realize that a variable was used in SystemVerilog .*- and .foo-style
    port connections.  This could cause spurious and confusing warnings about
    .* style connections that appeared to be missing variables.

  - Clean up new blank arg warning.  It had been printing the raw port
    structure, which was ugly.
Merge remote-tracking branch 'remotes/xb/master'
Removed unadvertised ACL2(h)-only declare forms dynamic-extent, inline, and notinline.

Quoting :doc note-7-0:

  We removed support for three [declare] forms that had been permitted
  in ACL2(h) only, but were not advertised: dynamic-extent, inline
  and notinline, because they seem difficult or impossible to support
  correctly. For alternatives to using inline and notinline
  declarations, see [defun-inline] and [defun-notinline].
typo in arithmetic/natp-posp.lisp
Merge pull request #320 from nadezhin/master

typo in arithmetic/natp-posp.lisp

Thanks for the fix and pull-request Dmitry!
Fixed typo found by Bob Boyer.
Merge remote-tracking branch 'remotes/origin/master'
Removed support for the nu-rewriter.  Fixed watch-raw.lsp as per suggestions from Bob Boyer.  Minor updates to installation instructions, :doc memoize, home page, and default-state-vars, for ACL2(h) conversion.

Quoting :doc note-7-0:

  The nu-rewriter contained special provisions for rewriting
  expressions composed of [nth], [update-nth], and
  [update-nth-array], together with [let] expressions and other
  applications of non-recursive functions or [lambda] expressions. An
  email query was sent to the acl2 mailing list on 10/24/2014, giving
  people an opportunity to object to the removal of this feature.
  Nobody objected, so we have removed it in order to simplify the
  ACL2 code base. Thanks to David Rager for suggesting this sort of
  code clean-up. Note that some system functions, for example
  all-equal, have been deleted in support of this change.

Quoting :doc note-7-0-books:

  The watch utility works again. Thanks to Bob Boyer for providing
  fixes. To use this utility:

    (include-book "centaur/memoize/old/watch" :dir :system :ttags :all)
    :q
    (watch)
    (lp)
    ; Now in Emacs, bring into a buffer the file reported by (watch), whose
    ; name is of the form watch-output-temp-n.lsp.  Then execute ACL2 forms.
Synched doc.lisp