Update README.md

README.md

@@ -43,10 +43,10 @@ ______________________________________________________________________
 ## Requirements
 
 * A working setup of [Lean 4](https://lean-lang.org/), including [elan](https://github.com/leanprover/elan) and [Lean's VSCode extension](https://lean-lang.org/lean4/doc/quickstart.html)
-* The latest version of [Z3](https://github.com/Z3Prover/z3) and [CVC5](https://cvc5.github.io/)
-* Install Python dependencies: `pip install smt-portfolio`
-* Optional: If you want to build the blueprint locally: `pip install leanblueprint`
-* Optional: If you want to run autoformalization experiments using GPT-4: `pip install openai`
+* Install the latest version of [Z3](https://github.com/Z3Prover/z3) and [CVC5](https://cvc5.github.io/) and make sure they can be accessed from the command line
+* Install Python dependencies: `pip install smt-portfolio leanblueprint openai`
+* Find out the location of `smt-portfolio` and make sure Lean's VSCode extension can also access it. For example, if `which smt-portfolio` outputs `/Users/yangky/miniconda3/envs/lean/bin/smt-portfolio`, you should set `Server Env Paths` in Lean's VSCode extension as below:
+<img width="938" alt="image" src="https://github.com/loganrjmurphy/LeanEuclid/assets/5431913/abfc6d25-e2e4-462e-934d-a10b4cb4e96c">