[acl2/acl2] 58ec95: Make b* stricter; inline support for FUN binders

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 58ec95efdf15d2836aca2ee173f231d24939cdac
https://github.com/acl2/acl2/commit/58ec95efdf15d2836aca2ee173f231d24939cdac
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-10-09 (Fri, 09 Oct 2015)

Changed paths:
M books/std/util/bstar.lisp

Log Message:
-----------
Make b* stricter; inline support for FUN binders

B* will now require that variables be bound to a form, e.g.,
it will no longer accept:

(b* ((x)) x)

B* will no longer treat T and NIL as aliases for & forms.
That is, previously the following were all equivalent:

(b* ((& (cw "Hello"))) t)
(b* ((t (cw "Hello"))) t)
(b* ((nil (cw "Hello"))) t)

The special & form is still allowed, but the NIL/T variants
are no longer allowed as they were rather obscure.

B* will now produce nicer error messages, instead of guard
violations, on forms such as:

(b* ((1 2)) 3)
(b* ((x . 5)) x)

The syntax for FUN binders has also been extended to allow
inline/notinline declarations on the resulting FLET forms, e.g.,
whereas before you could only write:

(b* (((fun (add a b)) (+ a b)))
(add 3 4))

You can now additionally write:

(b* (((fun inline (add a b)) (+ a b)))
(add 3 4))

(b* (((fun notinline (add a b)) (+ a b)))
(add 3 4))

Also, some b*/patbind-related functions now have verified
guards.


Commit: 30176d86db0792ad36423379ff1698a5748e39e2
https://github.com/acl2/acl2/commit/30176d86db0792ad36423379ff1698a5748e39e2
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-10-09 (Fri, 09 Oct 2015)

Changed paths:
M books/build/cert.pl
M books/build/make_cert_help.pl

Log Message:
-----------
Add cert.pl option for showing hostnames

This adds an CERT_PL_SHOW_HOSTNAME environment variable that you can
set if you want to show the hostname after each book gets certified.

Leaving it off by default because it's probably only useful at Centaur
and it adds a (probably trivial) amount of file IO overhead.


Commit: 325d157ac986e89a4e642a1d7bba2483029025fd
https://github.com/acl2/acl2/commit/325d157ac986e89a4e642a1d7bba2483029025fd
Author: Jared C. Davis <jared....@gmail.com>
Date: 2015-10-09 (Fri, 09 Oct 2015)

Changed paths:
M books/centaur/bitops/ihsext-basics.lisp
M books/centaur/bitops/integer-length.lisp
M books/centaur/misc/bound-rewriter.lisp
A books/projects/cache-coherence/german-protocol/ccp.m
A books/projects/cache-coherence/german-protocol/german.lisp
A books/projects/cache-coherence/vi/utils.lisp
A books/projects/cache-coherence/vi/vi-correct.lisp
A books/projects/cache-coherence/vi/vi-impl.lisp
R books/projects/cache-coherency/vi/utils.lisp
R books/projects/cache-coherency/vi/vi-correct.lisp
R books/projects/cache-coherency/vi/vi-impl.lisp
R books/projects/concurrent-programs/german-protocol/ccp.m
R books/projects/concurrent-programs/german-protocol/german.lisp
M books/workshops/2015/README

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master'


Compare: https://github.com/acl2/acl2/compare/3e5c449b916f...325d157ac986

[GitHub]

Branch: refs/heads/testing