[acl2/acl2] 41e5c7: [C$] Add infer-ienv

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 41e5c716af802899acb988366283180cfb4bc353
https://github.com/acl2/acl2/commit/41e5c716af802899acb988366283180cfb4bc353
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/ienv.c
A books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Add infer-ienv

This utility will create an implementation environment object by running
a test C program and interpreting the results.


Commit: 6eb82dba7a189bb8ef3d33029ecddcce968d228d
https://github.com/acl2/acl2/commit/6eb82dba7a189bb8ef3d33029ecddcce968d228d
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-12-22 (Mon, 22 Dec 2025)

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

Log Message:
-----------
[std] Add :long option to defirrelevant


Commit: 8f3082738bde2ae29b12516dbeb1712ffd8b63b4
https://github.com/acl2/acl2/commit/8f3082738bde2ae29b12516dbeb1712ffd8b63b4
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/code-ensembles.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/tests/input-files.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp

Log Message:
-----------
[C$] Replace input-files options with :ienv

This also distinguishes between irr-ienv, and ienv-default. Thanks to
Alessandro Coglio for discussion which led to this change.


Commit: c8149adc49d0a84daa0d9314abe1005785481bce
https://github.com/acl2/acl2/commit/c8149adc49d0a84daa0d9314abe1005785481bce
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/infer-ienv.lisp

Log Message:
-----------
[C$] Replace make-event with extend-pathname


Compare: https://github.com/acl2/acl2/compare/cc1a20aedb40...c8149adc49d0

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

[Alessandro Coglio]

Branch: refs/heads/master

Commit: 26f5e2a3cc9599f1e4f7167451b96ae183ee48bb
https://github.com/acl2/acl2/commit/26f5e2a3cc9599f1e4f7167451b96ae183ee48bb

Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:

M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add include to preprocessor test

The definition of ienv-default has been moved to input-files.


Commit: 14f7c5c70bb464a5888cfcacce2f7b9a7c92f581
https://github.com/acl2/acl2/commit/14f7c5c70bb464a5888cfcacce2f7b9a7c92f581
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/code-ensembles.lisp

A books/kestrel/c/syntax/ienv.c
M books/kestrel/c/syntax/implementation-environments.lisp
A books/kestrel/c/syntax/infer-ienv.lisp

M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/tests/input-files.lisp

M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp

M books/std/util/defirrelevant.lisp

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

Merge.


Commit: 031d9ed9624cc7e569e0607cd6990e072e4cf212
https://github.com/acl2/acl2/commit/031d9ed9624cc7e569e0607cd6990e072e4cf212
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2025-12-22 (Mon, 22 Dec 2025)

Changed paths:

M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp

Log Message:
-----------
[C$] Re-generate useless runes file.


Compare: https://github.com/acl2/acl2/compare/b454c15e1f1c...031d9ed9624c

[Alessandro Coglio]

Branch: refs/heads/testing