Update install_macos.sh #6390
Closed
Update install_macos.sh #6390
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The basic Mac installation of VS Code does not add it to the PATH.
agjftucker
added
the
awaiting-review
ocfnash
reviewed
Aug 24, 2023
| @@ -16,9 +16,8 @@ elan toolchain install stable | |||
| elan default stable | |||
|
|
|||
| # Install and configure VS Code | |||
| if ! which code > /dev/null; then | |||
| if ! "/Applications/Visual Studio Code.app/Contents/Resources/app/bin/code" --install-extension leanprover.lean4; then | |||
There was a problem hiding this comment.
Suggested change
| if ! "/Applications/Visual Studio Code.app/Contents/Resources/app/bin/code" --install-extension leanprover.lean4; then | |
| if ! "/Applications/Visual Studio Code.app/Contents/Resources/app/bin/code" --install-extension leanprover.lean4 > /dev/null; then |
| brew install --cask visual-studio-code | ||
| # Install the Lean4 VS Code extension | ||
| code --install-extension leanprover.lean4 |
There was a problem hiding this comment.
Shouldn't we also provide the full path here?
Suggested change
| code --install-extension leanprover.lean4 | |
| "/Applications/Visual Studio Code.app/Contents/Resources/app/bin/code" --install-extension leanprover.lean4 |
Given this I guess we should capture this in a variable above.
ocfnash
added
awaiting-author
|
@agjftucker Did you close this because we were too slow reviewing? If so, I'm sorry! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The basic download-and-drag installation of VS Code does not add it to the PATH. So this commit calls it with its full pathname.
This script-driven install is the one advocated on the leanprover-community website and I am trying to make it a little smoother. It should work for both Intel and M1-based Macs and it would be great if the install page were to change to reflect that (see here). However I don't really understand why we diverge at all from the approach described in the Lean manual.