[acl2/acl2] 7771ae: [C$] Improve a fixtype field name.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 7771ae15a4a4f8ea45e467e348df9c9a2d0809a5
https://github.com/acl2/acl2/commit/7771ae15a4a4f8ea45e467e348df9c9a2d0809a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Improve a fixtype field name.


Commit: 7606afe535a235d3e88ca8ceb9a26718173aa7b5
https://github.com/acl2/acl2/commit/7606afe535a235d3e88ca8ceb9a26718173aa7b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Extend information about a function-like macro.

Although this is redundant information, it seems better to compute it once.


Commit: c9fc77dc245c121cad7dc1e58312fcb3f3279d13
https://github.com/acl2/acl2/commit/c9fc77dc245c121cad7dc1e58312fcb3f3279d13
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Add a predicate on preprocessing lexemes.


Commit: 7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
https://github.com/acl2/acl2/commit/7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp

Log Message:
-----------
Updated hol-in-acl2 library with help from Konrad Slind. Added eval-events-from-file.

The hol-in-acl2 library is a bit cleaner now, in particular with the
addition of new utility zf::import-theory and files *.defhol generated
(by Konrad) using the hol-to-acl2 translator. Also added a new
utility; see :DOC eval-events-from-file.


Commit: f270dfb641705d84634069832cd119a99fe2796c
https://github.com/acl2/acl2/commit/f270dfb641705d84634069832cd119a99fe2796c
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp

Log Message:
-----------
Fixed mix-up with depends-on directives


Commit: 78d52469f0fa82ff1423a404011e2b693d9ac73b
https://github.com/acl2/acl2/commit/78d52469f0fa82ff1423a404011e2b693d9ac73b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

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

Log Message:
-----------
[C$] Add two theorems.


Commit: 644995e8dde2736cfe781c94f8b8b480b382b7e3
https://github.com/acl2/acl2/commit/644995e8dde2736cfe781c94f8b8b480b382b7e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Add a predicate on lexemes.


Commit: debe7806338f2b23d2e29aac10e906bf47588692
https://github.com/acl2/acl2/commit/debe7806338f2b23d2e29aac10e906bf47588692
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Add support for `#define` directives.

Only for preprocessing the directives themselves for now; still need to add
support for expanding them where/as needed.


Commit: f432338656d9f2d64efdc9039b34827d06029f5f
https://github.com/acl2/acl2/commit/f432338656d9f2d64efdc9039b34827d06029f5f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add and use specialized testing macro.


Commit: 481aea193f3472396875dfc9e71b520bd0f42e92
https://github.com/acl2/acl2/commit/481aea193f3472396875dfc9e71b520bd0f42e92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.3.c
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.4.c
A books/kestrel/c/syntax/tests/c17-std-example1-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example2-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example3-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example4-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example6-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example7-6.10.3.5.c
A books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add several tests for `#define`.


Commit: 3e153beb24051b99ad3aad8897cd52d3d7830ff1
https://github.com/acl2/acl2/commit/3e153beb24051b99ad3aad8897cd52d3d7830ff1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/e3d6f158d68d...3e153beb2405

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

[Alessandro Coglio]

Branch: refs/heads/master

Compare: https://github.com/acl2/acl2/compare/f270dfb64170...3e153beb2405

[Alessandro Coglio]

Branch: refs/heads/testing