Multiple top-level source directories

Stream: lean4

[Alex Sweeney]

I'm trying to set up a lean project like a monorepo, kinda like Mathlib I guess but hopefully less complicated. I'm reading through the FPIL book and watching the new videos for Lean for the Curious Mathematician and I have a directory for notes for each. I want all files in both directories to have access to Mathlib but I'm having trouble making it work with my project structure.

├── build
├── lake-packages
├── Functional Programming in Lean
│   ├── 5.0
│   ├── 5.1
│   └── 5.2
├── Lean for the Curious Mathematician
│   └── Structures and Classes.lean
└── lakefile.lean

This is what I've tried adding to the lakefile but my source files still can't see Mathlib

lean_lib «Functional Programming in Lean» {
  roots := #[`«Functional Programming in Lean»]
}

Also I would prefer if I didn't need to have a top-level lean file of the same name that imports every new file, but I can't get that to work either anyway. I want to be able to create a new file and have it see Mathlib without any extra work. Is this possible with Lake?

[Mario Carneiro]

That folder hierarchy should work. You should just add globs := #[.submodules `«Functional Programming in Lean»] to the «Functional Programming in Lean» lib, and your LFTCM lean lib will look similar.

[Alex Sweeney]

I now have

import Lake
open Lake DSL

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

package «sandbox» {
  -- add package configuration options here
}

lean_lib «Functional Programming in Lean» {
  globs := #[.submodules `«Functional Programming in Lean»]
}

lean_lib «Lean for the Curious Mathematician» {
  globs := #[.submodules `«Lean for the Curious Mathematician»]
}

But I'm still seeing errors that would be resolved if Mathlib were available

[Scott Morrison]

Are you opening the entire folder in VSCode? If you open individual files that will not work.

[Alex Sweeney]

I needed import Mathlib and it resolved my errors. Silly mistake. It actually looks like I can import anything from Mathlib and it works.

The reason I hadn't imported anything was because my error was about a missing instance and I had no idea which specific thing I needed to import to fix it.

typeclass instance problem is stuck, it is often due to metavariables
  HAdd (?m.564 a b) (?m.565 a b) ℝ✝

Then I found out you can just import the whole Mathlib. It feels a little hacky, is that bad practice?

[Scott Morrison]

Once your work is done you should carefully reduce imports again, but during development it is fine.

[Scott Morrison]

(Certainly if you want to contribute your work to Mathlib, then import Mathlib is not allowed. :-)