mathlib4 as a dependency

Stream: lean4

[Flo (Florent Schaffhauser)]

Hi @Sebastian Ullrich

After reading the discussion at #lean4/help.20with.20lake.20new and doing some testing myself, I noticed that the leanprover-community Wiki on using mathlib4 as a dependency says

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

for what should probably be

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

(.git missing at the end).

I think I tried the first one and it didn't work, but then the second one worked.

I hope I'm not mistaken and that this helps!

[James Gallicchio]

I think either one should work?

[Utensil Song]

From https://github.com/leanprover/lean4/blob/master/src/lake/Lake/Util/Git.lean#L25-L31 , it seems that .git is dropped anyway, so either should work.

EDIT: tested to confirm it works for my test project that depends on mathlib4. So if it didn't work, it might be caused by other reasons.

[Flo (Florent Schaffhauser)]

Thanks for letting me know! Indeed, whatever problem I had must have been caused by something else then. Anyway, it’s working now!