From 969dc1bc493632d728323a7af21b30e245c0786d Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 29 May 2024 16:15:11 -0400
Subject: [PATCH 1/7] add dev_setup script for macOS 14 #1673

---
 .gitignore   |   3 +-
 dev_setup.sh | 113 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 115 insertions(+), 1 deletion(-)
 create mode 100755 dev_setup.sh

diff --git a/.gitignore b/.gitignore
index e3fb03b09..d73c08b7f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,6 +11,7 @@ dist-newstyle
 cabal.project.freeze
 cabal.project.local*
 .vscode/
+dev_setup.log
 
 # don't check in generated documentation
 #docs/CryptolPrims.pdf
@@ -41,4 +42,4 @@ cryptol.wixobj
 cryptol.wixpdb
 
 # happy-generated files
-src/Cryptol/Parser.hs
\ No newline at end of file
+src/Cryptol/Parser.hs
diff --git a/dev_setup.sh b/dev_setup.sh
new file mode 100755
index 000000000..dd52b022c
--- /dev/null
+++ b/dev_setup.sh
@@ -0,0 +1,113 @@
+#!/usr/bin/env bash
+
+# cryptol setup script
+#
+# Supported distribution(s):
+#  * macOS 14 (AArch64)
+#
+# This script installs everything needed to get a working development
+# environment for cryptol. Any new environment requirements should be
+# added to this script.
+#
+
+set -e
+
+HERE=$(cd `dirname $0`; pwd)
+LOG=$HERE/dev_setup.log
+
+function notice {
+    echo "[NOTICE] $*"
+}
+
+# Requires: LOG set to log file path.
+function logged {
+    if ! [ -z "$LOG" ]
+    then
+        mkdir -p `dirname $LOG`
+        echo $* >>$LOG
+        if ! $* >>$LOG 2>&1
+        then
+            echo
+            echo "An error occurred; please see $LOG"
+            echo "Here are the last 50 lines:"
+            tail -n 50 $LOG
+            exit 1
+        fi
+    fi
+}
+
+function update_submodules {
+    cd $HERE
+    notice "Updating submodules"
+    git submodule update --init
+}
+
+function install_ghcup {
+    if ! ghcup --version &> /dev/null
+    then
+        notice "Installing ghcup, GHC, and cabal"
+        # technically the installation only requires cabal, but it's 
+        # recommended to get the whole GCH shebang in one package
+        curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh
+    else
+        notice "Using existing ghcup installation"
+    fi
+
+}
+
+# Indicate whether this is running macOS on the Apple M series hardware.
+function is_macos_aarch {
+    # Is it running macOS?
+    if [[ "$OSTYPE" != "darwin"* ]]; then
+        notice "dev setup does not currently support your OS / hardware"
+        exit 1 
+    fi
+
+    # Does it use an M-series chip?
+    chip=$(system_profiler SPHardwareDataType | grep Chip)
+    [[ $chip == *M1* || $chip == *M2* || $chip == *M3* ]]
+}
+
+function install_gmp {
+    if is_macos_aarch; then
+        notice "Installing gmp via Homebrew, if it's not already installed"
+        logged brew list gmp || brew install gmp
+
+        # on macOS 12 (x86_64), I think homebrew uses different locations
+        notice "You may need to add the following environment variables to your '.profile': \n"\
+            "export CPATH=/opt/homebrew/include\n"\
+            "export LIBRARY_PATH=/opt/homebrew/lib\n"
+    fi
+}
+
+function install_what4_solvers {
+    if ! cvc4 --version &> /dev/null || ! cvc5 --version &> /dev/null; then
+        notice "Installing cvc4 and/or cvc5 solvers"
+
+        # There are different URLs for other supported platforms
+        if is_macos_aarch; then
+            what4_solvers_url="https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/macos-14-ARM64-bin.zip"
+        fi
+
+        solvers_dir=$(mktemp -d)
+        curl --proto '=https' --tlsv1.2 -sSfL $what4_solvers_url > "$solvers_dir/solvers.bin.zip"
+        cd $solvers_dir
+        logged unzip solvers.bin.zip
+        rm solvers.bin.zip
+        
+        # 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 
+                notice "Installing $solver"
+                chmod u+x $solver
+                sudo mv $solver /usr/local/bin
+            fi
+        done
+    fi
+}
+
+update_submodules
+install_ghcup
+install_gmp
+install_what4_solvers

