Difference between import tactic and import mathlib.

Stream: new members

[Mattia Bottoni]

Hi everybody

When I was solving the formalising mathematics project (https://github.com/ImperialCollegeLondon/formalising-mathematics-2023), I saw that every exercise sheet started with "import tactic". I wanted to write similar exercise sheets so I started my own project with the guidelines from the official Lean page (https://leanprover-community.github.io/install/project.html). When I did this, I was not able to import the tactic package, only packages starting with “mathlib.”. I compared my project to the projects that could import “tactic” and I saw that these projects all contained a folder called “_target”, whereas my project did not. Is there any possibility of starting your own project containing that folder “_target”? I would really appreciate it if that would be possible because I prefer the proofwriting style with the “tactic” package. Thanks to all of you in advance!
All the best
Matt

P.S. @Elif Sacikara (Alumni) would also like to know the answer to this.

[Patrick Massot]

We very recently went across a major backward-incompatible change of version in Lean. The project https://github.com/ImperialCollegeLondon/formalising-mathematics-2023 is using Lean 3 which is fully obsolete. The instructions you followed are about Lean 4.

[Patrick Massot]

We are well aware the current situation can be rather confusing for outsiders, and we are sorry about that.

[Patrick Massot]

See https://leanprover-community.github.io/learn.html for links to current learning resources.

[Mattia Bottoni]

Thank you very much for your fast reply!
This helped a lot :)