importing own files in Lean projects

Stream: lean4

[Anthony Bordg]

Assume I started a project my_project, using mathlib 4 as a dependency, with two new files my_project/MyProject/fileA.lean and my_project/MyProject/fileB.lean, and I want to import fileA in fileB with import MyProject.fileA.
What has to be done before running the command import MyProject.fileA properly? I guess the file fileA should be built, but how? I don't see instructions in the Lean projects section of the Lean Community webpage.

[Kevin Buzzard]

It should just work out of the box. What's happening for you?

[Kevin Buzzard]

lake build will by default build every file imported in MyProject.lean (see mathlib for a huge example of such a file)

[Anthony Bordg]

Kevin Buzzard said:

It should just work out of the box. What's happening for you?

I have the following error Imports are out of date and must be rebuilt; use the "Restart File" command in your editor..

[Ruben Van de Velde]

Follow the instruction :)

[Anthony Bordg]

I eventually found the Restart File command :)