VS Code Welcome Page for Lean

Stream: general

[Hunter Monroe]

We are designing a VS Code welcome page (similar to those for the Python extension or VS Code itself), and would appreciate feedback on this proposal: there would be sections to: (1) Load Tutorials, Theorem Proving in Lean, Mathematics in Lean, Logic and Proof, Hitchhikers Guide to Logical Verification projects, or any project entered by the user, into a default or user chosen directory; (2) Create a new standalone project and push to github if desired; and (3) Contribute to mathlib following the shiny lemma instructions. There would be an option to not show the welcome page again, and a Ctrl-Shift-P command to make it reappear. The extension already has a "Lean: Open Documentation View" which (1) can draw on. The Python extension welcome page is here: VSCodePythonWelcome.png An end goal could be a three step install of Github for Windows; VS Code; and the Lean extension, and then the extension could install elan (functionality already there since v0.12) and leanproject.exe (which we can now build by continuous integration, removing the need to install Python). If the user clones or opens a github repository for a Lean project not using the welcome page above, the extension could offer to run elan/leanproject/add mathlib if needed. Your feedback is welcome.