4
$\begingroup$

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

Update: I got it figured out. Should I share?

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ 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.) $\endgroup$
    – Jason Rute
    Commented May 3, 2023 at 10:01
  • 1
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented May 11, 2023 at 6:55
  • 2
    $\begingroup$ 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. $\endgroup$
    – blackbirdsr
    Commented Sep 14, 2023 at 20:59
  • $\begingroup$ @blackbirdsr Where are you in the process? Have you set up lean with VS Code? $\endgroup$
    – Alex Byard
    Commented Sep 18, 2023 at 23:27
  • $\begingroup$ @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. $\endgroup$
    – Alex Byard
    Commented Sep 19, 2023 at 0:33

1 Answer 1

Reset to default
2
$\begingroup$

Here's how I go about setting up a project. This information can be found in the Lean documentation. In a terminal go to the folder you want to create your project in. We'll call this project my_project. In your terminal run

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

The date here doesn't need to be changed. The math keyword adds mathlib4 to the dependencies of the project so that you can 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. Launch VS Code by writing code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.

The documentation is here.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Can you also provide a link to the relevant documentation? Give how much Lean 4 is still in flux, it may change in the future and it is good to have a stable link to the latest instructions. $\endgroup$
    – Jason Rute
    Commented Sep 20, 2023 at 12:26
  • $\begingroup$ @JasonRute I read your profile... How does computability relate to analysis? I am a pure mathematician at heart. Documentation added btw. $\endgroup$
    – Alex Byard
    Commented Sep 21, 2023 at 8:01

Not the answer you're looking for? Browse other questions tagged or ask your own question.