[acl2/acl2] bea3e3: Fixed type declaration bug showing up at safety 3 ...
0 views
Skip to first unread message
MattKaufmann
Jan 8, 2026, 7:47:26 AM (13 days ago) Jan 8
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: bea3e3de6509a5611d05119dd72578ed23eda22e
https://github.com/acl2/acl2/commit/bea3e3de6509a5611d05119dd72578ed23eda22e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Fixed type declaration bug showing up at safety 3 with SBCL in books/misc/hidden-defpkg-checks/.
We fixed a low-level bug in [include-book], which we have only
observed using ACL2 built on host Lisp SBCL with safety 3 (an
optimization setting that causes more runtime checks at the cost of
longer run times). (Technical note: The bug was in bogus type
declarations in the definition of ACL2 source macro
with-hcomp-bindings.) Thanks to Jim White for reporting the bug.
This fix seems to permit Issue #1889 to be closed.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: bea3e3de6509a5611d05119dd72578ed23eda22e
https://github.com/acl2/acl2/commit/bea3e3de6509a5611d05119dd72578ed23eda22e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Fixed type declaration bug showing up at safety 3 with SBCL in books/misc/hidden-defpkg-checks/.
We fixed a low-level bug in [include-book], which we have only
observed using ACL2 built on host Lisp SBCL with safety 3 (an
optimization setting that causes more runtime checks at the cost of
longer run times). (Technical note: The bug was in bogus type
declarations in the definition of ACL2 source macro
with-hcomp-bindings.) Thanks to Jim White for reporting the bug.
This fix seems to permit Issue #1889 to be closed.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
MattKaufmann
Jan 8, 2026, 7:48:38 AM (13 days ago) Jan 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Jan 8, 2026, 4:59:02 PM (12 days ago) Jan 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
https://github.com/acl2/acl2/commit/66830d3524f48d387eb87def75f9f751742fd85f
M books/projects/hol-in-acl2/acl2/hol.lisp
A books/projects/hol-in-acl2/acl2/type-match.lisp
M books/projects/hol-in-acl2/examples/eval-poly-acl2.lisp
Log Message:
-----------
Tweaks to hol-in-acl2
Commit: ccc44d49459510dbc2212e29168eadcc6cd6a671
https://github.com/acl2/acl2/commit/ccc44d49459510dbc2212e29168eadcc6cd6a671
M books/projects/set-theory/logic.txt
Log Message:
-----------
Tweaked note on logical foundations of ACL2(zfc) to make it slightly more accessible
Commit: 80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
https://github.com/acl2/acl2/commit/80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Remove outdated doc..
Commit: 4839122ead0a91179128d94a188d3346907b6bbd
https://github.com/acl2/acl2/commit/4839122ead0a91179128d94a188d3346907b6bbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Tweak book inclusion order.
Rationale: first include books from current or sibling library via relative
paths, then from other libraries via `:dir :system` paths, then local
inclusions, finally set the controlled configuraion.
Commit: d9dee1a1b36befa0d5a1e18eb7f8f45675424302
https://github.com/acl2/acl2/commit/d9dee1a1b36befa0d5a1e18eb7f8f45675424302
Author: Grant Jurgensen <gr...@jurgensen.dev>
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
[OMAP] Add from-alist and from-lists
Commit: a2683ab3150b87df607d5d874d1a1e8a01ea7854
https://github.com/acl2/acl2/commit/a2683ab3150b87df607d5d874d1a1e8a01ea7854
Author: ACL2 Build Server <acl2bui...@gmail.com>
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge commit 'd9dee1a1b36befa0d5a1e18eb7f8f45675424302' into HEAD
Commit: d1dd38b6f3503d5045faa127f192086fa327b241
https://github.com/acl2/acl2/commit/d1dd38b6f3503d5045faa127f192086fa327b241
Author: Alessandro Coglio <em...@alessandrocoglio.info>
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge.
Commit: dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
https://github.com/acl2/acl2/commit/dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Add support for GCC statement attributes.
Compare: https://github.com/acl2/acl2/compare/6ed575ca1c36...dd62b342b8ac
Home: https://github.com/acl2/acl2
Commit: bea3e3de6509a5611d05119dd72578ed23eda22e
https://github.com/acl2/acl2/commit/bea3e3de6509a5611d05119dd72578ed23eda22e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Fixed type declaration bug showing up at safety 3 with SBCL in books/misc/hidden-defpkg-checks/.
We fixed a low-level bug in [include-book], which we have only
observed using ACL2 built on host Lisp SBCL with safety 3 (an
optimization setting that causes more runtime checks at the cost of
longer run times). (Technical note: The bug was in bogus type
declarations in the definition of ACL2 source macro
with-hcomp-bindings.) Thanks to Jim White for reporting the bug.
This fix seems to permit Issue #1889 to be closed.
Commit: 66830d3524f48d387eb87def75f9f751742fd85f
Commit: bea3e3de6509a5611d05119dd72578ed23eda22e
https://github.com/acl2/acl2/commit/bea3e3de6509a5611d05119dd72578ed23eda22e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Fixed type declaration bug showing up at safety 3 with SBCL in books/misc/hidden-defpkg-checks/.
We fixed a low-level bug in [include-book], which we have only
observed using ACL2 built on host Lisp SBCL with safety 3 (an
optimization setting that causes more runtime checks at the cost of
longer run times). (Technical note: The bug was in bogus type
declarations in the definition of ACL2 source macro
with-hcomp-bindings.) Thanks to Jim White for reporting the bug.
This fix seems to permit Issue #1889 to be closed.
https://github.com/acl2/acl2/commit/66830d3524f48d387eb87def75f9f751742fd85f
M books/projects/hol-in-acl2/acl2/hol.lisp
A books/projects/hol-in-acl2/acl2/type-match.lisp
M books/projects/hol-in-acl2/examples/eval-poly-acl2.lisp
Log Message:
-----------
Tweaks to hol-in-acl2
Commit: ccc44d49459510dbc2212e29168eadcc6cd6a671
https://github.com/acl2/acl2/commit/ccc44d49459510dbc2212e29168eadcc6cd6a671
M books/projects/set-theory/logic.txt
Log Message:
-----------
Tweaked note on logical foundations of ACL2(zfc) to make it slightly more accessible
Commit: 80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
https://github.com/acl2/acl2/commit/80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Changed paths:
Log Message:
-----------
[C$] Remove outdated doc..
Commit: 4839122ead0a91179128d94a188d3346907b6bbd
https://github.com/acl2/acl2/commit/4839122ead0a91179128d94a188d3346907b6bbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Changed paths:
Log Message:
-----------
[C$] Tweak book inclusion order.
Rationale: first include books from current or sibling library via relative
paths, then from other libraries via `:dir :system` paths, then local
inclusions, finally set the controlled configuraion.
Commit: d9dee1a1b36befa0d5a1e18eb7f8f45675424302
https://github.com/acl2/acl2/commit/d9dee1a1b36befa0d5a1e18eb7f8f45675424302
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
A books/std/omaps/from-alist.lisp
Changed paths:
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
[OMAP] Add from-alist and from-lists
Commit: a2683ab3150b87df607d5d874d1a1e8a01ea7854
https://github.com/acl2/acl2/commit/a2683ab3150b87df607d5d874d1a1e8a01ea7854
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
A books/std/omaps/from-alist.lisp
Changed paths:
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge commit 'd9dee1a1b36befa0d5a1e18eb7f8f45675424302' into HEAD
Commit: d1dd38b6f3503d5045faa127f192086fa327b241
https://github.com/acl2/acl2/commit/d1dd38b6f3503d5045faa127f192086fa327b241
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
A books/std/omaps/from-alist.lisp
Changed paths:
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge.
Commit: dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
https://github.com/acl2/acl2/commit/dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Add support for GCC statement attributes.
Compare: https://github.com/acl2/acl2/compare/6ed575ca1c36...dd62b342b8ac
acl2buildserver
Jan 8, 2026, 10:09:52 PM (12 days ago) Jan 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
https://github.com/acl2/acl2/commit/4a97222418b3043b09e492a70568f601c37015ad
Author: Eric Smith <ews...@gmail.com>
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
Log Message:
-----------
[build] Add MAKEACL2OPTS option to Jenkins scripts.
Unlike MAKEOPTS, which only applies to books, MAKEACL2OPTS applies to building ACL2 itself.
Commit: f4be7f84b31222b67c4dddd52dcbecf8de5497c8
https://github.com/acl2/acl2/commit/f4be7f84b31222b67c4dddd52dcbecf8de5497c8
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[build] Try to fix syntax.
Commit: 4de378350400f7c7487feaf747168458f3846771
https://github.com/acl2/acl2/commit/4de378350400f7c7487feaf747168458f3846771
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[build] Fix tabs in Jenkins Makefile.
Commit: 7d791aa11c28256665c140249f9d70417e01c212
https://github.com/acl2/acl2/commit/7d791aa11c28256665c140249f9d70417e01c212
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[build] Fix printing in Jenkins Makefile.
Commit: 761ed1a5c96dc6be103beedb499d282be5f9d9bf
https://github.com/acl2/acl2/commit/761ed1a5c96dc6be103beedb499d282be5f9d9bf
M books/doc/publications.lisp
Log Message:
-----------
Updated URL for book by Russinoff, as he requested
Commit: db1d5d66264ad0cab20610f1c9cfb55d8099cf99
https://github.com/acl2/acl2/commit/db1d5d66264ad0cab20610f1c9cfb55d8099cf99
Author: Eric Smith <ews...@gmail.com>
M books/build/jenkins/build-single.sh
Log Message:
-----------
[build] Add some documentation.
This was suggested by a comment in Matt Kaufmann's review of the PR.
Commit: 89078791d2e9aad30f76fb85b7244a303c36b5f2
https://github.com/acl2/acl2/commit/89078791d2e9aad30f76fb85b7244a303c36b5f2
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
Log Message:
-----------
Merge pull request #1892 from acl2/jenkins-makeacl2opts
Add option in Jenkins scripts to pass make options for ACL2 itself
Commit: b4df8fad9fe1baa75bc692334b13517c9e4b9558
https://github.com/acl2/acl2/commit/b4df8fad9fe1baa75bc692334b13517c9e4b9558
M books/projects/dpss/Base/events.lisp
Log Message:
-----------
Fixed typo.
This typo was found in an SBCL-based safety-3 run. Thanks to Eric
Smith for setting up leeroy to run tests with safety 3. The typo
was "delare" instead of "declare" here:
(def::und smallest-impending-dt-index (ens)
(delare (xargs :fty ((uav-list) uav-id)))
...)
Apparently the def::und macro could be improved by doing more checking.
Commit: d0bab51550952c3048df522936c05a2a5fb67b38
https://github.com/acl2/acl2/commit/d0bab51550952c3048df522936c05a2a5fb67b38
Compare: https://github.com/acl2/acl2/compare/d9dee1a1b36b...d0bab5155095
Commit: a2683ab3150b87df607d5d874d1a1e8a01ea7854
https://github.com/acl2/acl2/commit/a2683ab3150b87df607d5d874d1a1e8a01ea7854
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge commit 'd9dee1a1b36befa0d5a1e18eb7f8f45675424302' into HEAD
Commit: 4a97222418b3043b09e492a70568f601c37015ad
https://github.com/acl2/acl2/commit/a2683ab3150b87df607d5d874d1a1e8a01ea7854
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp
Log Message:
-----------
Merge commit 'd9dee1a1b36befa0d5a1e18eb7f8f45675424302' into HEAD
https://github.com/acl2/acl2/commit/4a97222418b3043b09e492a70568f601c37015ad
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/Makefile
Changed paths:
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
Log Message:
-----------
[build] Add MAKEACL2OPTS option to Jenkins scripts.
Unlike MAKEOPTS, which only applies to books, MAKEACL2OPTS applies to building ACL2 itself.
Commit: f4be7f84b31222b67c4dddd52dcbecf8de5497c8
https://github.com/acl2/acl2/commit/f4be7f84b31222b67c4dddd52dcbecf8de5497c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/Makefile
Changed paths:
Log Message:
-----------
[build] Try to fix syntax.
Commit: 4de378350400f7c7487feaf747168458f3846771
https://github.com/acl2/acl2/commit/4de378350400f7c7487feaf747168458f3846771
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/Makefile
Changed paths:
Log Message:
-----------
[build] Fix tabs in Jenkins Makefile.
Commit: 7d791aa11c28256665c140249f9d70417e01c212
https://github.com/acl2/acl2/commit/7d791aa11c28256665c140249f9d70417e01c212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/Makefile
Changed paths:
Log Message:
-----------
[build] Fix printing in Jenkins Makefile.
https://github.com/acl2/acl2/commit/761ed1a5c96dc6be103beedb499d282be5f9d9bf
M books/doc/publications.lisp
Log Message:
-----------
Updated URL for book by Russinoff, as he requested
Commit: db1d5d66264ad0cab20610f1c9cfb55d8099cf99
https://github.com/acl2/acl2/commit/db1d5d66264ad0cab20610f1c9cfb55d8099cf99
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/build-multi.sh
Changed paths:
M books/build/jenkins/build-single.sh
Log Message:
-----------
[build] Add some documentation.
This was suggested by a comment in Matt Kaufmann's review of the PR.
Commit: 89078791d2e9aad30f76fb85b7244a303c36b5f2
https://github.com/acl2/acl2/commit/89078791d2e9aad30f76fb85b7244a303c36b5f2
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/build/jenkins/Makefile
Changed paths:
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
Log Message:
-----------
Merge pull request #1892 from acl2/jenkins-makeacl2opts
Add option in Jenkins scripts to pass make options for ACL2 itself
Commit: b4df8fad9fe1baa75bc692334b13517c9e4b9558
https://github.com/acl2/acl2/commit/b4df8fad9fe1baa75bc692334b13517c9e4b9558
M books/projects/dpss/Base/events.lisp
Log Message:
-----------
Fixed typo.
This typo was found in an SBCL-based safety-3 run. Thanks to Eric
Smith for setting up leeroy to run tests with safety 3. The typo
was "delare" instead of "declare" here:
(def::und smallest-impending-dt-index (ens)
(delare (xargs :fty ((uav-list) uav-id)))
...)
Apparently the def::und macro could be improved by doing more checking.
Commit: d0bab51550952c3048df522936c05a2a5fb67b38
https://github.com/acl2/acl2/commit/d0bab51550952c3048df522936c05a2a5fb67b38
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
Merge commit 'dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce' into HEAD
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
Compare: https://github.com/acl2/acl2/compare/d9dee1a1b36b...d0bab5155095
Reply all
Reply to author
Forward
0 new messages