chore(install_macos.sh): Don't overwrite existing vscode (#18300)

If this script is run without sudo and VSCode is already installed, it seems to break VSCode.  There's no need to install it VSCode if it's already installed, in any case.

(We could do the same with elan, I'm less sure about the tradeoffs there.)




Co-authored-by: Jason Gross <[email protected]>

scripts/install_macos.sh

@@ -14,17 +14,22 @@ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf
 elan toolchain install stable
 elan default stable
 
-# Install the universal darwin build of VS Code
-curl -L https://update.code.visualstudio.com/latest/darwin-universal/stable -o ~/Downloads/VSCode-darwin-universal.zip
+# Check if VS Code is available on the command line
+if ! command -v code &> /dev/null; then
+    # Install the universal darwin build of VS Code
+    curl -L https://update.code.visualstudio.com/latest/darwin-universal/stable -o ~/Downloads/VSCode-darwin-universal.zip
 
-# Unzip the downloaded file to the Applications folder
-unzip -o ~/Downloads/VSCode-darwin-universal.zip -d /Applications
+    # Unzip the downloaded file to the Applications folder
+    unzip -o ~/Downloads/VSCode-darwin-universal.zip -d /Applications
 
-# Add the VS Code binary to the PATH to enable launching from the terminal
-cat << EOF >> ~/.zprofile
+    # Add the VS Code binary to the PATH to enable launching from the terminal
+    cat >> ~/.zprofile << EOF
 # Add Visual Studio Code (code)
 export PATH="\$PATH:/Applications/Visual Studio Code.app/Contents/Resources/app/bin"
 EOF
+else
+    echo "VS Code is already installed."
+fi
 
 # Install the Lean4 VS Code extension
 code --install-extension leanprover.lean4