VL (with Jared): add scopestack abstraction for looking up various kinds of things, and use that in various transforms
Merge branch 'master' into scopestack
vl -- porting more transforms to use scopestacks
Fixed a bug in oracle-apply-raw.
Merge pull request #234 from ragerdl/master

Some changes from the weekend
Update to bin/make-fancy-manual.sh incorporates Rager's script for generating HTML (for search engines).
add test/demo of sharedlibs relocation code
VL parser and UDP updates.

Parser change: all parsers now produce vl-warning-p objects when we need to
cause a real parse error.  (Previously it was an ad-hoc msg object.)

Initial implementation of user-defined primitives:
  - Parses Verilog-2005 style UDPs (sequential and combinational)
  - Transform that handles very basic combinational UDPs
    (and converts all UDPs into modules)
  - Basic systest for some combinational UDPs

Notes and caveats:
  - We don't at all handle sequential UDPs.
  - This is a bit more permissive than it should be, e.g., we don't
    properly reject UDPs with conflicting lines.
  - I haven't looked at SystemVerilog extensions yet
scopestack work
add function for flattening a design into its descriptions
vl: comment injection tweak to avoid duplicating comments in multiply included files.
fix apparent package problem with arith-equiv-defs book
more work on scopestacks
fix up a few remaining things broken by scopestack stuff
Improve cert.pl support for provisional certification in the presence
of other, non-provisionally-certified files.  In books/GNUMakefile,
remove the special cases for the two directories that use it.
Move a set-inhibit-warnings form from the top of doc.lisp into doc.acl2, allowing it to certify faster by skipping most of the second pass.
fix more breakage
VL: Add tools for looking up variables, definitions, etc. in nested
namespaces (mlib/scopestack.lisp).  Change some existing transforms to
use them.
Added :doc git-quick-start.  Updated :doc community-books for github.  Added static-hons support for GCL.  Use compiled memoized functions during include-book.  For Lisps that don't always compile, memoize only compiles when existing function is compiled.

:Doc note-7-0 has a link to new topic git-quick-start, and also says:

  Static honsing for ACL2(h), an efficiency enhancement formerly only
  available for CCL, is now incorporated into builds on sufficiently
  recent GCL versions.

  ACL2(h) could fail to use previously-compiled definitions for
  [memoize]d functions when [include-book] is invoked. This has been
  fixed.

  (For ACL2(h), and irrelevant for CCL and SBCL) Calls of [memoize]
  only compile the memoized definition when the original function is
  compiled, rather than unconditionally as before.

Also fixed a small bug in :doc note-7-0: @(tsee pbt!) should have been
@(tsee pcb!), and now it is.

NOTE regarding the new :doc topic, git-quick-start, in
books/system/doc/acl2-doc.lisp: I suspect that the pairs of
fetch/merge commands can be replaced by a suitable pull command.  If
anyone is SURE about that, I hope that person will make that change.
Merge remote-tracking branch 'remotes/origin/master'