We've tried a bunch of approaches for getting ACL2/ACL2s installed on students' computers, but it generally ends up being painful. There are a few reasons one might want to do this, but for class purposes here are a few:
- Avoiding building ACL2 and certifying books on students' machines, which may be slow and low on resources (particularly RAM)
- Simplifying the installation process
- Ensuring everyone is on the same version of ACL2
There are others who may want to install pre-built ACL2 distributions for similar reasons. @calebegg is one such person, who noted in #1602 that he tried one of the ways that we describe for installing pre-built ACL2 distributions (the ACL2s Homebrew package) but that it failed to use the pre-built binaries and ended up taking prohibitively long to build from scratch. I replied with some of the reasons why the pre-built distributions may not have been used, but I recognize that the current user experience for the ACL2s Homebrew package is bad and I'd love for it to be easier.
To be clear, when I say "ACL2 distributions" here I really mean ACL2 binaries + certificates for some books. In my experience, the generation of the ACL2 binary itself is fairly fast (less than a minute) but certifying e.g. books/acl2s/top and its dependencies is substantially slower, especially if on a system with limited RAM or with a slower processor.
I'd love a world where it was super easy to install pre-built ACL2 distributions on Windows, macOS and Linux systems, and I'm hoping this issue will provoke some discussion about what works and what doesn't! I'll start by talking about what we currently are doing with ACL2s at Northeastern:
We distribute the homebrew-acl2s Homebrew package, which (in perfect conditions) allows one to install a pre-built ACL2s system on a macOS and Linux system with Homebrew installed. The conditions under which Homebrew decides to use pre-built binaries ("bottles") are a little unclear to me, and I wrote up some of the issues in detail in my aforementioned reply. Basically, the main issues revolve around needing to build the pre-built binary on (ideally) 6 different macOS version-processor kind combinations, and that's only if one wants to support the most modern 3 versions of macOS. Additionally, bottles won't be used if the user decides to install Homebrew to a different location ("prefix") than the default one.
We had previously had students run ACL2s inside of a Linux VM, but this became untenable with the introduction of Apple Silicon Macs and the fact that VirtualBox (our hypervisor of choice) didn't even have a test build that supports Apple Silicon Macs until quite recently (it is a "developer preview with known issues" currently). We ran into other issues with students running ACL2s inside of a VM, especially on weaker computers, including situations where folks would need to drop into BIOS/UEFI to change settings around virtualization.
We've tried a bunch of approaches for getting ACL2/ACL2s installed on students' computers, but it generally ends up being painful. There are a few reasons one might want to do this, but for class purposes here are a few:
There are others who may want to install pre-built ACL2 distributions for similar reasons. @calebegg is one such person, who noted in #1602 that he tried one of the ways that we describe for installing pre-built ACL2 distributions (the ACL2s Homebrew package) but that it failed to use the pre-built binaries and ended up taking prohibitively long to build from scratch. I replied with some of the reasons why the pre-built distributions may not have been used, but I recognize that the current user experience for the ACL2s Homebrew package is bad and I'd love for it to be easier.
To be clear, when I say "ACL2 distributions" here I really mean ACL2 binaries + certificates for some books. In my experience, the generation of the ACL2 binary itself is fairly fast (less than a minute) but certifying e.g.
books/acl2s/topand its dependencies is substantially slower, especially if on a system with limited RAM or with a slower processor.I'd love a world where it was super easy to install pre-built ACL2 distributions on Windows, macOS and Linux systems, and I'm hoping this issue will provoke some discussion about what works and what doesn't! I'll start by talking about what we currently are doing with ACL2s at Northeastern:
We distribute the homebrew-acl2s Homebrew package, which (in perfect conditions) allows one to install a pre-built ACL2s system on a macOS and Linux system with Homebrew installed. The conditions under which Homebrew decides to use pre-built binaries ("bottles") are a little unclear to me, and I wrote up some of the issues in detail in my aforementioned reply. Basically, the main issues revolve around needing to build the pre-built binary on (ideally) 6 different macOS version-processor kind combinations, and that's only if one wants to support the most modern 3 versions of macOS. Additionally, bottles won't be used if the user decides to install Homebrew to a different location ("prefix") than the default one.
We had previously had students run ACL2s inside of a Linux VM, but this became untenable with the introduction of Apple Silicon Macs and the fact that VirtualBox (our hypervisor of choice) didn't even have a test build that supports Apple Silicon Macs until quite recently (it is a "developer preview with known issues" currently). We ran into other issues with students running ACL2s inside of a VM, especially on weaker computers, including situations where folks would need to drop into BIOS/UEFI to change settings around virtualization.