[acl2/acl2] aa08e2: [Remora] Move a note to a more central position.

0 views
Skip to first unread message

Alessandro Coglio

unread,
Jul 24, 2026, 9:23:52 PM (5 days ago) Jul 24
to acl2-...@googlegroups.com
Branch: refs/heads/grammar-note
Home: https://github.com/acl2/acl2
Commit: aa08e28029585b351d3320c52bb9d08823d66cb9
https://github.com/acl2/acl2/commit/aa08e28029585b351d3320c52bb9d08823d66cb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

Log Message:
-----------
[Remora] Move a note to a more central position.



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

Alessandro Coglio

unread,
Jul 25, 2026, 10:32:24 PM (4 days ago) Jul 25
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: aa08e28029585b351d3320c52bb9d08823d66cb9
https://github.com/acl2/acl2/commit/aa08e28029585b351d3320c52bb9d08823d66cb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

Log Message:
-----------
[Remora] Move a note to a more central position.


Commit: 174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
https://github.com/acl2/acl2/commit/174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

Log Message:
-----------
[Remora] Remove stray blank line.


Commit: 89d2cf4304c4002efa205c9ed51c453b7b2d4263
https://github.com/acl2/acl2/commit/89d2cf4304c4002efa205c9ed51c453b7b2d4263
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add more inference rules.


Commit: b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
https://github.com/acl2/acl2/commit/b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/fields/README
M books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
M books/projects/fields/galois.lisp
A books/projects/fields/polynomials.lisp
M books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/galois.lisp
A books/projects/fields/vectors.lisp
M books/projects/linear/field.lisp
M books/projects/linear/ring.lisp
M books/projects/linear/support/field.lisp
M books/projects/linear/support/ring.lisp
M books/projects/linear/support/vectors.lisp
M books/projects/linear/vectors.lisp
M books/std/util/definductive.lisp

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


Commit: c0b81f47bf75544e141e04b5802cb7e9882ed5c4
https://github.com/acl2/acl2/commit/c0b81f47bf75544e141e04b5802cb7e9882ed5c4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Improve some doc.


Commit: 01c535f961022c5a01f27331aedf1fb589f498b3
https://github.com/acl2/acl2/commit/01c535f961022c5a01f27331aedf1fb589f498b3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Simplify two inference rules.


Commit: 2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
https://github.com/acl2/acl2/commit/2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add and improve some inference rules.


Commit: 25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
https://github.com/acl2/acl2/commit/25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add a rule for dimension subtractions.


Commit: c9ca7237aafd1842a6d4e9e00e321a09eea76230
https://github.com/acl2/acl2/commit/c9ca7237aafd1842a6d4e9e00e321a09eea76230
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Fix layout.


Commit: bb08f3c7e07c2641f26ece0c1ce3272cfe124854
https://github.com/acl2/acl2/commit/bb08f3c7e07c2641f26ece0c1ce3272cfe124854
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Fix some code and doc.


Commit: 4584af836f19a05f51c3e6a4d1f46c3160f21f02
https://github.com/acl2/acl2/commit/4584af836f19a05f51c3e6a4d1f46c3160f21f02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Fix typo in doc.


Commit: 2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
https://github.com/acl2/acl2/commit/2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add an inference rule.


Commit: e819cef97511be7c96577a12704b1817600df5d8
https://github.com/acl2/acl2/commit/e819cef97511be7c96577a12704b1817600df5d8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add inference rule.


Commit: 19a79469dbf277ff1e9eaef7f7977d977353faf6
https://github.com/acl2/acl2/commit/19a79469dbf277ff1e9eaef7f7977d977353faf6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remore] Remove some redundant inf. rules.


Commit: cf8a4ae1465ed49634b77b72f8eaa54179849c57
https://github.com/acl2/acl2/commit/cf8a4ae1465ed49634b77b72f8eaa54179849c57
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Improve the inf. rules.


Commit: 6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
https://github.com/acl2/acl2/commit/6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Improve dimeq inf rules and their doc.


Compare: https://github.com/acl2/acl2/compare/98383ead4d64...6df62bcb2c68

Alessandro Coglio

unread,
Jul 25, 2026, 10:33:43 PM (4 days ago) Jul 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Jul 26, 2026, 1:36:24 AM (4 days ago) Jul 26
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: aa08e28029585b351d3320c52bb9d08823d66cb9
https://github.com/acl2/acl2/commit/aa08e28029585b351d3320c52bb9d08823d66cb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

Log Message:
-----------
[Remora] Move a note to a more central position.


Commit: 174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
https://github.com/acl2/acl2/commit/174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

Log Message:
-----------
[Remora] Remove stray blank line.


Commit: 4b184ad520371bfc4c3bb02499898a53f4cc240c
https://github.com/acl2/acl2/commit/4b184ad520371bfc4c3bb02499898a53f4cc240c
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp

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


Commit: c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
https://github.com/acl2/acl2/commit/c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/projects/fields/embeddings.lisp
M books/projects/fields/support/embeddings.lisp

Log Message:
-----------
Defined inverse embedding


Commit: 89d2cf4304c4002efa205c9ed51c453b7b2d4263
https://github.com/acl2/acl2/commit/89d2cf4304c4002efa205c9ed51c453b7b2d4263
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp

Log Message:
-----------
[Remora] Add more inference rules.


Commit: 4f41c9f07359f37071f263ab6dd9d628b3eee524
https://github.com/acl2/acl2/commit/4f41c9f07359f37071f263ab6dd9d628b3eee524
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
Merge commit '6a464d57c695a911e59ccd6c748fcd04bda09065' into HEAD


Commit: a20ec9a94780982cc48fc875c447fa3b9b8101d1
https://github.com/acl2/acl2/commit/a20ec9a94780982cc48fc875c447fa3b9b8101d1
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:

Log Message:
-----------
“merge”


Commit: 9230f610e8176bef5e8b7519df0a335310b335f9
https://github.com/acl2/acl2/commit/9230f610e8176bef5e8b7519df0a335310b335f9
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
“merge”


Commit: 98383ead4d64968fa0e2645c4223257c39d5eff3
https://github.com/acl2/acl2/commit/98383ead4d64968fa0e2645c4223257c39d5eff3
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/std/util/definductive.lisp

Log Message:
-----------
Merge commit '127036a730484d24d097aa2f5b78fa8c4c01f265' into HEAD
Compare: https://github.com/acl2/acl2/compare/127036a73048...6df62bcb2c68
Reply all
Reply to author
Forward
0 new messages