moving files in mathlib

Stream: new members

[Emily Riehl]

I'm working on a PR (by request) that moves a few files into an existing folder in mathlib. I've moved all the files to where they belong on my local branch and run lake exe mk_all. The file list in Mathlib.lean looks correct.

But when I try to run lake build I get an immediate error

error: no such file or directory (error code: 2)
  file: ././././Mathlib/AlgebraicTopology/SimplicialSet.lean

This is one of the files that was moved so indeed it is not there anymore.

I suspect there is some import of this file I missed updating. But the error doesn't tell me which file is generating the error. Can I search somehow for which files import a specific file? Or is there some way to query this error message to see where it came from?

[Yaël Dillies]

Did you run lake exe mk_all?

[Yaël Dillies]

I suspect you didn't, in which case Mathlib.lean will still contain a line with import Mathlib.AlgebraicTopology.SimplicialSet

[Yaël Dillies]

In general, you can grep (= Ctrl + F throughout a project) for import Mathlib.AlgebraicTopology.SimplicialSet to see where it is imported

[Emily Riehl]

I had run lake exe mk_all

[Emily Riehl]

I figured out the issue though: I had manually updated the imports of some files but then not rebuilt all the files (by clicking the button in the infoview in vscode). After I did that lake build works.

[Damiano Testa]

I don't know if this is the issue, but lake exe mk_all modifies only the "import-all" files (typically, Mathlib.lean and Mathlib/Tactic.lean). If you moved files around, then it should generate the correct "import all" files, but it will not modify the individual import XX statements within any other file.

[Yaël Dillies]

Emily Riehl said:

I figured out the issue though: I had manually updated the imports of some files but then not rebuilt all the files (by clicking the button in the infoview in vscode). After I did that lake build works.

That... shouldn't happen. What you rebuild from the infoview has no incidence on what lake build does (someone tell me if I'm wrong)