From 2ca4188fc3d1da0346988120447999471505969a Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Thu, 23 Sep 2021 11:52:32 -0700 Subject: [PATCH] doc: somehow wsl2.md was created so the page on https://leanprover.github.io/lean4/doc/make/wsl2.html is empty. This fixes that. --- doc/SUMMARY.md | 2 +- doc/dev/index.md | 2 +- doc/make/wsl.md | 12 +++++------- doc/make/wsl2.md | 1 - 4 files changed, 7 insertions(+), 10 deletions(-) delete mode 100644 doc/make/wsl2.md diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index f2bc424987..b3ffcc726f 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -61,7 +61,7 @@ - [Ubuntu Setup](./make/ubuntu-16.04.md) - [macOS Setup](./make/osx-10.9.md) - [Windows MSYS2 Setup](./make/msys2.md) - - [Windows with WSL](./make/wsl2.md) + - [Windows with WSL](./make/wsl.md) - [Nix Setup (*Experimental*)](./make/nix.md) - [Unit Testing](./dev/testing.md) - [Building This Manual](./dev/mdbook.md) diff --git a/doc/dev/index.md b/doc/dev/index.md index a0976dbcc1..7a8dc48d16 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md @@ -4,7 +4,7 @@ - [Ubuntu Setup](../make/ubuntu-16.04.md) - [macOS Setup](../make/osx-10.9.md) - [Windows MSYS2 Setup](../make/msys2.md) - - [Windows with WSL](../make/wsl2.md) + - [Windows with WSL](../make/wsl.md) - [Nix Setup (*Experimental*)](../make/nix.md) - [Unit Testing](./testing.md) - [Building This Manual](./mdbook.md) diff --git a/doc/make/wsl.md b/doc/make/wsl.md index 894140a1a8..76669b60a2 100644 --- a/doc/make/wsl.md +++ b/doc/make/wsl.md @@ -27,20 +27,18 @@ into the WSL using: `Install in WSL: Ubuntu` Type `Ctrl+Shift+P` and select `Remote-WSL: Open Folder in WSL...` to open a folder containing your hello world lean package. -When everything is working you should see this: +When everything is working you should see something like this with a +functioning infoview, syntax coloring and tooltips: ![screenshot](../images/code-wsl.png) -with a functioning infoview, syntax coloring and tooltips. ## Troubleshooting -**Connection to server is erroring. Shutting down server.** +**lean4: Could not find Lean version by running 'lean --version'.** -If your `leanpkg` has a `build` folder try deleting it. Lean .olean -binaries are not cross platform so if the binaries were copied from a -different platform they need to be deleted so that the new build is -created for your platform. +Check that the `lean` program is available in your PATH in your WSL +environment. **Logs are showing up with a windows file path** diff --git a/doc/make/wsl2.md b/doc/make/wsl2.md deleted file mode 100644 index f86b60582c..0000000000 --- a/doc/make/wsl2.md +++ /dev/null @@ -1 +0,0 @@ -# Windows with WSL