[acl2/acl2] 4a7f28: [FTY] Improve some proofs generated by `deffold-map`.

[Alessandro Coglio]

Branch: refs/heads/deffold-map
Home: https://github.com/acl2/acl2
Commit: 4a7f2885a205e950d7f65a4499903a3f6194f3e5
https://github.com/acl2/acl2/commit/4a7f2885a205e950d7f65a4499903a3f6194f3e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[FTY] Improve some proofs generated by `deffold-map`.

Enable some functions in the termination proofs, making the proof more robust
and self-contained. The same change has been made to `fty::deffold-reduce`
already.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Home: https://github.com/acl2/acl2
Commit: 4a7f2885a205e950d7f65a4499903a3f6194f3e5
https://github.com/acl2/acl2/commit/4a7f2885a205e950d7f65a4499903a3f6194f3e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[FTY] Improve some proofs generated by `deffold-map`.

Enable some functions in the termination proofs, making the proof more robust
and self-contained. The same change has been made to `fty::deffold-reduce`
already.

Commit: 314cf49f1495a1048777c7cb531b55a7575a2edf
https://github.com/acl2/acl2/commit/314cf49f1495a1048777c7cb531b55a7575a2edf

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:

M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

Log Message:
-----------
Merge.


Commit: 4618d9ecfbd85f757e4b7cdeec87c0d1eb107b4f
https://github.com/acl2/acl2/commit/4618d9ecfbd85f757e4b7cdeec87c0d1eb107b4f
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-03-18 (Wed, 18 Mar 2026)

Changed paths:
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------

Merge pull request #1920 from acl2/deffold-map

Improvements to `deffold-map`-generated proofs.


Compare: https://github.com/acl2/acl2/compare/9dbffa503d54...4618d9ecfbd8

[acl2buildserver]

Branch: refs/heads/master

Commit: f55950d3abe4e2273d1e96fb663bf18d19457808
https://github.com/acl2/acl2/commit/f55950d3abe4e2273d1e96fb663bf18d19457808
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-18 (Wed, 18 Mar 2026)

Changed paths:
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------

Merge commit '4618d9ecfbd85f757e4b7cdeec87c0d1eb107b4f' into HEAD


Compare: https://github.com/acl2/acl2/compare/d8a170136e14...f55950d3abe4

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: d3703430885ee64df5d0eca0b837bdc6c7e74e65
https://github.com/acl2/acl2/commit/d3703430885ee64df5d0eca0b837bdc6c7e74e65
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M books/GNUmakefile

Log Message:
-----------
[books/GNUmakefile] Add blake2s proof to SLOW_BOOKS.

As suggested by Matt Kaufmann.


Commit: 74df1daae0ae88dfddb265864936affdd34e41d1
https://github.com/acl2/acl2/commit/74df1daae0ae88dfddb265864936affdd34e41d1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M books/kestrel/bibtex/xdoc-generation.lisp

Log Message:
-----------
[bibtex] Improve xdoc generated for bibtex.

Include a link to access the paper via doi.org if a DOI is present.


Commit: 0d9e5f5885ae8c546c9ea49d950f522a039640cc
https://github.com/acl2/acl2/commit/0d9e5f5885ae8c546c9ea49d950f522a039640cc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[doc] Finish adding my release notes for v8-7.


Commit: b3e0ef9bc0e3adfce2fa20d976bf8ee738094a16
https://github.com/acl2/acl2/commit/b3e0ef9bc0e3adfce2fa20d976bf8ee738094a16
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[doc] Alphabetize relnotes.

Also make a couple of tweaks.


Commit: 701acd698099b047e012cb9ce03afec2990e56a8
https://github.com/acl2/acl2/commit/701acd698099b047e012cb9ce03afec2990e56a8

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M books/GNUmakefile
M books/doc/relnotes.lisp
M books/kestrel/bibtex/xdoc-generation.lisp

Log Message:
-----------
Merge commit 'b3e0ef9bc0e3adfce2fa20d976bf8ee738094a16' into HEAD


Commit: 36851786c69a1b36d7c5bec8ee59b1eb4d550eac
https://github.com/acl2/acl2/commit/36851786c69a1b36d7c5bec8ee59b1eb4d550eac
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M acl2.lisp

Log Message:
-----------
This is a dummy commit, to mark the starting point for releasing the next version (ACL2 8.7).


Commit: 07c0959aece490ced6ff00a13cc9d4425cffb805
https://github.com/acl2/acl2/commit/07c0959aece490ced6ff00a13cc9d4425cffb805
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M acl2.lisp
M books/GNUmakefile
M books/doc/relnotes.lisp
M books/kestrel/bibtex/xdoc-generation.lisp

M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------

Merge.


Commit: ae717e8f83805b4d619d4ad98ee92af45dcad32b
https://github.com/acl2/acl2/commit/ae717e8f83805b4d619d4ad98ee92af45dcad32b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Fix XDOC link.


Compare: https://github.com/acl2/acl2/compare/7bab5d1cbb16...ae717e8f8380