Description
When responding to PR #1602, I had many thoughts about the installation page, but decided they belong in this issue rather than that PR. Below is entirely my opinion, feel free to push back on any of it.
For clarity, I would add something to the top of the page reiterating that the easy Unix install instructions are likely the best option for most people (this is said on the main installation guide page, but it's pretty easy to get dropped directly into the "Obtaining and Installing ACL2" page by following Google). Note that Windows users nowadays can use Windows Subsystem for Linux to install ACL2 in a Linux environment running inside of Windows. This is what we recommend for students at Northeastern who need to use ACL2s on a Windows machine.
I would add a section about ways to try ACL2 out before "installing" it. This section might mention the following:
- @calebegg 's Proof Pad, a web-based IDE for ACL2 which is super cool (this is up to you though Caleb!)
- I provide an ACL2 Docker container (atwalter/acl2, repo is here) and I think others do as well. (I'm pretty sure Ruben has one) Not sure if this really counts as "not installing" but it's easy to get started with if you already have Docker installed. I wouldn't recommend this as a long-term solution though.
- Ruben's ACL2 Jupyter Notebook kernel is also available, though I don't know if this requires an existing local installation of ACL2s.
For the pre-built binary distributions section, I would remove the old ACL2s links as Caleb suggested and add the following:
- Some folks maintain a Homebrew recipe for ACL2, which includes bottles (binaries) for some macOS version + architecture combinations. (Likely) per Homebrew rules, this recipe tracks stable ACL2 releases, so it currently packages ACL2 v8.5 for example. Note that the recipe can also be used on Linux if one installs Homebrew there, and binaries are available for x86 Linux systems.
- There's also a Nix package for ACL2: https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/interpreters/acl2/default.nix
- Folks interested in installing ACL2s should be pointed to the ACL2s installation XDOC topics