project depending on PhysLean

Stream: PhysLean

[Matteo Cipollina]

I'm trying to set up a lean repository that depends on PhysLean as well as on mathlib and I'm not sure whether I'm doing the right thing. I've set-up the lean.toml and lean.toolchain as follows:

...
...

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.22.0"

[[require]]
name = "PhysLean"
git = "https://github.com/HepLean/PhysLean"
rev = "v4.22.0"

...
...

leanprover/lean4:v4.22.0

But I'm getting this error: unknown module prefix 'PhysLean'

No directory 'PhysLean' or file 'PhysLean.olean' in the search path entries: ....

Has anyone tried this setup before?

[Matteo Cipollina]

lake update and lake build went on smoothly

[Joseph Tooby-Smith]

What are you doingg when you get this error:

 unknown module prefix 'PhysLean'

Are you in VS code?

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

What are you doingg when you get this error:

 unknown module prefix 'PhysLean'

Are you in VS code?

yes :)

[Joseph Tooby-Smith]

Does your .lake/packages/ file have PhysLean in it?

[Matteo Cipollina]

Joseph Tooby-Smith ha scritto:

What are you doingg when you get this error:

 unknown module prefix 'PhysLean'

Are you in VS code?

indeed after saving the file with 'import PhysLean' now it magically builds cache

[Matteo Cipollina]

Screenshot 2025-09-12 at 16.52.52.png

[Matteo Cipollina]

sorry, I just needed to save the file, close and relaod

[Matteo Cipollina]

I wonder whether one needs to have the mathlib dependencies since it should be a transitive dependency of PhysLean

[Joseph Tooby-Smith]

Yeah, I suspect not, since when you import Mathlib you get 'for free' all the things it depends on.

[Kevin Buzzard]

FLT only depends on Mathlib and Mathlib depends on a gazillion things which aren't my problem if I only depend on Mathlib. Can you do the same thing here and only depend on PhysLean? If you depend on both then it becomes your job to make sure that your version of Mathlib always matches your version of PhysLean, doesn't it?

[Matteo Cipollina]

Kevin Buzzard ha scritto:

FLT only depends on Mathlib and Mathlib depends on a gazillion things which aren't my problem if I only depend on Mathlib. Can you do the same thing here and only depend on PhysLean? If you depend on both then it becomes your job to make sure that your version of Mathlib always matches your version of PhysLean, doesn't it?

Thanks! I've removed the mathlib dependency, relying only on Physlean.