doc: replace quickstart leanpkg info with info about lake.

[lovettchris]

time to tell folks how to use lake.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[Kha]

I've cherry-picked the resolved parts onto master in c3a9860.

[lovettchris]

I've cherry-picked the resolved parts onto master in c3a9860.

@Kha , rats, I really wanted to get rid of the user having to manually run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh which is not needed if you just start with the VS code extension and let it do that for you.

[lovettchris]

I agree, see updated quickstart.md

[Kha]

Great! Happy to merge as soon as the fix is deployed.

[lovettchris]

Yes, see https://github.com/lovettchris/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx#L57 From: Sebastian Ullrich ***@***.***> Sent: Friday, January 21, 2022 1:12 AM To: leanprover/lean4 ***@***.***> Cc: Chris Lovett ***@***.***>; Mention ***@***.***> Subject: Re: [leanprover/lean4] doc: replace quickstart leanpkg info with info about lake. (PR #842) @Kha commented on this pull request.

________________________________ In doc/quickstart.md<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fleanprover%2Flean4%2Fpull%2F842%23discussion_r789479527&data=04%7C01%7Cclovett%40microsoft.com%7C9632301f3f824ce5903f08d9dcbe1b2c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637783531325652688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=klBr7YXrOsFoPYgOh2KVW94I7KbFoeHUF31Ni9stA6g%3D&reserved=0>:

Note: Packages **have** to be opened using "File > Open Folder..." for imports to work. Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`). + +## Troubleshooting + +**The InfoView says "Waiting for Lean server to start..." forever.** + +Check that the VS Code Terminal is not prompting you with `Press ENTER key to start Lean:`. If so click in the terminal window and pressthe ENTER key. Do we still have such prompts? - Reply to this email directly, view it on GitHub<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fleanprover%2Flean4%2Fpull%2F842%23pullrequestreview-859278398&data=04%7C01%7Cclovett%40microsoft.com%7C9632301f3f824ce5903f08d9dcbe1b2c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637783531325652688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=oHUYrAJhVgQG0FOHODXCwqUI50dMGAqzijt4UsddMdM%3D&reserved=0>, or unsubscribe<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAEOXFKQREQS5DBZ6CAXATH3UXEPOVANCNFSM5JISPJAQ&data=04%7C01%7Cclovett%40microsoft.com%7C9632301f3f824ce5903f08d9dcbe1b2c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637783531325652688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=pL9EuQjcEBejdKfs%2FEboUIFbcFRqb9s3bkcpOiyysdI%3D&reserved=0>. Triage notifications on the go with GitHub Mobile for iOS<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7Cclovett%40microsoft.com%7C9632301f3f824ce5903f08d9dcbe1b2c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637783531325652688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=KmZF%2FNtCFJx5ZHJH2LZFkzTsEyeks7t9azF3kJ2SSq0%3D&reserved=0> or Android<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7Cclovett%40microsoft.com%7C9632301f3f824ce5903f08d9dcbe1b2c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637783531325652688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=fUIwMHLFo5YMMhF2j5zaQiUsMUGgndfqKcuhkOt84lA%3D&reserved=0>. You are receiving this because you were mentioned.Message ID: ***@***.******@***.***>>

[Kha]

Yes, see https://github.com/lovettchris/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx#L57

No, I meant the "Press ENTER key to start Lean" part.

[Kha]

I see the prompt is still there in vscode-lean4, but I'm not entirely sure about its purpose

[lovettchris]

Ah, yes, I was going to remove it by auto-exiting the process, then I wondered about "error conditions", if the elan install fails there will be an error message in that output window, and if I auto-close it the user won't know why it failed...

[Kha]

Then, should we restrict it to non-zero exit codes from the installer?