From 7de11d2aa3d3f57232ef1790b882a28783c95227 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 7 Apr 2021 14:50:36 +0200 Subject: [PATCH] doc: quickstart: beware the Windows --- doc/quickstart.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/quickstart.md b/doc/quickstart.md index a6affce58a..2543ef6b79 100644 --- a/doc/quickstart.md +++ b/doc/quickstart.md @@ -8,6 +8,7 @@ See [Setup](./setup.md) for other ways and more details on setting up Lean. $ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly ``` See the `elan` link above for other installation options and details. +Note that using Lean with multi-file projects on Windows currently comes with some [additional limitations](./setup.md#leanpkg). 1. Install [VS Code](https://code.visualstudio.com/). 1. Open VS Code and install the `lean4` extension. ![installing the vscode-lean4 extension](images/code-ext.png)