add dev_setup script for macOS 14 #1674
Conversation
marsella
force-pushed
the
add-macos-dev-setup
branch
from
7928d93 to
969dc1b
Compare
|
also note that my review and Jonathan's were simultaneous and probably have duplicate things in them... |
|
on the scripts/ front, I think we probably do want a subdir to hold developer-facing utility material... but probably most of the stuff we'll be putting in it probably isn't scripts. So I dunno what to call it and probably it should wait until we have more stuff... |
|
Thank you for the feedback, I think I've addressed all of it, with some questions inline. This should now support macOS 12 as well as 14, but I am not sure how to test it since I don't have that OS and I don't think you can make a Docker container running macOS. Do you have a suggestion for how to test it, or is it OK to just add that it should support 12 but isn't tested in the docs? |
I resolved all the threads that I started that have been addressed in your latest changes. Thank you!
My $0.02 is that until we have tested on macOS 12, we cannot say it is supported. Perhaps IT has a testing host with macOS 12 on it still? And then I must also ask: is it important to support macOS 12 specifically for some reason? |
- Fixes some control flow and methods for checking what distribution we're on - Adds a version check for CVC4 and 5 - Modifies and documents behavior for env.sh file - Removes some bashisms and accidental use of fancy names
|
This is ready for re-review.
Sounds good to me, I'll leave this floating where it is.
We still have not formally decided what the set of officially supported OSes is for cryptol, but it will probably include macOS 12. I have not surveyed the folks at Galois who are currently working on or potentially ramping up on cryptol to know if any of them are actively using macOS 12 such that it would be worth testing and officially adding support at this time. |
|
@marsella I added a couple more comments and resolved a bunch of others. Aside from the new ones I believe all of my older threads are now resolved. Thank you! |
dev_setup.sh
Outdated
| # Technically the installation only requires cabal, but it's | ||
| # recommended to get the whole GCH shebang in one package. | ||
| # The output is not routed to log because the installer is interactive. | ||
| curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh |
There was a problem hiding this comment.
Piping a network download through sh makes me cringe, especially because it could happen as a hidden part of this script without user consent.
Is this installer a short thing that doesn't change much? This would allow having a (short list of) checksum values here in this script that verify the download before executing. Or maybe just pre-informing the user of what is about to happen and getting their consent.
There was a problem hiding this comment.
I looked but it seems that ghcup doesn't publish checksums; I could verify the gpg signatures but that would require adding some gpg keys to the user's toolchain and running the downloaded program anyway and adds a dependency on gpg, which doesn't seem ideal to me. I will add a prompt to get consent though.
There was a problem hiding this comment.
Just a note: this script almost certainly needs to be runnable in an non-interactive setting when being used to set up the environment in a container. Consent would be interactive, but it might also be important to add a command-line flag like --non-interactive to give consent and install ghcup with defaults as a result.
There was a problem hiding this comment.
Also, isn't a user not consenting to install ghcup equivalent to not consenting to run this? Isn't the content of this script implicitly trusted? If there's a concern about running malicious code, you could also pre-fetch the script and put it under version control, and run that instead.
There was a problem hiding this comment.
By "run this" I assume you mean "run dev_setup"; running a script I've downloaded and have read is different than something automatically downloading and running something else entirely that I don't necessarily even have visibility into or awareness that it's going to occur. Even with https and certs, I know that I personally would want the opportunity to inspect something downloaded before just letting it run whatever commands it wanted. The original intent is clearly benign and helpful, but we recently saw the exploit where innocuous looking changes accepted to a project had rather sinister effects. Not that I'm claiming I would have caught those either, but I'm just suggesting we err on the side of safety and clarity.
Also, if we want this to run non-interactively that presumably would require some flags or other input to the ghcup installation process as well; I haven't used ghcup so I'm based this on the preceding comment in the devscript.
There was a problem hiding this comment.
Good.
Also, I apologize for jumping in on this and don't mean to derail the process. I've just had lots of experiences (both good and bad) in this area and wanted to help steer us towards the former. So please feel free to ignore me if I'm just adding friction, and thank you again for putting this together, @marsella .
There was a problem hiding this comment.
it might also be important to add a command-line flag
This makes sense; I would propose adding any CI-specific flags when we take on the issue to actually use this in CI rather than right now.
I apologize for jumping in on this
It's no problem! Usually I'm the only one who uses my scripts, so it's nice to get a better sense of best practices.
There was a problem hiding this comment.
One should really never curl | sh, but that's how you install a lot of things these days and pushing back on it isn't very effective IME :-(
I think you can install ghcup from homebrew instead (that's where mine seems to have come from) and while I suspect it just does the same thing there's at least other eyeballs on it. So maybe we should take that route since we're using homebrew for other stuff?
There was a problem hiding this comment.
This makes sense; I would propose adding any CI-specific flags when we take on the issue to actually use this in CI rather than right now.
Sounds good to me, something to keep in mind for later if it isn't relevant to your immediate needs. Maybe add a comment to the top of the script saying that it's assumed to be interactive in the mean time?
There was a problem hiding this comment.
The brew package only installs ghcup and not the whole toolchain but I was able to manually install the other parts. It does look much nicer now. I left a breadcrumb to the original install method in the docs in case the simple thing doesn't work for someone. As an added bonus, this removes all the interactivity!
dev_setup.sh
Outdated
| # includes a half dozen other solvers that are compatible with cryptol. | ||
| function install_what4_solvers { | ||
| if ! cvc4 --version &> /dev/null || ! cvc5 --version &> /dev/null; then | ||
| notice "Installing cvc4 and/or cvc5 solvers" |
There was a problem hiding this comment.
I'd recommend indicating where these are coming from (WHAT4_SOLVERS_URL) so the user is informed and knows these might be different locations.
dev_setup.sh
Outdated
| # If we want to install more solvers by default, we can do so here, | ||
| # although we might need a different check than `--version` | ||
| for solver in cvc4 cvc5; do | ||
| if ! $solver --version &> /dev/null; then |
There was a problem hiding this comment.
Should this be if ! ./$solver ... since frequently . is explicitly not in PATH for security reasons? This also helps ensure this operates on the just unpacked file and not something that might be in the PATH (which was verified in line 113, but is still a "bad smell"). Also, the notice in the following line should probably indicate where the solvers are being installed so the user can ensure they are in their path. And I guess perhaps this whole then block might want to check if /usr/local/bin is in the path in case these are actually installed and it's just a path issue.
There was a problem hiding this comment.
Oh, this is confusing. This explicitly is trying to run the version on the path, not the version in the local directory. The parent conditional says if we're missing either of these solvers, we need to download the whole set of binaries from what4_solvers. But if you're only missing one of them, we don't want to clobber the version you do have, so this double-checks for each solver whether it's already in the path and only installs it if it not.
I'm adding an is_installed method to replace this version check that will hopefully make it more obvious what's happening.
dev_setup.sh
Outdated
| notice "Not installing cvc4 or cvc5 solvers because they already exist" | ||
|
|
||
| if ! (grep -q "version 1.8" <<< "$(cvc4 --version)"); then | ||
| notice "Your version of cvc4 is incorrect; expected 1.8" |
There was a problem hiding this comment.
I'd suggest "unexpected" rather than "incorrect" and adding the path where the corresponding solver was found.
You might also want to let the user know that the setup is not marked as failure due to these version mismatches but that they might wish to re-run after uninstalling the existing versions to get the suggested versions installed to avoid runtime cryptol issues.
And lastly, you might want to use vars (e.g. WHAT4_CVC5_VERSION) here that you set near line 30 so that it's close to the declared snapshot version used for future updates.
There was a problem hiding this comment.
These are good suggestions, I cleaned all this up.
|
Thanks for continued comments! This is ready for re-review again. |
|
I just went through and resolved any remaining threads of mine (all of which were addressed). Thanks again! |
- stop running script from the internet; start using nice commands - ghc install now depends on brew, so rewrote the brew path stuff - fixes small quoting issues and bashisms
|
Ready once again for your eyes 👀 |
dev_setup.sh
Outdated
| logged ghcup install ghc --set recommended | ||
| logged ghcup install cabal --set recommended | ||
| logged ghcup install stack --set recommended | ||
| logged ghcup install hls --set recommended |
There was a problem hiding this comment.
I think we should avoid referencing ghcup's recommended versions here. The recommended version will change over time and won't necessarily be in sync with the version we intended to target. We could list at the top of this script the versions of tools we require and then install exactly those versions with these commands. When it comes up invoking the versions of things we want it can be done explicitly by version.
For example when building with cabal we can do: cabal configure -w ghc-9.6.5 to explicitly set the build to use the expected version of GHC. If we want to lock down the version of cabal we use we could also go further: cabal-3.10.3.0 configure -w ghc-9.6.5
There was a problem hiding this comment.
As far as I know we don't use stack in our builds. We probably don't need to install it as part of this development environment.
There was a problem hiding this comment.
+1 on locking down GHC and related tools here.
There was a problem hiding this comment.
There are cabal configs for three GHC versions, though; which one? Or should we install all three by default?
There was a problem hiding this comment.
Yeah... good question. ISTM having this script use those cabal configs (or whatever canonically defines which GHCs we need to support) to find out which GHC versions to install might be nice, in the spirit of having one source of truth for that.
There was a problem hiding this comment.
I was not sure how to implement @jtdaugherty's suggestion so I hardcoded the currently recommended cabal and ghc versions in the script, which corresponds to the oldest ghc version that we have a config for.
Partially addresses #1673
This adds a
dev_setup.shscript to install dependencies for macos 14.Some other questions for reviewers:
scripts/but there isn't any such directory here. Is there a more appropriate place to keep it, or is in the root directory fine?