Timeline for Lean 4 Importing into VSCode
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 20, 2023 at 2:47 | vote | accept | Alex Byard | ||
| Sep 20, 2023 at 2:47 | answer | added | Alex Byard | timeline score: 2 | |
| Sep 19, 2023 at 0:33 | comment | added | Alex Byard |
@blackbirdsr Here's how I set up a project: In a terminal go to the folder you want to create your project folder my_project inside. Run lake +leanprover/lean4:nightly-2023-02-04 new my_project math. The math keyword adds mathlib4 to the dependencies of your project, so that you can use import Mathlib in your project files. Go inside the my_project folder and run lake update, then lake exe cache get, and then mkdir MyProject. Run VS Code by running code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.
|
|
| Sep 18, 2023 at 23:27 | comment | added | Alex Byard | @blackbirdsr Where are you in the process? Have you set up lean with VS Code? | |
| Sep 14, 2023 at 20:59 | comment | converted from answer | blackbirdsr | I'm new to stackexchange so sorry if writing this counts as 'necro' or is in some other way inappropiate. Could you please share how you managed to import mathlib4? I'm having the same problem you were having. Thanks in advance. | |
| May 11, 2023 at 6:55 | comment | added | Andrej Bauer | As the question stands, it's quite uninformative ("There's a student with a problem."). I would recommend that you not only share the solution, but also what was confusing to you. | |
| May 10, 2023 at 18:49 | history | edited | Alex Byard | CC BY-SA 4.0 |
added 49 characters in body
|
| May 4, 2023 at 15:36 | history | edited | Alex Byard | CC BY-SA 4.0 |
added 169 characters in body
|
| May 3, 2023 at 10:01 | comment | added | Jason Rute | See here: github.com/leanprover-community/…. (In particular see the end about if you already have a project and what to use mathlib 4 as a dependency.) | |
| May 3, 2023 at 0:38 | history | asked | Alex Byard | CC BY-SA 4.0 |