[acl2/acl2] aa9411: Add-macro-alias, add-macro-fn, and add-binop now s...
0 views
Skip to first unread message
MattKaufmann
Dec 14, 2025, 10:05:45 PM (2 days ago) Dec 14
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: aa941139c049fcf178691ddfcdf52c2a0ab246db
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Add-macro-alias, add-macro-fn, and add-binop now support a second argument that is a macro-alias. :Trans* uses the :TERM evisc-tuple when printing; clarified :DOC accordingly in :DOC for :trans* and also :trans. Deref-macro-name is now more directly a :logic mode function (doesn't use system-verify-guards mechanism). Removed a confusing comment in (set-table-guard macro-aliases-table ...).
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: aa941139c049fcf178691ddfcdf52c2a0ab246db
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Add-macro-alias, add-macro-fn, and add-binop now support a second argument that is a macro-alias. :Trans* uses the :TERM evisc-tuple when printing; clarified :DOC accordingly in :DOC for :trans* and also :trans. Deref-macro-name is now more directly a :logic mode function (doesn't use system-verify-guards mechanism). Removed a confusing comment in (set-table-guard macro-aliases-table ...).
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
acl2buildserver
Dec 14, 2025, 10:06:41 PM (2 days ago) Dec 14
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages