acl2/acl2
Fork: 100 Star: 369 (更新于 2024-11-29 00:05:07)
license: NOASSERTION
Language: Common Lisp .
ACL2 System and Books as Maintained by the Community
ACL2 System and Community Books
The ACL2 theorem proving environment consists of two parts: The ACL2 System and The ACL2 Books. This repository contains both.
ACL2 System
The included version of the ACL2 System is the latest, under-development version of the ACL2 Theorem Prover. It is updated only by the ACL2 authors, Matt Kaufmann and J Moore.
WARNING: On rare occasions development versions of ACL2 may be incomplete, fragile, or unable to pass the usual regression tests. You may choose to download an official ACL2 release as described on the ACL2 Home Page or below in this README.
ACL2 Books
The books/
directory of this repository comprises the Community Books,
which are the canonical collection of open-source libraries for the ACL2
System. As the name suggests, they are updated by the ACL2 community.
Documentation
-
The Combined ACL2 + Books Manual has extensive documentation for the latest stable version of ACL2 and many of the community books that come with it.
-
There is also a development version of the manual which is updated reasonably frequently and corresponds to the development version of ACL2 and its books.
-
Finally there is the more compact ACL2-only manual which only documents the ACL2 system itself and not any books.
Each of these manuals can be downloaded for offline use by clicking the download button on the right hand side of the upper toolbar while browsing the manual.
Obtaining the Source Code
While active development of ACL2 occurs at the acl2/acl2
repo on
GitHub, stable releases are officially distributed from the
acl2-devel/acl2-devel
fork, which exists for that purpose.
Latest Stable Release
You can download a gzipped tarfile or zip file for the latest release, which includes the ACL2 system and the community books, from the releases page on GitHub.
Alternatively you can obtain a copy of the latest release using
git
. For example, do the following in a fresh directory
(note the "." at the end).
git clone -b 8.6 https://github.com/acl2-devel/acl2-devel .
The new directory /path/to/somewhere/acl2/
will now contain a copy of
ACL2 Version 8.6. Please see the ACL2 home page, specifically
its installation instructions, for how to build an
executable and certify books in your new directory.
Experimental Development Version
To check out the latest development version of the repository using
git
, you can (for example) do the following in a fresh directory
(note the "." at the end):
git clone https://github.com/acl2/acl2 .
Contributing
See the documentation for how to contribute.
Even though we have merged the Community Books (formerly acl2-books) and
ACL2 System (formerly acl2-devel) repositories into one, changes should
be made only to the books/
subdirectory unless you are Matt Kaufmann
or J Moore, since everything outside books/
is part of the ACL2
system. (If you have suggestions for system changes, they should be
emailed to Matt or J, as has been done
in the past.)
Staying Informed
We invite anyone who is using this repository to join the acl2-books mailing list, which receives commit messages and other discussion related to ACL2 system- and book-related development.
Contributors Wanted!
Everyone can contribute documentation and advice to our wiki and discuss problems and feature requests.
If you would like to contribute to this repository, see the documentation topic git-quick-start. Please note the guidelines for book development.
最近版本更新:(数据更新于 2024-09-18 00:09:13)
主题(topics):
acl2, common-lisp, first-order-logic, formal-methods, formal-verification, logic, rewriting, theorem-prover, theorem-proving
acl2/acl2同语言 Common Lisp最近更新仓库
2024-04-27 09:24:59 slime/slime
1970-01-01 00:00:00 satoukennta-cit/satokennga
1970-01-01 00:00:00 reddit-archive/reddit1.0
1970-01-01 00:00:00 fukamachi/cl-dbi
1970-01-01 00:00:00 oblivia-simplex/roper