doc: minor adjustments to manual and setup guide (#564)

Adds a note about disabling automatic hovers to the manual and notes
about antivirus software, adding `brew` to the PATH and network drives
or cloud storage to the setup guide.

Closes #533.

Author: mhuisi

vscode-lean4/manual/manual.md

@@ -343,6 +343,8 @@ When hovering over parts of the code with the mouse pointer, VS Code will displa
 1. **Errors, warnings and information**. When hovering over a piece of code that is [underlined with a squiggly line](#errors-warnings-and-information), VS Code will display the error, warning or information associated with the squiggly line.
 1. **Unicode symbols**. When hovering over a unicode symbol, VS Code will provide all available [abbreviation identifiers](#unicode-input) to input the symbol.
 
+Automatic hovers can be disabled by un-ticking the 'Editor › Hover: Enabled' configuration option. This is especially helpful when presenting Lean 4 code to an audience.
+
 Hovers can also be triggered at the current text cursor position using the keyboard with the `Ctrl+K Ctrl+I` (`Cmd+K Cmd+I`) [chord](#chords) or the ['Show or Focus Hover'](command:editor.action.showHover) command.
 
 Moving the mouse away from the hover popup panel will immediately collapse it. Clicking on the hover popup panel will pin it so that it remains open when the mouse is moved away from the hover popup panel.

vscode-lean4/media/guide-help.md

@@ -1,3 +1,10 @@
+## Antivirus Software
+Some users have reported that overly aggressive antivirus software will interfere with all secure network connections in certain Lean commands, leading to errors like the following:
+```
+curl: (35) schannel: next InitializeSecurityContext failed: Unknown error (0x80092012) - The revocation function was unable to check revocation for the certificate
+```
+If you encounter this issue, you can try disabling your antivirus, re-run the command that failed and re-enable it afterwards. If you are uncomfortable with disabling your antivirus software altogether, you can also try disabling the specific antivirus feature that is typically causing these issues, commonly known as 'encrypted connection scanning' or 'HTTPS scanning'. You can disable HTTPS scanning as follows in certain common antivirus software: [Kaspersky](https://support.kaspersky.com/KESWin/11.6.0/en-US/175124.htm), [AVG](https://support.avg.com/SupportArticleView?l=en&urlName=Use-AVG-Antivirus-HTTPS-scan&supportType=home), [Avast](https://support.avast.com/en-us/article/use-antivirus-https-scan/#pc).
+
 ## Collecting VS Code Output
 If you are encountering an issue with Lean or this VS Code extension, copying the output from the 'Troubleshooting: Show Setup Information' and 'Troubleshooting: Show Output' commands can be helpful for others who are trying to help you. 
 You can run these commands by clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Setup Information' and 'Troubleshooting: Show Output'.

vscode-lean4/media/guide-installDeps-mac.md

@@ -6,7 +6,7 @@
 ## Installing Required Dependencies
 1. [Open a new terminal](command:workbench.action.terminal.new).
 2. Type in `/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"` and press Enter to install [Homebrew](https://brew.sh/), a package manager for macOS.
-3. Follow the instructions in the terminal.
+3. Follow the instructions in the terminal. Make sure to add `brew` to your PATH as instructed.
 4. Type in `brew install curl git` and press Enter.
 5. Wait until the installation has completed.
 

vscode-lean4/media/guide-setupProject.md

@@ -1,5 +1,5 @@
 ## Creating a Project
-Below, you will find links that create new projects or download projects for you. After creating or downloading a project, you can re-open the project in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created.  
+Below, you will find links that create new projects or download projects for you. After creating or downloading a project, you can re-open the project in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created. If possible, you should avoid creating projects on network drives or in directories indexed by cloud storage, e.g. OneDrive.
 Completing the project creation process and choosing to open the new project will close this guide. You can re-open it later by clicking the ∀-symbol in the top right and selecting 'Documentation…' > 'Docs: Show Setup Guide'.
 
   ![∀-symbol buttons](open-local-project_show-setup_buttons.png)