**HTTP 200 OK**
**Allow:** GET, HEAD, OPTIONS
**Content-Type:** application/json
**Vary:** Accept
{
"name": "acl2",
"portdir": "math/acl2",
"version": "8.3",
"license": "BSD",
"platforms": "darwin",
"epoch": 0,
"replaced_by": null,
"homepage": "http://www.cs.utexas.edu/users/moore/acl2/v8-3",
"description": "Applicative Common Lisp / A Computational Logic",
"long_description": "ACL2 (Applicative Common Lisp / A Computational Logic) is the successor to nqthm, the Boyer-Moore theorem prover. ACL2 can be used to automatically or semi-automatically prove theorems and has been used extensively in real applications (e.g., proving the correctness of certain calculations in the floating point unit of the AMD K5 microprocessor. ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover. Because the meta-language is the same as the language (a subset of Common Lisp), it is very flexible.",
"active": true,
"categories": [
"math"
],
"maintainers": [
{
"name": "ijackson",
"github": "JacksonIsaac",
"ports_count": 33
}
],
"variants": [
"emacs",
"ccl",
"certify",
"regression",
"nonstd"
],
"dependencies": [
{
"type": "build",
"ports": [
"clang-9.0"
]
},
{
"type": "lib",
"ports": [
"sbcl"
]
}
],
"depends_on": []
}