| HEAD | 2c7c690 | Made miscellaneous changes to accommodate GCL Avoided compiler warning that was caused by a call of warning$ laid down for *1* functions with invariant-risk. In books/kestrel/bv/rules.lisp, changed ::hints to :hints. Added some forms (set-compile-fns t). Those might not be necessary, though they might help: they didn't solve all GCL regression problems, but things improved when using not only those fixes but also -j 4 instead of -j 8 on a 32G machine, and continuing to use GCL_MEM_MULTIPLE=0.25 in the "make" command. I plan on more GCL testing in the near future to make sure all is well with GCL; for now I've just run an SBCL "everything" regression successfully, to check that I didn't make things worse. | 12 July 2022, 01:02:09 UTC |
| refs/heads/abnf-rulename-subs | e5032d6 | [abnf] add utility that finds subtype-like rulenames from a given rule name and grammar | 06 May 2022, 00:06:35 UTC |
| refs/heads/arith-deps | fb65406 | [arithmetic] Reduce what is exported by arithmetic books. Include cowles/acl2-crg only locally (adjust a few workshop books to compensate). Remove arithmetic/cert.acl2 since it is unnecessary. This also prevents the unncessary inclusion of std/portcullis. Add customization file. | 18 May 2022, 19:06:21 UTC |
| refs/heads/arithmetic-deps | ea6b63e | [arithmetic] Add customization file. | 15 May 2022, 16:07:22 UTC |
| refs/heads/cert-dep-lsp | 1ec6514 | rename environment variable INHIBIT_DEPS_LSP to ACL2_INHIBIT_DEPS_LSP; improve comment slightly | 10 May 2022, 01:00:35 UTC |
| refs/heads/cert-heed-useless-runes-2 | 0e430c2 | add explicit ignore of ignored params | 12 January 2022, 05:09:49 UTC |
| refs/heads/cert-heed-useless-runes-2-doc | 3547190 | move some useless runes notes from note-8-5 to note-8-5-books | 19 January 2022, 07:56:07 UTC |
| refs/heads/defstobj-fnname-guards | 77b68d5 | Add guards to some stobj-related functions. | 30 April 2022, 22:06:10 UTC |
| refs/heads/doc-top-fast | 474aa42 | Renamed doc/top to doc/top-slow, renamed doc/top-fast to doc/top. Added doc/top-slow to list of slow books in GNUMakefile. | 23 July 2019, 17:16:19 UTC |
| refs/heads/fix-acl2r-build-aug-2020 | 77f9a09 | Make include-book local; change a few references This is at least a partial fixing of the ACL2(r) build | 02 August 2020, 06:56:52 UTC |
| refs/heads/fix-topics | 99f079b | Merge branch 'master' of github.com:acl2/acl2 into testing-centaur | 13 April 2020, 15:18:40 UTC |
| refs/heads/improve-books-makefile | b9f0e02 | Merge pull request #1014 from ragerdl/improve-books-makefile No review needed: merging into non-standard branch (not in a mathematical sense) | 30 July 2019, 19:35:13 UTC |
| refs/heads/master | 2c7c690 | Made miscellaneous changes to accommodate GCL Avoided compiler warning that was caused by a call of warning$ laid down for *1* functions with invariant-risk. In books/kestrel/bv/rules.lisp, changed ::hints to :hints. Added some forms (set-compile-fns t). Those might not be necessary, though they might help: they didn't solve all GCL regression problems, but things improved when using not only those fixes but also -j 4 instead of -j 8 on a 32G machine, and continuing to use GCL_MEM_MULTIPLE=0.25 in the "make" command. I plan on more GCL testing in the near future to make sure all is well with GCL; for now I've just run an SBCL "everything" regression successfully, to check that I didn't make things worse. | 12 July 2022, 01:02:09 UTC |
| refs/heads/mv-nth-weakening-tweaks | 0777180 | fixes for books for change in rewriting of mv-nth terms | 30 September 2019, 20:43:22 UTC |
| refs/heads/mv-nth-weakening-tweaks-new | e7f488f | Book changes needed for rewriter mv-nth handling change | 27 September 2019, 15:01:48 UTC |
| refs/heads/namedb-deps | 9a418b3 | [VL] Reduce deps of vl/util/namedb. This change prevents vl/util/namedb from including vl/util/defs. Various include-books have to be added in namedb.lisp and other files to compensate, but the net effect is to greatly reduce what is included by namedb and tools that include it, including defrstobj and the x86 model. | 03 May 2022, 03:17:06 UTC |
| refs/heads/nested-abstract-stobjs | 7ad777f | Fifth and perhaps final version (on a branch) of child stobjs of abstract stobj. Passed "everything" regression. | 21 May 2021, 03:07:08 UTC |
| refs/heads/parse-json-with-sha256 | 480415f | add function that parses and returns json and at the same time runs sha-256 on the bytes and returns that as well | 13 September 2021, 20:27:18 UTC |
| refs/heads/pete-symbol-gen-defequiv-refinement-cong | 5dedc13 | Updates to centaur books to synchronize with the updates to defequiv, defrefinement and defcong. | 12 September 2019, 16:31:59 UTC |
| refs/heads/svex-compose-theory | c42d568 | WIP on new svex composition theory | 06 August 2021, 22:30:52 UTC |
| refs/heads/testing | 2c7c690 | Made miscellaneous changes to accommodate GCL Avoided compiler warning that was caused by a call of warning$ laid down for *1* functions with invariant-risk. In books/kestrel/bv/rules.lisp, changed ::hints to :hints. Added some forms (set-compile-fns t). Those might not be necessary, though they might help: they didn't solve all GCL regression problems, but things improved when using not only those fixes but also -j 4 instead of -j 8 on a 32G machine, and continuing to use GCL_MEM_MULTIPLE=0.25 in the "make" command. I plan on more GCL testing in the near future to make sure all is well with GCL; for now I've just run an SBCL "everything" regression successfully, to check that I didn't make things worse. | 12 July 2022, 01:02:09 UTC |
| refs/heads/testing-acl2s | 2c7c690 | Made miscellaneous changes to accommodate GCL Avoided compiler warning that was caused by a call of warning$ laid down for *1* functions with invariant-risk. In books/kestrel/bv/rules.lisp, changed ::hints to :hints. Added some forms (set-compile-fns t). Those might not be necessary, though they might help: they didn't solve all GCL regression problems, but things improved when using not only those fixes but also -j 4 instead of -j 8 on a 32G machine, and continuing to use GCL_MEM_MULTIPLE=0.25 in the "make" command. I plan on more GCL testing in the near future to make sure all is well with GCL; for now I've just run an SBCL "everything" regression successfully, to check that I didn't make things worse. | 12 July 2022, 01:02:09 UTC |
| refs/heads/testing-intel | eddb087 | Merge pull request #1403 from intel-staging/intel-main Fixed certification issue with projects/rp-rewriter/lib/mult3/demo/demo-3.lisp | 14 June 2022, 23:34:43 UTC |
| refs/heads/testing-kestrel | 0ba4be1 | Merge commit '861719a45e579b0a050aa7af131b1537c41ce77f' into HEAD | 11 July 2022, 20:01:11 UTC |
| refs/heads/testing-user-01 | 2b093a8 | [ATC] Fix XDOC link. | 07 July 2022, 13:13:04 UTC |
| refs/tags/7.1 | 865417b | ACL2 Version 7.1 release | 06 May 2015, 21:14:16 UTC |
| refs/tags/7.2 | a12f619 | ACL2 Version 7.2 release | 15 January 2016, 04:09:12 UTC |
| refs/tags/7.3 | 59077a3 | ACL2 Version 7.3 release | 16 December 2016, 20:19:28 UTC |
| refs/tags/7.4 | ab320f0 | ACL2 Version 7.4 release | 20 March 2017, 18:04:18 UTC |
| refs/tags/8.0 | 5ab2134 | ACL2 Version 8.0 release | 13 December 2017, 03:31:37 UTC |
| refs/tags/8.1 | ebe08ba | ACL2 Version 8.1 release | 17 September 2018, 02:36:09 UTC |
| refs/tags/8.2 | 0602ef9 | ACL2 Version 8.2 release | 05 May 2019, 03:04:52 UTC |
| refs/tags/8.4 | a8441ff | ACL2 Version 8.4 release | 06 August 2021, 00:24:51 UTC |
