how to include mathlib4 in the lakefile?

Stream: mathlib4

[Arien Malec]

This line, when uncommented, breaks Lake

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

stderr:
Error parsing '././lakefile.lean'.  Please restart the lean server after fixing the Lake configuration file.

[Arien Malec]

To note, the correct name is mathlib but it breaks either way.

[Scott Morrison]

It's @ "master" not @ "main", but hopefully that doesn't cause a parse error... Can you post your entire lakefile?

[Arien Malec]

"master" fixes the issue

[Arien Malec]

import Lake
open Lake DSL

package complex4

@[default_target]
lean_lib Complex4


require std from git "https://github.com/leanprover/std4" @ "main"
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"

Changing "master" to "main" causes the error above

[Gabriel Ebner]

This is https://github.com/leanprover/lake/issues/116