Eligibility of ACL2s Software for Core

[mister-walter]

I'm interested in getting a formula for the ACL2 Sedan (ACL2s) theorem proving system into the Homebrew/core repository. Before putting together a PR, I figured it would be a good idea to put out some feelers regarding whether ACL2s would be an appropriate piece of software to include in Homebrew/core.

Side note: I have developed a Homebrew formula for ACL2s on GitHub. I am not an author of ACL2s, but I work under its maintainer.

ACL2s is a set of libraries that run on top of the ACL2 theorem proving system, which does have a package in the core repository. To use these libraries ("books") inside of ACL2, they first must be certified, a process that takes a substantial amount of time. The existing ACL2 package certifies the "base" set of libraries and distributes bottles containing these pre-certified files, in addition to all of the ACL2 community libraries (including ACL2s), which are left uncertified.

The primary benefit of an ACL2s package is that a user does need to spend a significant amount of time and resources certifying the books it depends on. This can be the difference between a user being able to run the software or not, depending on their system's resources.

A couple places where I am concerned ACL2s might not satisfy Homebrew's "Acceptable Formulae" policies:

• "Stable versions": ACL2s does not have a modern stable release, though after discussion with its maintainer, this might change.
• "Niche (or self-submitted) stuff": This software is fairly niche, though it is used by a few hundred university students each year. I am associated with the current maintainer, though I am not that maintainer.

The current formula bundles its own copy of SBCL, but that would not be necessary in the case that ACL2s was in the core repo, since it would just be rebuilt every time its underlying Common Lisp implementation (SBCL) was updated, just like ACL2.

Hopefully this is making sense, thanks for your time.

[SMillerDev]

The stable version is really the big problem here. Without it we can't really track updates.