From dfd0a0feadbb7ee96daa59bdcf1d4e3d98dc32f9 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Fri, 31 May 2024 11:02:07 -0400
Subject: [PATCH 2/7] clean up control flow in dev script #1673

---
 dev_setup.sh | 54 ++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 38 insertions(+), 16 deletions(-)

diff --git a/dev_setup.sh b/dev_setup.sh
index dd52b022c..23c99f895 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -15,8 +15,13 @@ set -e
 HERE=$(cd `dirname $0`; pwd)
 LOG=$HERE/dev_setup.log
 
+WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212"
+WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT/"
+WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip"
+WHAT4_SOLVERS_MACOS_14="macos-14-ARM64-bin.zip"
+
 function notice {
-    echo "[NOTICE] $*"
+    echo -e "[NOTICE] $*"
 }
 
 # Requires: LOG set to log file path.
@@ -37,6 +42,7 @@ function logged {
 }
 
 function update_submodules {
+    # todo: change names here
     cd $HERE
     notice "Updating submodules"
     git submodule update --init
@@ -55,45 +61,61 @@ function install_ghcup {
 
 }
 
+function is_macos {
+    [ "$OSTYPE" = "darwin"* ]
+}
+
 # Indicate whether this is running macOS on the Apple M series hardware.
 function is_macos_aarch {
     # Is it running macOS?
-    if [[ "$OSTYPE" != "darwin"* ]]; then
-        notice "dev setup does not currently support your OS / hardware"
-        exit 1 
+    if [ ! is_macos ]; then
+        return 1
     fi
 
     # Does it use an M-series chip?
+    # Actually this command apparently doesn't exist in macOS 12, so this will fail the wrong way
     chip=$(system_profiler SPHardwareDataType | grep Chip)
-    [[ $chip == *M1* || $chip == *M2* || $chip == *M3* ]]
+    [ $chip == *M1* || $chip == *M2* || $chip == *M3* ]
 }
 
 function install_gmp {
-    if is_macos_aarch; then
-        notice "Installing gmp via Homebrew, if it's not already installed"
-        logged brew list gmp || brew install gmp
+    if [ is_macos ]; then
+        notice "Installing GMP via Homebrew, if it's not already installed"
+        logged brew install gmp
 
-        # on macOS 12 (x86_64), I think homebrew uses different locations
+        # `brew --prefix` is different on macOS 12 and macOS 14
         notice "You may need to add the following environment variables to your '.profile': \n"\
-            "export CPATH=/opt/homebrew/include\n"\
-            "export LIBRARY_PATH=/opt/homebrew/lib\n"
+            "export CPATH=$(brew --prefix)/include\n"\
+            "export LIBRARY_PATH=$(brew --prefix)/lib\n"
+    else
+        notice "Did not install GMP. This script only supports macOS 12 and 14"
     fi
 }
 
+# Installs the two solvers required to run the test suite for the repo.
+# Users may want to install other solvers, and indeed the what4 solvers repo
+# 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 are different URLs for other supported platforms
-        if is_macos_aarch; then
-            what4_solvers_url="https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/macos-14-ARM64-bin.zip"
+        if [ ! is_macos ]; then
+            notice "Did not install what4 solvers. This script only supports macOS 12 and 14"
+            return
+        fi
+
+        if [ is_macos_aarch ]; then
+            solvers_version=$WHAT4_SOLVERS_MACOS_14
+        else
+            # This assumes that developers have read the docs and only run this
+            # script if they're on 12 or 14. This might bork on older versions.
+            solvers_version=$WHAT4_SOLVERS_MACOS_12
         fi
 
         solvers_dir=$(mktemp -d)
-        curl --proto '=https' --tlsv1.2 -sSfL $what4_solvers_url > "$solvers_dir/solvers.bin.zip"
+        curl --proto '=https' --tlsv1.2 -sSfL "$WHAT4_SOLVERS_URL$solvers_version" > "$solvers_dir/solvers.bin.zip"
         cd $solvers_dir
         logged unzip solvers.bin.zip
-        rm solvers.bin.zip
         
         # If we want to install more solvers by default, we can do so here,
         # although we might need a different check than `--version`

From 0413716e45c7bfce5861bd06448256d16b7d8cca Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Fri, 31 May 2024 12:19:02 -0400
Subject: [PATCH 3/7] fix paths and logging in the setup script #1673

---
 .gitignore   |  3 +++
 dev_setup.sh | 31 +++++++++++++++++++------------
 2 files changed, 22 insertions(+), 12 deletions(-)

diff --git a/.gitignore b/.gitignore
index d73c08b7f..206533b60 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,7 +11,10 @@ dist-newstyle
 cabal.project.freeze
 cabal.project.local*
 .vscode/
+
+# artifacts of the setup script
 dev_setup.log
+env.sh
 
 # don't check in generated documentation
 #docs/CryptolPrims.pdf
diff --git a/dev_setup.sh b/dev_setup.sh
index 23c99f895..22cc055c0 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
 
 # cryptol setup script
 #
@@ -14,6 +14,8 @@ set -e
 
 HERE=$(cd `dirname $0`; pwd)
 LOG=$HERE/dev_setup.log
+ROOT=$HERE
+ENV=$ROOT/env.sh
 
 WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212"
 WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT/"
@@ -21,7 +23,7 @@ WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip"
 WHAT4_SOLVERS_MACOS_14="macos-14-ARM64-bin.zip"
 
 function notice {
-    echo -e "[NOTICE] $*"
+    echo "[NOTICE] $*"
 }
 
 # Requires: LOG set to log file path.
@@ -29,8 +31,8 @@ function logged {
     if ! [ -z "$LOG" ]
     then
         mkdir -p `dirname $LOG`
-        echo $* >>$LOG
-        if ! $* >>$LOG 2>&1
+        echo "$@" >>$LOG
+        if ! "$@" >>$LOG 2>&1
         then
             echo
             echo "An error occurred; please see $LOG"
@@ -42,18 +44,18 @@ function logged {
 }
 
 function update_submodules {
-    # todo: change names here
-    cd $HERE
+    cd $ROOT
     notice "Updating submodules"
-    git submodule update --init
+    logged git submodule update --init
 }
 
 function install_ghcup {
     if ! ghcup --version &> /dev/null
     then
         notice "Installing ghcup, GHC, and cabal"
-        # technically the installation only requires cabal, but it's 
-        # recommended to get the whole GCH shebang in one package
+        # 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
     else
         notice "Using existing ghcup installation"
@@ -84,9 +86,10 @@ function install_gmp {
         logged brew install gmp
 
         # `brew --prefix` is different on macOS 12 and macOS 14
-        notice "You may need to add the following environment variables to your '.profile': \n"\
-            "export CPATH=$(brew --prefix)/include\n"\
-            "export LIBRARY_PATH=$(brew --prefix)/lib\n"
+        echo "export CPATH=$(brew --prefix)/include" >> $ENV
+        echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $ENV
+        notice "You may need to source new environment variables added here:\n" \
+            "\$ source $ENV"
     else
         notice "Did not install GMP. This script only supports macOS 12 and 14"
     fi
@@ -126,6 +129,10 @@ function install_what4_solvers {
                 sudo mv $solver /usr/local/bin
             fi
         done
+
+        rm -r $solvers_dir
+    else
+        notice "Not installing cvc4 or cvc5 solvers because they already exist"
     fi
 }
 

From e25afff5191bee1b6bb0670e77e713ebbcaa5e3e Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Mon, 3 Jun 2024 11:21:14 -0400
Subject: [PATCH 4/7] Fix distro and version checks in dev script #1673

- 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
---
 dev_setup.sh | 79 ++++++++++++++++++++++++++++++----------------------
 1 file changed, 46 insertions(+), 33 deletions(-)

diff --git a/dev_setup.sh b/dev_setup.sh
index 22cc055c0..d1b227aea 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -9,19 +9,46 @@
 # environment for cryptol. Any new environment requirements should be
 # added to this script.
 #
+# There is some half-baked support for macOS 12 (x86_64), but it hasn't been
+# tested.
+#
 
 set -e
 
 HERE=$(cd `dirname $0`; pwd)
 LOG=$HERE/dev_setup.log
 ROOT=$HERE
-ENV=$ROOT/env.sh
+
+# Create a new, empty file for environment variables
+VAR_FILE=$ROOT/env.sh
+truncate -s 0 $VAR_FILE
+echo "# Generated environment variables. Manual changes will get clobbered by dev_setup.sh" >> $VAR_FILE
 
 WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212"
 WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT/"
 WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip"
 WHAT4_SOLVERS_MACOS_14="macos-14-ARM64-bin.zip"
 
+MACOS14="macos14"
+MACOS12="macos12"
+# Make sure we're running on a supported platform
+case $(uname -s) in
+    Darwin)
+        if [ $(uname -m) = "arm64" ]; then
+            CRYPTOL_PLATFORM=$MACOS14
+        # This is how we'd support macOS 12. Since this hasn't been tested yet,
+        # we withhold official support.
+        # This might bork on something running macOS <12, since we're basing
+        # the it on the hardware, not the specific version.
+        elif [ $(uname -m) = "x86_64" ]; then
+            CRYPTOL_PLATFORM=$MACOS12
+            echo "Unsupported platform" 2>&1; exit 1;
+        else
+            echo "Unsupported platform" 2>&1; exit 1;
+        fi;;
+    *) echo "Unsupported platform" 2>&1; exit 1;;
+esac
+
 function notice {
     echo "[NOTICE] $*"
 }
@@ -30,6 +57,7 @@ function notice {
 function logged {
     if ! [ -z "$LOG" ]
     then
+        # This may or may not be the same directory that this script lives in.
         mkdir -p `dirname $LOG`
         echo "$@" >>$LOG
         if ! "$@" >>$LOG 2>&1
@@ -63,35 +91,18 @@ function install_ghcup {
 
 }
 
-function is_macos {
-    [ "$OSTYPE" = "darwin"* ]
-}
-
-# Indicate whether this is running macOS on the Apple M series hardware.
-function is_macos_aarch {
-    # Is it running macOS?
-    if [ ! is_macos ]; then
-        return 1
-    fi
-
-    # Does it use an M-series chip?
-    # Actually this command apparently doesn't exist in macOS 12, so this will fail the wrong way
-    chip=$(system_profiler SPHardwareDataType | grep Chip)
-    [ $chip == *M1* || $chip == *M2* || $chip == *M3* ]
-}
-
 function install_gmp {
-    if [ is_macos ]; then
+    if [ $CRYPTOL_PLATFORM = $MACOS12 ] || [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
         notice "Installing GMP via Homebrew, if it's not already installed"
         logged brew install gmp
 
         # `brew --prefix` is different on macOS 12 and macOS 14
-        echo "export CPATH=$(brew --prefix)/include" >> $ENV
-        echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $ENV
+        echo "export CPATH=$(brew --prefix)/include" >> $VAR_FILE
+        echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $VAR_FILE
         notice "You may need to source new environment variables added here:\n" \
-            "\$ source $ENV"
+            "\$ source $VAR_FILE"
     else
-        notice "Did not install GMP. This script only supports macOS 12 and 14"
+        notice "Did not install GMP. This script only supports macOS 14"
     fi
 }
 
@@ -102,21 +113,14 @@ function install_what4_solvers {
     if ! cvc4 --version &> /dev/null || ! cvc5 --version &> /dev/null; then
         notice "Installing cvc4 and/or cvc5 solvers"
 
-        if [ ! is_macos ]; then
-            notice "Did not install what4 solvers. This script only supports macOS 12 and 14"
-            return
-        fi
-
-        if [ is_macos_aarch ]; then
+        if [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
             solvers_version=$WHAT4_SOLVERS_MACOS_14
-        else
-            # This assumes that developers have read the docs and only run this
-            # script if they're on 12 or 14. This might bork on older versions.
+        elif [ $CRYPTOL_PLATFORM = $MACOS12 ]; then
             solvers_version=$WHAT4_SOLVERS_MACOS_12
         fi
 
         solvers_dir=$(mktemp -d)
-        curl --proto '=https' --tlsv1.2 -sSfL "$WHAT4_SOLVERS_URL$solvers_version" > "$solvers_dir/solvers.bin.zip"
+        logged curl --proto '=https' --tlsv1.2 -sSfL -o "$solvers_dir/solvers.bin.zip" "$WHAT4_SOLVERS_URL$solvers_version"
         cd $solvers_dir
         logged unzip solvers.bin.zip
         
@@ -133,6 +137,15 @@ function install_what4_solvers {
         rm -r $solvers_dir
     else
         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"
+            notice "Got: $(grep "cvc4 version" <<< "$(cvc4 --version)")"
+        fi
+        if ! (grep -q "version 1.1.1" <<< "$(cvc5 --version)" ); then
+            notice "Your version of cvc5 is incorrect; expected 1.1.1"
+            notice "Got: $(grep "cvc5 version" <<< "$(cvc5 --version)")"
+        fi
     fi
 }
 

From 0380a45d89fabd1a4fd73a80e5c66df88f9d00e7 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Mon, 3 Jun 2024 16:22:05 -0400
Subject: [PATCH 5/7] consolidate funcs, improve errors in setup script

---
 dev_setup.sh | 98 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 66 insertions(+), 32 deletions(-)

diff --git a/dev_setup.sh b/dev_setup.sh
index d1b227aea..4cb1d9dfe 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -28,31 +28,42 @@ WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212"
 WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT/"
 WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip"
 WHAT4_SOLVERS_MACOS_14="macos-14-ARM64-bin.zip"
+WHAT4_CVC4_VERSION="version 1.8"
+WHAT4_CVC5_VERSION="version 1.1.1"
 
+# Set of supported platforms:
 MACOS14="macos14"
-MACOS12="macos12"
-# Make sure we're running on a supported platform
-case $(uname -s) in
-    Darwin)
-        if [ $(uname -m) = "arm64" ]; then
-            CRYPTOL_PLATFORM=$MACOS14
-        # This is how we'd support macOS 12. Since this hasn't been tested yet,
-        # we withhold official support.
-        # This might bork on something running macOS <12, since we're basing
-        # the it on the hardware, not the specific version.
-        elif [ $(uname -m) = "x86_64" ]; then
-            CRYPTOL_PLATFORM=$MACOS12
-            echo "Unsupported platform" 2>&1; exit 1;
-        else
-            echo "Unsupported platform" 2>&1; exit 1;
-        fi;;
-    *) echo "Unsupported platform" 2>&1; exit 1;;
-esac
+MACOS12="macos12" # actually, this isn't supported yet
+
+# Returns a string indicating the platform (from the set above), or empty if
+# a supported platform is not detected.
+function supported_platform {
+    # Make sure we're running on a supported platform
+    case $(uname -s) in
+        Darwin)
+            if [ $(uname -m) = "arm64" ]; then
+                echo $MACOS14
+            # This is how we'd support macOS 12. Since this hasn't been tested yet,
+            # we withhold official support.
+            # This might bork on something running macOS <12, since we're basing
+            # the it on the hardware, not the specific version.
+            elif [ $(uname -m) = "x86_64" ]; then
+                # CRYPTOL_PLATFORM=$MACOS12
+                echo ""
+            fi;;
+        *) echo ""
+    esac
+}
 
+RED="\033[0;31m"
 function notice {
     echo "[NOTICE] $*"
 }
 
+function is_installed {
+    command -v $* >/dev/null 2>&1
+}
+
 # Requires: LOG set to log file path.
 function logged {
     if ! [ -z "$LOG" ]
@@ -63,9 +74,10 @@ function logged {
         if ! "$@" >>$LOG 2>&1
         then
             echo
-            echo "An error occurred; please see $LOG"
-            echo "Here are the last 50 lines:"
             tail -n 50 $LOG
+            echo
+            echo "[ERROR] An error occurred; please see $LOG"
+            echo "[ERROR] The last 50 lines are printed above for convenience"
             exit 1
         fi
     fi
@@ -78,13 +90,24 @@ function update_submodules {
 }
 
 function install_ghcup {
-    if ! ghcup --version &> /dev/null
+    if ! is_installed ghcup
     then
-        notice "Installing ghcup, GHC, and cabal"
+        ghcup_url="https://get-ghcup.haskell.org"
+        notice "ghcup not found; do you want to install from $ghcup_url"
+        read -p "Press Enter to continue or 'n' to skip: " consent
+        case $consent in
+            [Nn]* ) notice "Skipping ghcup installation"; return;;
+            * ) notice "Installing ghcup";;
+        esac
+
         # 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
+        ghc_dir=$(mktemp -d)
+        logged curl --proto '=https' --tlsv1.2 -sSf -o "$ghc_dir/ghcup.bin" $ghcup_url
+        cd $ghc_dir
+        sh ghcup.bin
+        rm -r $ghc_dir
     else
         notice "Using existing ghcup installation"
     fi
@@ -110,8 +133,8 @@ function install_gmp {
 # Users may want to install other solvers, and indeed the what4 solvers repo
 # 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"
+    if ! is_installed cvc4 || ! is_installed cvc5; then
+        notice "Installing cvc4 and/or cvc5 solvers from $WHAT4_SOLVERS_URL"
 
         if [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
             solvers_version=$WHAT4_SOLVERS_MACOS_14
@@ -124,10 +147,9 @@ function install_what4_solvers {
         cd $solvers_dir
         logged unzip solvers.bin.zip
         
-        # If we want to install more solvers by default, we can do so here,
-        # although we might need a different check than `--version`
+        # If we want to install more solvers by default, we can do so here
         for solver in cvc4 cvc5; do
-            if ! $solver --version &> /dev/null; then 
+            if ! is_installed $solver ; then
                 notice "Installing $solver"
                 chmod u+x $solver
                 sudo mv $solver /usr/local/bin
@@ -138,17 +160,29 @@ function install_what4_solvers {
     else
         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"
+        if ! (grep -q $WHAT4_CVC4_VERSION <<< "$(cvc4 --version)"); then
+            notice "Your version of cvc4 is unexpected; expected $WHAT4_CVC4_VERSION"
             notice "Got: $(grep "cvc4 version" <<< "$(cvc4 --version)")"
+            notice "To ensure compatibility, you might want to uninstall the "\
+                "existing version and re-run this script."
         fi
-        if ! (grep -q "version 1.1.1" <<< "$(cvc5 --version)" ); then
-            notice "Your version of cvc5 is incorrect; expected 1.1.1"
+        if ! (grep -q $WHAT4_CVC5_VERSION <<< "$(cvc5 --version)" ); then
+            notice "Your version of cvc5 is unexpected; expected $WHAT5_CVC5_VERSION"
             notice "Got: $(grep "cvc5 version" <<< "$(cvc5 --version)")"
+            notice "To ensure compatibility, you might want to uninstall the "\
+                "existing version and re-run this script."
         fi
     fi
 }
 
+
+# Make sure script is running on a supported platform
+CRYPTOL_PLATFORM=$(supported_platform)
+if [ -z "$CRYPTOL_PLATFORM" ]; then
+    echo "Unsupported platform"
+    exit 1
+fi
+
 update_submodules
 install_ghcup
 install_gmp

From e03e7be18fea2de31baca97eff7641dab0ba0ffd Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Tue, 4 Jun 2024 07:17:55 -0400
Subject: [PATCH 6/7] simplify ghc install in dev script #1673

- 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
---
 dev_setup.sh | 91 ++++++++++++++++++++++++++++++++--------------------
 1 file changed, 56 insertions(+), 35 deletions(-)

diff --git a/dev_setup.sh b/dev_setup.sh
index 4cb1d9dfe..d6c2f088b 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -7,7 +7,8 @@
 #
 # This script installs everything needed to get a working development
 # environment for cryptol. Any new environment requirements should be
-# added to this script.
+# added to this script. This script is not interactive but it may define
+# some environment variables that need to be loaded after it runs.
 #
 # There is some half-baked support for macOS 12 (x86_64), but it hasn't been
 # tested.
@@ -35,6 +36,8 @@ WHAT4_CVC5_VERSION="version 1.1.1"
 MACOS14="macos14"
 MACOS12="macos12" # actually, this isn't supported yet
 
+USED_BREW=false
+
 # Returns a string indicating the platform (from the set above), or empty if
 # a supported platform is not detected.
 function supported_platform {
@@ -48,7 +51,6 @@ function supported_platform {
             # This might bork on something running macOS <12, since we're basing
             # the it on the hardware, not the specific version.
             elif [ $(uname -m) = "x86_64" ]; then
-                # CRYPTOL_PLATFORM=$MACOS12
                 echo ""
             fi;;
         *) echo ""
@@ -61,7 +63,7 @@ function notice {
 }
 
 function is_installed {
-    command -v $* >/dev/null 2>&1
+    command -v "$@" >/dev/null 2>&1
 }
 
 # Requires: LOG set to log file path.
@@ -90,26 +92,25 @@ function update_submodules {
 }
 
 function install_ghcup {
-    if ! is_installed ghcup
-    then
-        ghcup_url="https://get-ghcup.haskell.org"
-        notice "ghcup not found; do you want to install from $ghcup_url"
-        read -p "Press Enter to continue or 'n' to skip: " consent
-        case $consent in
-            [Nn]* ) notice "Skipping ghcup installation"; return;;
-            * ) notice "Installing ghcup";;
-        esac
-
-        # 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.
-        ghc_dir=$(mktemp -d)
-        logged curl --proto '=https' --tlsv1.2 -sSf -o "$ghc_dir/ghcup.bin" $ghcup_url
-        cd $ghc_dir
-        sh ghcup.bin
-        rm -r $ghc_dir
+    if ! is_installed ghcup; then
+        notice "Installing GHC toolchain via GHCup"
+        # Manually install Haskel toolchain. If this doesn't work, try
+        # using the install script at https://www.haskell.org/ghcup/
+        if [ $CRYPTOL_PLATFORM = $MACOS12 ] || [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
+            logged brew install ghcup
+            USED_BREW=true
+        else
+            notice "Did not install GHCup. This script only supports macOS 14"
+        fi
+
+        logged ghcup install ghc --set recommended
+        logged ghcup install cabal --set recommended
+        logged ghcup install stack --set recommended
+        logged ghcup install hls --set recommended
+        logged cabal update
     else
-        notice "Using existing ghcup installation"
+        notice "Using existing GHCup installation, and assuming that if you"\
+            "have GHCup, you also have the rest of the Haskell toolchain"
     fi
 
 }
@@ -118,12 +119,7 @@ function install_gmp {
     if [ $CRYPTOL_PLATFORM = $MACOS12 ] || [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
         notice "Installing GMP via Homebrew, if it's not already installed"
         logged brew install gmp
-
-        # `brew --prefix` is different on macOS 12 and macOS 14
-        echo "export CPATH=$(brew --prefix)/include" >> $VAR_FILE
-        echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $VAR_FILE
-        notice "You may need to source new environment variables added here:\n" \
-            "\$ source $VAR_FILE"
+        USED_BREW=true
     else
         notice "Did not install GMP. This script only supports macOS 14"
     fi
@@ -132,7 +128,16 @@ function install_gmp {
 # Installs the two solvers required to run the test suite for the repo.
 # Users may want to install other solvers, and indeed the what4 solvers repo
 # includes a half dozen other solvers that are compatible with cryptol. 
-function install_what4_solvers {
+function install_solvers {
+
+    # Install the latest z3
+    if ! is_installed z3; then
+        notice "Installing z3 solver via Homebrew"
+        logged brew install z3
+        USED_BREW=true
+    fi
+
+    # Install other solvers using the cryptol-approved set of binaries
     if ! is_installed cvc4 || ! is_installed cvc5; then
         notice "Installing cvc4 and/or cvc5 solvers from $WHAT4_SOLVERS_URL"
 
@@ -156,25 +161,40 @@ function install_what4_solvers {
             fi
         done
 
+        cd $HERE
         rm -r $solvers_dir
     else
         notice "Not installing cvc4 or cvc5 solvers because they already exist"
 
-        if ! (grep -q $WHAT4_CVC4_VERSION <<< "$(cvc4 --version)"); then
+        # Make sure the installed versions are the versions that have been tested
+        version_file=$(mktemp)
+        cvc4 --version > $version_file
+        if ! (grep -q "$WHAT4_CVC4_VERSION" $version_file); then
             notice "Your version of cvc4 is unexpected; expected $WHAT4_CVC4_VERSION"
-            notice "Got: $(grep "cvc4 version" <<< "$(cvc4 --version)")"
+            notice "Got: $(grep 'cvc4 version' $version_file)"
             notice "To ensure compatibility, you might want to uninstall the "\
                 "existing version and re-run this script."
         fi
-        if ! (grep -q $WHAT4_CVC5_VERSION <<< "$(cvc5 --version)" ); then
-            notice "Your version of cvc5 is unexpected; expected $WHAT5_CVC5_VERSION"
-            notice "Got: $(grep "cvc5 version" <<< "$(cvc5 --version)")"
+        cvc5 --version > $version_file
+        if ! (grep -q "$WHAT4_CVC5_VERSION" $version_file); then
+            notice "Your version of cvc5 is unexpected; expected $WHAT4_CVC5_VERSION"
+            notice "Got: $(grep "cvc5 version" $version_file)"
             notice "To ensure compatibility, you might want to uninstall the "\
                 "existing version and re-run this script."
         fi
     fi
 }
 
+function put_brew_in_path {
+    if $USED_BREW; then
+        # `brew --prefix` is different on macOS 12 and macOS 14
+        echo "export CPATH=$(brew --prefix)/include" >> $VAR_FILE
+        echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $VAR_FILE
+        notice "You may need to source new environment variables added here:\n" \
+            "\$ source $VAR_FILE"
+    fi
+}
+
 
 # Make sure script is running on a supported platform
 CRYPTOL_PLATFORM=$(supported_platform)
@@ -186,4 +206,5 @@ fi
 update_submodules
 install_ghcup
 install_gmp
-install_what4_solvers
+install_solvers
+put_brew_in_path
\ No newline at end of file

From 4a7f0a8513ccb3ad9f31429e43b73fd1d94b6c1d Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 5 Jun 2024 08:36:52 -0400
Subject: [PATCH 7/7] use specific ghc/cabal versions in dev setup #1673

---
 dev_setup.sh | 30 ++++++++++++++++++------------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/dev_setup.sh b/dev_setup.sh
index d6c2f088b..45a0a7f01 100755
--- a/dev_setup.sh
+++ b/dev_setup.sh
@@ -25,6 +25,9 @@ VAR_FILE=$ROOT/env.sh
 truncate -s 0 $VAR_FILE
 echo "# Generated environment variables. Manual changes will get clobbered by dev_setup.sh" >> $VAR_FILE
 
+GHC_VERSION="9.4.8"
+CABAL_VERSION="3.10.3.0"
+
 WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212"
 WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT/"
 WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip"
@@ -93,7 +96,7 @@ function update_submodules {
 
 function install_ghcup {
     if ! is_installed ghcup; then
-        notice "Installing GHC toolchain via GHCup"
+        notice "Installing GHCup via Homebrew"
         # Manually install Haskel toolchain. If this doesn't work, try
         # using the install script at https://www.haskell.org/ghcup/
         if [ $CRYPTOL_PLATFORM = $MACOS12 ] || [ $CRYPTOL_PLATFORM = $MACOS14 ]; then
@@ -102,15 +105,17 @@ function install_ghcup {
         else
             notice "Did not install GHCup. This script only supports macOS 14"
         fi
-
-        logged ghcup install ghc --set recommended
-        logged ghcup install cabal --set recommended
-        logged ghcup install stack --set recommended
-        logged ghcup install hls --set recommended
-        logged cabal update
     else
-        notice "Using existing GHCup installation, and assuming that if you"\
-            "have GHCup, you also have the rest of the Haskell toolchain"
+        notice "Using existing GHCup installation"
+    fi
+
+    notice "Installing ghc and cabal via GHCup"
+    logged ghcup install ghc $GHC_VERSION
+    logged ghcup install cabal $CABAL_VERSION
+    logged ~/.ghcup/bin/cabal-$CABAL_VERSION update
+
+    if ! is_installed ghc || ! is_installed cabal; then
+        echo "export PATH=$PATH:~/.ghcup/bin" >> $VAR_FILE
     fi
 
 }
@@ -190,8 +195,6 @@ function put_brew_in_path {
         # `brew --prefix` is different on macOS 12 and macOS 14
         echo "export CPATH=$(brew --prefix)/include" >> $VAR_FILE
         echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $VAR_FILE
-        notice "You may need to source new environment variables added here:\n" \
-            "\$ source $VAR_FILE"
     fi
 }
 
@@ -207,4 +210,7 @@ update_submodules
 install_ghcup
 install_gmp
 install_solvers
-put_brew_in_path
\ No newline at end of file
+put_brew_in_path
+
+notice "You may need to source new environment variables added here:\n" \
+    "\$ source $VAR_FILE"