Remove ACL2s section from installation page #1602
Conversation
ACL2s no longer provides precompiled binaries
(I assumed the TOC was autogenerated 😅)
|
Thanks. Normally, pull requests are to go to testing rather than to master, so that they can be tested first; however, that testing isn't relevant for this file. Also, J and I are normally the only ones to modify files outside books/; however, I'll be happy to accept this pull request if either @pmanolios or @mister-walter says it's OK. (I want to check in case they prefer a different change.) |
Good to know, I'll keep this in mind for the future! |
|
Many apologies for the dead links Caleb! Indeed ACL2s doesn't provide binaries in the way it used to. I agree with Caleb's edits removing the old links. I have many thoughts about the installation page. I put these in #1608 as most of them aren't relevant to this PR. I would ask that we wait for @pmanolios to weigh in on this PR before merging. He likely won't be able to respond until next week. |
|
It looks like @MattKaufmann's changes to the installation page supersede this PR. @calebegg what do you think of the new version of the "Obtaining and Installing ACL2" page? |
|
The broken link has been copied here: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.html?topic=ACL2____PRE-BUILT-BINARY-DISTRIBUTIONS |
|
Oops, I was just about to work on a PR updating that XDOC topic. I will submit that later today. |
|
@calebegg Looks like the XDOC documentation has been updated since my PR was accepted, can you check now? |
|
Actually I just realized that the windows-installation topic probably should be updated as well - I will submit a PR for this soon. |
|
I guess it seems a little strange to mention ACL2s at all under the heading "Pre-built-binary-distributions", since ACL2s no longer provides those. It may make sense to mention homebrew, I don't know if it provides pre-built binaries, it did not for me (it had to compile for my platform which took prohibitively long, leading me to look elsewhere). |
|
I apologize for the pain regarding Homebrew - below I've included some more details that may explain why you ran into issues there. I agree that the user experience is bad, though we have found it better than other options we've tried for getting ACL2s installed on a large number of students' machines. We do aim to provide pre-built binaries for ACL2s, at least in the form of Homebrew bottles, though as you have seen it is easy to run into a situation where you are building things from scratch. I'm happy to add additional text around the Homebrew bottle situation in the documentation wherever you think it would be helpful - the simplest way to ensure you're only installing bottles and never compiling yourself is to use I'm keenly interested in there being an easier way to install ACL2 (and ACL2s) without having to go through the build/certification process on every user's machine. I think this deserves additional discussion (maybe Homebrew isn't the right way!), so I'll create a GitHub issue where we can dive into that in more detail. More details on Homebrew and binariesUnfortunately the way that Homebrew determines whether or not to use a pre-built binary on macOS is somewhat opaque. The typical situation where I've seen bottles not be used is when no pre-built binary is available for your system's processor and for a macOS version that is compatible with yours - the Homebrew bottle documentation seems to indicate it only works if a bottle exists for your exact macOS version, though I seem to recall bottles working/being used if one existed for the right processor kind (x86 vs Apple Silicon) and if one existed for the same version or an older version of macOS than the one you're using. For "official" Homebrew recipes, bottles are maintained for both processor kinds, for the most recent 3 stable versions of macOS. These are built using Homebrew's CI infrastructure. Note that there is an ACL2 formula in the official Homebrew repo, which should have the aforementioned CI-generated bottles available. Formulas in the official Homebrew repo are required to track stable versions of software (see the basic requirements for formulas in homebrew/core), which means the current ACL2 formula is tracking ACL2 8.5, which is around 2 years old. This isn't a problem with ACL2's release schedule to be clear, but Homebrew's rules limit the use of the ACL2 formula to those who don't require any of the recent ACL2 changes. I haven't had access to the full range of macOS processor kinds/OS versions when building bottles for the homebrew-acl2s formula and I generally only update it before the beginning of a semester. Github only recently started offering Apple Silicon action runners for free, making it possible for me to finally automatically build Apple Silicon bottles, though they only offer macOS Sonoma Apple Silicon runners and don't offer x86 macOS Sonoma runners. Long story short, it could have been that the set of bottles currently available for the homebrew-acl2s formula was insufficient to support your system. This usually happens on macOS machines, though it could also happen if using a non-x86 Linux machine, or if you have installed Homebrew to a non-standard prefix. |
|
Thanks for the detailed explanation! I will try again with homebrew and the flag you mentioned when I get a chance. In the meantime, the goal of this PR was to remove the confusing broken link and that's accomplished so I'm going to close it. |
ACL2s no longer provides precompiled binaries