Install STP

[jimwhite]

This is a great formula and rescued me from days of trying to figure out how to get acl2(s) fully working.

One small addition which greatly increases the number of useable books is to install STP. That enables the entire Kestrel library (notable for me are APT and AXE).

Formula/acl2s.rb

depends_on "zstd"
depends_on "stp"

test-docker/Dockerfile

RUN brew install lz4 xz zlib zstd stp sbcl

I realize it is easy enough for a user to do this themselves but the issue (as you well know) is that the error message they get when trying to include the book gives them no clue about what is actually wrong and how to fix it.

[mister-walter]

Thanks much for this suggestion Jim!

I'm sympathetic to the issue you ran into here - it's often difficult to identify that a book failed to certify due to some dependency missing from your system. I'm a little unsure about whether adding a hard dependency on STP makes sense here though, mainly due to the number of dependencies STP ends up pulling in:

$ brew install stp
==> Fetching dependencies for stp: icu4c, bzip2, boost, cryptominisat, gmp, minisat, mpdecimal, ca-certificates, openssl@3, ncurses, readline, sqlite, expat, libedit, libffi, libxcrypt, unzip, berkeley-db@5, krb5, libtirpc, libnsl, python@3.12, gdbm and perl

(note to self: perl really should be a dependency of the acl2s package, though clearly it is currently installed on the systems we support given we haven't noticed this yet)

Something I can pretty easily do that I'd be happy with is create another version of the package (acl2s-full? acl2-full?) that has STP and some of the other optional ACL2 dependencies installed: maybe Glucose, Z3 and IPASIR? We could also certify more books than we currently do, maybe even books/top/doc?

Let me know what you think - I'm happy to discuss this more!

Side rant: One thing I quite dislike about having additional Homebrew packages installed on my machine is that their binaries will often end up getting used over those from my system's installed packages. This is perhaps why I'm particularly sensitive to adding additional dependencies, as I'll need to brew unlink all that stuff.

[jimwhite]

Does homebrew have specializations like pypi so we could have something like brew install acl2s[stp]? I've never seen a command like that so I'm guessing no. So yes, I think additional formulae is likely the way to go. ATM I'd be happy with what could be called acl2s-kestrel (although I've also been trying to include centaur). I tried making workshops and the numerous messages made it clear that was folly.

I spent days trying to get Docker working and thought I wanted centaur/bridge (for Jupyter) but eventually learned they really mean it when they say it probably only works for CCL (and that is X86 only). When I come back to that I'm going to start with your test Dockerfile. For a Jupyter kernel I'm thinking what I'd like is to use the one for SBCL and hook ACL2 into that somehow.

I think the real issue is the building of the books. Is it feasible to (re-)build as need as an option for include-book?

The dependencies may not be compete and it also appears they don't all get along with each other. So with STP installed I did:

cd `which acl2s`/../acl2/books
make -j 8 basic centaur kestrel acl2s

but when I tried (include-book "kestrel/axe/top" :dir :system :ttags :all) I got an error about query macro being redefined:

ACL2 Error in ( defmacro query ...):  The name query is in use as a
label.  The redefinition feature is currently off.  See :DOC ld-redefinition-
action.

Note: query was previously defined in the last of the following books.

   [Included books, outermost to innermost:
    "/opt/homebrew/Cellar/acl2s/0.1.12/opt/acl2s/acl2/books/acl2s/ccg/ccg.lisp"
   ]

Note: the current attempt to define query is being made in the last
of the following books.

   [Included books, outermost to innermost:
    "/opt/homebrew/Cellar/acl2s/0.1.12/opt/acl2s/acl2/books/kestrel/axe/top.lisp"
    "/opt/homebrew/Cellar/acl2s/0.1.12/opt/acl2s/acl2/books/kestrel/axe/query.lisp"
   ]

And when I tried to do the minimum:

make -j 8 kestrel/apt

The (include-book "kestrel/apt/top" :dir :system :ttags :all) failed with some missing dependency and I had to remake the kestrel dir to get it to work.

And finally there is the question of using the HEAD of the ACL2 github vs 8.5. Pretty sure I've seen some issues (perhaps including the CCG/AXE conflict above) that arise from using these unreleased snapshots. I know ACL2S has a formula version, but going back to the naming question (far lol) above, this could also call for another formula like acl2s-kestrel-8.5.