[docs] Simplify README unix setup instructions

README.md

@@ -6,37 +6,36 @@ Simple real-time Doom-style raycasting engine in Lean4:
 
 ![Screenshot](screenshots/screenshot1.png)
 
-## Cloning
-
-When you clone, MAKE SURE YOU RUN ``git submodule update --init --recursive`` IN THE ROOT OF THIS REPOSITORY JUST TO BE SAFE
-
 ## Run
 
-This is just an experiment
-
-First, make sure you've set up Lean properly on your computer.
-
-If you are on Windows, use MSYS2 or WSL 
-
-IMPORTANT: FOR MSYS2, MAKE SURE YOU ARE USING THE "CLANG" SHELL TO RUN EVERYTHING
-
-(For more information on MSYS2, see: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md)
-
-Follow the "legacy" instructions from here (They should work on Linux, WSL, and MSYS2): https://leanprover-community.github.io/install/linux.html
-
-Second, make sure you run the build script first to build all the dependencies to get this to work
+### Unix (Linux, Mac)
 
 ```bash
+# Install elan if this is your first time using Lean
+curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
+
+# Clone project and submodules (SDL3 etc)
+git clone --recurse-submodules https://github.com/ValorZard/LeanDoomed.git
+cd LeanDoomed
+
+# Build dependencies
 chmod +x ./build_sdl_and_friends.sh
 sudo ./build_sdl_and_friends.sh
-```
 
-Then you can run the game proper
-
-```bash
+# Run the "game"
 lake exe LeanDoomed
 ```
 
+### Windows (MSYS2 or WSL)
+
+On Windows, use MSYS2 or WSL!
+
+**IMPORTANT**: FOR MSYS2, MAKE SURE YOU ARE USING THE "CLANG" SHELL TO RUN EVERYTHING!
+
+For more information on MSYS2, see: https://github.com/leanprover/lean4/blob/master/doc/make/msys2.md
+
+Next, follow the instructions for Unix above.
+
 ## License
 
 MIT